MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqr2irr Unicode version

Theorem sqr2irr 12624
Description: The square root of 2 is irrational. See zsqrelqelz 12926 for a generalization to all non-square integers. The proof's core is proven in sqr2irrlem 12623, which shows that if  A  /  B  =  sqr ( 2 ), then  A and  B are even, so  A  /  2 and  B  /  2 are smaller representatives, which is absurd. An older version of this proof was included in The Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on his Formalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
Assertion
Ref Expression
sqr2irr  |-  ( sqr `  2 )  e/  QQ

Proof of Theorem sqr2irr
Dummy variables  x  n  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2nn 9848 . . . . . 6  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
2 breq2 4108 . . . . . . . . 9  |-  ( n  =  1  ->  (
z  <  n  <->  z  <  1 ) )
32imbi1d 308 . . . . . . . 8  |-  ( n  =  1  ->  (
( z  <  n  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  ( z  <  1  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
43ralbidv 2639 . . . . . . 7  |-  ( n  =  1  ->  ( A. z  e.  NN  ( z  <  n  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  A. z  e.  NN  ( z  <  1  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
5 breq2 4108 . . . . . . . . 9  |-  ( n  =  y  ->  (
z  <  n  <->  z  <  y ) )
65imbi1d 308 . . . . . . . 8  |-  ( n  =  y  ->  (
( z  <  n  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
76ralbidv 2639 . . . . . . 7  |-  ( n  =  y  ->  ( A. z  e.  NN  ( z  <  n  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  A. z  e.  NN  ( z  < 
y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
8 breq2 4108 . . . . . . . . 9  |-  ( n  =  ( y  +  1 )  ->  (
z  <  n  <->  z  <  ( y  +  1 ) ) )
98imbi1d 308 . . . . . . . 8  |-  ( n  =  ( y  +  1 )  ->  (
( z  <  n  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  ( z  <  ( y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
109ralbidv 2639 . . . . . . 7  |-  ( n  =  ( y  +  1 )  ->  ( A. z  e.  NN  ( z  <  n  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  A. z  e.  NN  ( z  < 
( y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
11 nnnlt1 9866 . . . . . . . . 9  |-  ( z  e.  NN  ->  -.  z  <  1 )
1211pm2.21d 98 . . . . . . . 8  |-  ( z  e.  NN  ->  (
z  <  1  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  /  z
) ) )
1312rgen 2684 . . . . . . 7  |-  A. z  e.  NN  ( z  <  1  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )
14 nnrp 10455 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  RR+ )
15 rphalflt 10472 . . . . . . . . . . . . . 14  |-  ( y  e.  RR+  ->  ( y  /  2 )  < 
y )
1614, 15syl 15 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  /  2 )  <  y )
17 breq1 4107 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  / 
2 )  ->  (
z  <  y  <->  ( y  /  2 )  < 
y ) )
18 oveq2 5953 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y  / 
2 )  ->  (
x  /  z )  =  ( x  / 
( y  /  2
) ) )
1918neeq2d 2535 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( y  / 
2 )  ->  (
( sqr `  2
)  =/=  ( x  /  z )  <->  ( sqr `  2 )  =/=  (
x  /  ( y  /  2 ) ) ) )
2019ralbidv 2639 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  / 
2 )  ->  ( A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z )  <->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) ) ) )
2117, 20imbi12d 311 . . . . . . . . . . . . . . 15  |-  ( z  =  ( y  / 
2 )  ->  (
( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  ( (
y  /  2 )  <  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) ) ) ) )
2221rspcv 2956 . . . . . . . . . . . . . 14  |-  ( ( y  /  2 )  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  -> 
( ( y  / 
2 )  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
( y  /  2
) ) ) ) )
2322com13 74 . . . . . . . . . . . . 13  |-  ( ( y  /  2 )  <  y  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  -> 
( ( y  / 
2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
( y  /  2
) ) ) ) )
2416, 23syl 15 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  -> 
( ( y  / 
2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
( y  /  2
) ) ) ) )
25 simpr 447 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( sqr `  2
)  =  ( z  /  y ) )
26 zcn 10121 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  ZZ  ->  z  e.  CC )
2726ad2antlr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  z  e.  CC )
28 nncn 9844 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  y  e.  CC )
2928ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  y  e.  CC )
30 2cn 9906 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  CC
3130a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  2  e.  CC )
32 nnne0 9868 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  y  =/=  0 )
3332ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  y  =/=  0
)
34 2ne0 9919 . . . . . . . . . . . . . . . . . . 19  |-  2  =/=  0
3534a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  2  =/=  0
)
3627, 29, 31, 33, 35divcan7d 9654 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( ( z  /  2 )  / 
( y  /  2
) )  =  ( z  /  y ) )
3725, 36eqtr4d 2393 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( sqr `  2
)  =  ( ( z  /  2 )  /  ( y  / 
2 ) ) )
38 simplr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  z  e.  ZZ )
39 simpll 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  y  e.  NN )
4038, 39, 25sqr2irrlem 12623 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( ( z  /  2 )  e.  ZZ  /\  ( y  /  2 )  e.  NN ) )
4140simprd 449 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( y  / 
2 )  e.  NN )
4240simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( z  / 
2 )  e.  ZZ )
43 oveq1 5952 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( z  / 
2 )  ->  (
x  /  ( y  /  2 ) )  =  ( ( z  /  2 )  / 
( y  /  2
) ) )
4443neeq2d 2535 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( z  / 
2 )  ->  (
( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) )  <->  ( sqr `  2 )  =/=  (
( z  /  2
)  /  ( y  /  2 ) ) ) )
4544rspcv 2956 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  /  2 )  e.  ZZ  ->  ( A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
( y  /  2
) )  ->  ( sqr `  2 )  =/=  ( ( z  / 
2 )  /  (
y  /  2 ) ) ) )
4642, 45syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) )  -> 
( sqr `  2
)  =/=  ( ( z  /  2 )  /  ( y  / 
2 ) ) ) )
4741, 46embantd 50 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( ( ( y  /  2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) ) )  ->  ( sqr `  2
)  =/=  ( ( z  /  2 )  /  ( y  / 
2 ) ) ) )
4847necon2bd 2570 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  ( ( sqr `  2 )  =  ( ( z  / 
2 )  /  (
y  /  2 ) )  ->  -.  (
( y  /  2
)  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  /  (
y  /  2 ) ) ) ) )
4937, 48mpd 14 . . . . . . . . . . . . . . 15  |-  ( ( ( y  e.  NN  /\  z  e.  ZZ )  /\  ( sqr `  2
)  =  ( z  /  y ) )  ->  -.  ( (
y  /  2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) ) ) )
5049ex 423 . . . . . . . . . . . . . 14  |-  ( ( y  e.  NN  /\  z  e.  ZZ )  ->  ( ( sqr `  2
)  =  ( z  /  y )  ->  -.  ( ( y  / 
2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
( y  /  2
) ) ) ) )
5150necon2ad 2569 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  z  e.  ZZ )  ->  ( ( ( y  /  2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  ( y  / 
2 ) ) )  ->  ( sqr `  2
)  =/=  ( z  /  y ) ) )
5251ralrimdva 2709 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( y  / 
2 )  e.  NN  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
( y  /  2
) ) )  ->  A. z  e.  ZZ  ( sqr `  2 )  =/=  ( z  / 
y ) ) )
5324, 52syld 40 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  ->  A. z  e.  ZZ  ( sqr `  2 )  =/=  ( z  / 
y ) ) )
54 oveq1 5952 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
x  /  y )  =  ( z  / 
y ) )
5554neeq2d 2535 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( sqr `  2
)  =/=  ( x  /  y )  <->  ( sqr `  2 )  =/=  (
z  /  y ) ) )
5655cbvralv 2840 . . . . . . . . . . 11  |-  ( A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  /  y
)  <->  A. z  e.  ZZ  ( sqr `  2 )  =/=  ( z  / 
y ) )
5753, 56syl6ibr 218 . . . . . . . . . 10  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
y ) ) )
58 oveq2 5953 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  (
x  /  z )  =  ( x  / 
y ) )
5958neeq2d 2535 . . . . . . . . . . . 12  |-  ( z  =  y  ->  (
( sqr `  2
)  =/=  ( x  /  z )  <->  ( sqr `  2 )  =/=  (
x  /  y ) ) )
6059ralbidv 2639 . . . . . . . . . . 11  |-  ( z  =  y  ->  ( A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z )  <->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  y ) ) )
6160ceqsralv 2891 . . . . . . . . . 10  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  y ) ) )
6257, 61sylibrd 225 . . . . . . . . 9  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  ->  A. z  e.  NN  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) ) ) )
6362ancld 536 . . . . . . . 8  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  -> 
( A. z  e.  NN  ( z  < 
y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  /\  A. z  e.  NN  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) ) )
64 nnleltp1 10163 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  y  e.  NN )  ->  ( z  <_  y  <->  z  <  ( y  +  1 ) ) )
65 nnre 9843 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN  ->  z  e.  RR )
66 nnre 9843 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  RR )
67 leloe 8998 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  RR  /\  y  e.  RR )  ->  ( z  <_  y  <->  ( z  <  y  \/  z  =  y ) ) )
6865, 66, 67syl2an 463 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  y  e.  NN )  ->  ( z  <_  y  <->  ( z  <  y  \/  z  =  y ) ) )
6964, 68bitr3d 246 . . . . . . . . . . . . 13  |-  ( ( z  e.  NN  /\  y  e.  NN )  ->  ( z  <  (
y  +  1 )  <-> 
( z  <  y  \/  z  =  y
) ) )
7069ancoms 439 . . . . . . . . . . . 12  |-  ( ( y  e.  NN  /\  z  e.  NN )  ->  ( z  <  (
y  +  1 )  <-> 
( z  <  y  \/  z  =  y
) ) )
7170imbi1d 308 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  z  e.  NN )  ->  ( ( z  < 
( y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  <-> 
( ( z  < 
y  \/  z  =  y )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
72 jaob 758 . . . . . . . . . . 11  |-  ( ( ( z  <  y  \/  z  =  y
)  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  <-> 
( ( z  < 
y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  /\  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
7371, 72syl6bb 252 . . . . . . . . . 10  |-  ( ( y  e.  NN  /\  z  e.  NN )  ->  ( ( z  < 
( y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  <-> 
( ( z  < 
y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  /\  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) ) )
7473ralbidva 2635 . . . . . . . . 9  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  (
y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  A. z  e.  NN  ( ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  /\  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) ) )
75 r19.26 2751 . . . . . . . . 9  |-  ( A. z  e.  NN  (
( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  /\  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) ) )  <-> 
( A. z  e.  NN  ( z  < 
y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) )  /\  A. z  e.  NN  ( z  =  y  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) ) )
7674, 75syl6bb 252 . . . . . . . 8  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  (
y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  ( A. z  e.  NN  (
z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  /  z
) )  /\  A. z  e.  NN  (
z  =  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) ) ) ) )
7763, 76sylibrd 225 . . . . . . 7  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  y  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  ->  A. z  e.  NN  ( z  <  (
y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) ) ) )
784, 7, 10, 10, 13, 77nnind 9854 . . . . . 6  |-  ( ( y  +  1 )  e.  NN  ->  A. z  e.  NN  ( z  < 
( y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) )
791, 78syl 15 . . . . 5  |-  ( y  e.  NN  ->  A. z  e.  NN  ( z  < 
( y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2
)  =/=  ( x  /  z ) ) )
8066ltp1d 9777 . . . . 5  |-  ( y  e.  NN  ->  y  <  ( y  +  1 ) )
81 breq1 4107 . . . . . . 7  |-  ( z  =  y  ->  (
z  <  ( y  +  1 )  <->  y  <  ( y  +  1 ) ) )
82 df-ne 2523 . . . . . . . . . 10  |-  ( ( sqr `  2 )  =/=  ( x  / 
y )  <->  -.  ( sqr `  2 )  =  ( x  /  y
) )
8359, 82syl6bb 252 . . . . . . . . 9  |-  ( z  =  y  ->  (
( sqr `  2
)  =/=  ( x  /  z )  <->  -.  ( sqr `  2 )  =  ( x  /  y
) ) )
8483ralbidv 2639 . . . . . . . 8  |-  ( z  =  y  ->  ( A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z )  <->  A. x  e.  ZZ  -.  ( sqr `  2 )  =  ( x  /  y
) ) )
85 ralnex 2629 . . . . . . . 8  |-  ( A. x  e.  ZZ  -.  ( sqr `  2 )  =  ( x  / 
y )  <->  -.  E. x  e.  ZZ  ( sqr `  2
)  =  ( x  /  y ) )
8684, 85syl6bb 252 . . . . . . 7  |-  ( z  =  y  ->  ( A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z )  <->  -.  E. x  e.  ZZ  ( sqr `  2
)  =  ( x  /  y ) ) )
8781, 86imbi12d 311 . . . . . 6  |-  ( z  =  y  ->  (
( z  <  (
y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  <->  ( y  <  ( y  +  1 )  ->  -.  E. x  e.  ZZ  ( sqr `  2
)  =  ( x  /  y ) ) ) )
8887rspcv 2956 . . . . 5  |-  ( y  e.  NN  ->  ( A. z  e.  NN  ( z  <  (
y  +  1 )  ->  A. x  e.  ZZ  ( sqr `  2 )  =/=  ( x  / 
z ) )  -> 
( y  <  (
y  +  1 )  ->  -.  E. x  e.  ZZ  ( sqr `  2
)  =  ( x  /  y ) ) ) )
8979, 80, 88mp2d 41 . . . 4  |-  ( y  e.  NN  ->  -.  E. x  e.  ZZ  ( sqr `  2 )  =  ( x  /  y
) )
9089nrex 2721 . . 3  |-  -.  E. y  e.  NN  E. x  e.  ZZ  ( sqr `  2
)  =  ( x  /  y )
91 elq 10410 . . . 4  |-  ( ( sqr `  2 )  e.  QQ  <->  E. x  e.  ZZ  E. y  e.  NN  ( sqr `  2
)  =  ( x  /  y ) )
92 rexcom 2777 . . . 4  |-  ( E. x  e.  ZZ  E. y  e.  NN  ( sqr `  2 )  =  ( x  /  y
)  <->  E. y  e.  NN  E. x  e.  ZZ  ( sqr `  2 )  =  ( x  /  y
) )
9391, 92bitri 240 . . 3  |-  ( ( sqr `  2 )  e.  QQ  <->  E. y  e.  NN  E. x  e.  ZZ  ( sqr `  2
)  =  ( x  /  y ) )
9490, 93mtbir 290 . 2  |-  -.  ( sqr `  2 )  e.  QQ
95 df-nel 2524 . 2  |-  ( ( sqr `  2 )  e/  QQ  <->  -.  ( sqr `  2 )  e.  QQ )
9694, 95mpbir 200 1  |-  ( sqr `  2 )  e/  QQ
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1642    e. wcel 1710    =/= wne 2521    e/ wnel 2522   A.wral 2619   E.wrex 2620   class class class wbr 4104   ` cfv 5337  (class class class)co 5945   CCcc 8825   RRcr 8826   0cc0 8827   1c1 8828    + caddc 8830    < clt 8957    <_ cle 8958    / cdiv 9513   NNcn 9836   2c2 9885   ZZcz 10116   QQcq 10408   RR+crp 10446   sqrcsqr 11814
This theorem is referenced by:  nthruc  12626
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-cnex 8883  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-mulcom 8891  ax-addass 8892  ax-mulass 8893  ax-distr 8894  ax-i2m1 8895  ax-1ne0 8896  ax-1rid 8897  ax-rnegex 8898  ax-rrecex 8899  ax-cnre 8900  ax-pre-lttri 8901  ax-pre-lttrn 8902  ax-pre-ltadd 8903  ax-pre-mulgt0 8904  ax-pre-sup 8905
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-1st 6209  df-2nd 6210  df-riota 6391  df-recs 6475  df-rdg 6510  df-er 6747  df-en 6952  df-dom 6953  df-sdom 6954  df-sup 7284  df-pnf 8959  df-mnf 8960  df-xr 8961  df-ltxr 8962  df-le 8963  df-sub 9129  df-neg 9130  df-div 9514  df-nn 9837  df-2 9894  df-3 9895  df-n0 10058  df-z 10117  df-uz 10323  df-q 10409  df-rp 10447  df-seq 11139  df-exp 11198  df-cj 11680  df-re 11681  df-im 11682  df-sqr 11816  df-abs 11817
  Copyright terms: Public domain W3C validator