MM> show statement sqr2irr 12791 sqr2irr $p |- ( sqr ` 2 ) e/ QQ $= ... $. MM> show proof sqr2irr 51 mtbir.1=sqr2irrlem3 $p |- -. E. x e. NN E. y e. NN ( x ^ 2 ) = ( 2 x. ( y ^ 2 ) ) 65 birexdva.1=sqr2irrlem5 $p |- ( ( x e. NN /\ y e. NN ) -> ( ( sqr ` 2 ) = ( x / y ) <-> ( x ^ 2 ) = ( 2 x. ( y ^ 2 ) ) ) ) 66 birala.1=birexdva $p |- ( x e. NN -> ( E. y e. NN ( sqr ` 2 ) = ( x / y ) <-> E. y e. NN ( x ^ 2 ) = ( 2 x. ( y ^ 2 ) ) ) ) 67 mtbir.2=birexa $p |- ( E. x e. NN E. y e. NN ( sqr ` 2 ) = ( x / y ) <-> E. x e. NN E. y e. NN ( x ^ 2 ) = ( 2 x. ( y ^ 2 ) ) ) 68 mto.1=mtbir $p |- -. E. x e. NN E. y e. NN ( sqr ` 2 ) = ( x / y ) 164 mp3an1.1=ax0re $p |- 0 e. RR 168 mp3an1.2=ltdivmult $p |- ( ( 0 e. RR /\ x e. RR /\ y e. RR ) -> ( 0 < y -> ( 0 < ( x / y ) <-> ( 0 x. y ) < x ) ) ) 169 sylan.1=mp3an1 $p |- ( ( x e. RR /\ y e. RR ) -> ( 0 < y -> ( 0 < ( x / y ) <-> ( 0 x. y ) < x ) ) ) 171 syl2an.2=zr $p |- ( x e. ZZ -> x e. RR ) 173 syl2an.3=nnret $p |- ( y e. NN -> y e. RR ) 174 syl5.1=syl2an $p |- ( ( x e. ZZ /\ y e. NN ) -> ( 0 < y -> ( 0 < ( x / y ) <-> ( 0 x. y ) < x ) ) ) 176 syl5.2=nngt0t $p |- ( y e. NN -> 0 < y ) 177 comm.1=syl5 $p |- ( ( x e. ZZ /\ y e. NN ) -> ( y e. NN -> ( 0 < ( x / y ) <-> ( 0 x. y ) < x ) ) ) 178 anabsi7.1=comm $p |- ( y e. NN -> ( ( x e. ZZ /\ y e. NN ) -> ( 0 < ( x / y ) <-> ( 0 x. y ) < x ) ) ) 179 syl5bi.1=anabsi7 $p |- ( ( x e. ZZ /\ y e. NN ) -> ( 0 < ( x / y ) <-> ( 0 x. y ) < x ) ) 187 sqrlem1.1=2re $p |- 2 e. RR 188 sqrlem1.2=2pos $p |- 0 < 2 189 mpbii.min=sqrgt0i $p |- 0 < ( sqr ` 2 ) 194 mpbii.maj=breq2 $p |- ( ( sqr ` 2 ) = ( x / y ) -> ( 0 < ( sqr ` 2 ) <-> 0 < ( x / y ) ) ) 195 syl5bi.2=mpbii $p |- ( ( sqr ` 2 ) = ( x / y ) -> 0 < ( x / y ) ) 196 sylibd.1=syl5bi $p |- ( ( x e. ZZ /\ y e. NN ) -> ( ( sqr ` 2 ) = ( x / y ) -> ( 0 x. y ) < x ) ) 215 syl.1=nncnt $p |- ( y e. NN -> y e. CC ) 217 syl.2=mulzer2t $p |- ( y e. CC -> ( 0 x. y ) = 0 ) 218 breq1d.1=syl $p |- ( y e. NN -> ( 0 x. y ) = 0 ) 219 adantl.1=breq1d $p |- ( y e. NN -> ( ( 0 x. y ) < x <-> 0 < x ) ) 220 sylibd.2=adantl $p |- ( ( x e. ZZ /\ y e. NN ) -> ( ( 0 x. y ) < x <-> 0 < x ) ) 221 exp.1=sylibd $p |- ( ( x e. ZZ /\ y e. NN ) -> ( ( sqr ` 2 ) = ( x / y ) -> 0 < x ) ) 222 r19.23adv.1=exp $p |- ( x e. ZZ -> ( y e. NN -> ( ( sqr ` 2 ) = ( x / y ) -> 0 < x ) ) ) 223 anc2li.1=r19.23adv $p |- ( x e. ZZ -> ( E. y e. NN ( sqr ` 2 ) = ( x / y ) -> 0 < x ) ) 224 syl6ibr.1=anc2li $p |- ( x e. ZZ -> ( E. y e. NN ( sqr ` 2 ) = ( x / y ) -> ( x e. ZZ /\ 0 < x ) ) ) 226 syl6ibr.2=eln $p |- ( x e. NN <-> ( x e. ZZ /\ 0 < x ) ) 227 impac.1=syl6ibr $p |- ( x e. ZZ -> ( E. y e. NN ( sqr ` 2 ) = ( x / y ) -> x e. NN ) ) 228 19.22i.1=impac $p |- ( ( x e. ZZ /\ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) -> ( x e. NN /\ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) ) 229 3imtr4.1=19.22i $p |- ( E. x ( x e. ZZ /\ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) -> E. x ( x e. NN /\ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) ) 233 3imtr4.2=df-rex $a |- ( E. x e. ZZ E. y e. NN ( sqr ` 2 ) = ( x / y ) <-> E. x ( x e. ZZ /\ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) ) 237 3imtr4.3=df-rex $a |- ( E. x e. NN E. y e. NN ( sqr ` 2 ) = ( x / y ) <-> E. x ( x e. NN /\ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) ) 238 mto.2=3imtr4 $p |- ( E. x e. ZZ E. y e. NN ( sqr ` 2 ) = ( x / y ) -> E. x e. NN E. y e. NN ( sqr ` 2 ) = ( x / y ) ) 239 mtbir.1=mto $p |- -. E. x e. ZZ E. y e. NN ( sqr ` 2 ) = ( x / y ) 243 mtbir.2=elq $p |- ( ( sqr ` 2 ) e. QQ <-> E. x e. ZZ E. y e. NN ( sqr ` 2 ) = ( x / y ) ) 244 mpbir.min=mtbir $p |- -. ( sqr ` 2 ) e. QQ 247 mpbir.maj=df-nel $a |- ( ( sqr ` 2 ) e/ QQ <-> -. ( sqr ` 2 ) e. QQ ) 248 sqr2irr=mpbir $p |- ( sqr ` 2 ) e/ QQ