Metamath Proof Explorer

Theorem sqrt2irr

Description: The square root of 2 is irrational. See zsqrtelqelz for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem , which shows that if A / B = sqrt ( 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 inThe Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on hisFormalizing 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)

Ref Expression
Assertion sqrt2irr 
|- ( sqrt ` 2 ) e/ QQ

Proof

Step Hyp Ref Expression
1 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
2 breq2 
 |-  ( n = 1 -> ( z < n <-> z < 1 ) )
3 2 imbi1d 
 |-  ( n = 1 -> ( ( z < n -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( z < 1 -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
4 3 ralbidv 
 |-  ( n = 1 -> ( A. z e. NN ( z < n -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> A. z e. NN ( z < 1 -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
5 breq2 
 |-  ( n = y -> ( z < n <-> z < y ) )
6 5 imbi1d 
 |-  ( n = y -> ( ( z < n -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
7 6 ralbidv 
 |-  ( n = y -> ( A. z e. NN ( z < n -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
8 breq2 
 |-  ( n = ( y + 1 ) -> ( z < n <-> z < ( y + 1 ) ) )
9 8 imbi1d 
 |-  ( n = ( y + 1 ) -> ( ( z < n -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
10 9 ralbidv 
 |-  ( n = ( y + 1 ) -> ( A. z e. NN ( z < n -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
11 nnnlt1 
 |-  ( z e. NN -> -. z < 1 )
12 11 pm2.21d 
 |-  ( z e. NN -> ( z < 1 -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) )
13 12 rgen 
 |-  A. z e. NN ( z < 1 -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) )
14 nnrp 
 |-  ( y e. NN -> y e. RR+ )
15 rphalflt 
 |-  ( y e. RR+ -> ( y / 2 ) < y )
16 14 15 syl 
 |-  ( y e. NN -> ( y / 2 ) < y )
17 breq1 
 |-  ( z = ( y / 2 ) -> ( z < y <-> ( y / 2 ) < y ) )
18 oveq2 
 |-  ( z = ( y / 2 ) -> ( x / z ) = ( x / ( y / 2 ) ) )
19 18 neeq2d 
 |-  ( z = ( y / 2 ) -> ( ( sqrt ` 2 ) =/= ( x / z ) <-> ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) )
20 19 ralbidv 
 |-  ( z = ( y / 2 ) -> ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) <-> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) )
21 17 20 imbi12d 
 |-  ( z = ( y / 2 ) -> ( ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( ( y / 2 ) < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) ) )
22 21 rspcv 
 |-  ( ( y / 2 ) e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> ( ( y / 2 ) < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) ) )
23 22 com13 
 |-  ( ( y / 2 ) < y -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) ) )
24 16 23 syl 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) ) )
25 simpr 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( sqrt ` 2 ) = ( z / y ) )
26 zcn 
 |-  ( z e. ZZ -> z e. CC )
27 26 ad2antlr 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> z e. CC )
28 nncn 
 |-  ( y e. NN -> y e. CC )
29 28 ad2antrr 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> y e. CC )
30 2cnd 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> 2 e. CC )
31 nnne0 
 |-  ( y e. NN -> y =/= 0 )
32 31 ad2antrr 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> y =/= 0 )
33 2ne0 
 |-  2 =/= 0
34 33 a1i 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> 2 =/= 0 )
35 27 29 30 32 34 divcan7d 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( ( z / 2 ) / ( y / 2 ) ) = ( z / y ) )
36 25 35 eqtr4d 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( sqrt ` 2 ) = ( ( z / 2 ) / ( y / 2 ) ) )
37 simplr 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> z e. ZZ )
38 simpll 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> y e. NN )
39 37 38 25 sqrt2irrlem 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( ( z / 2 ) e. ZZ /\ ( y / 2 ) e. NN ) )
40 39 simprd 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( y / 2 ) e. NN )
41 39 simpld 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( z / 2 ) e. ZZ )
42 oveq1 
 |-  ( x = ( z / 2 ) -> ( x / ( y / 2 ) ) = ( ( z / 2 ) / ( y / 2 ) ) )
43 42 neeq2d 
 |-  ( x = ( z / 2 ) -> ( ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) <-> ( sqrt ` 2 ) =/= ( ( z / 2 ) / ( y / 2 ) ) ) )
44 43 rspcv 
 |-  ( ( z / 2 ) e. ZZ -> ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) -> ( sqrt ` 2 ) =/= ( ( z / 2 ) / ( y / 2 ) ) ) )
45 41 44 syl 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) -> ( sqrt ` 2 ) =/= ( ( z / 2 ) / ( y / 2 ) ) ) )
46 40 45 embantd 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) -> ( sqrt ` 2 ) =/= ( ( z / 2 ) / ( y / 2 ) ) ) )
47 46 necon2bd 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> ( ( sqrt ` 2 ) = ( ( z / 2 ) / ( y / 2 ) ) -> -. ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) ) )
48 36 47 mpd 
 |-  ( ( ( y e. NN /\ z e. ZZ ) /\ ( sqrt ` 2 ) = ( z / y ) ) -> -. ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) )
49 48 ex 
 |-  ( ( y e. NN /\ z e. ZZ ) -> ( ( sqrt ` 2 ) = ( z / y ) -> -. ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) ) )
50 49 necon2ad 
 |-  ( ( y e. NN /\ z e. ZZ ) -> ( ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) -> ( sqrt ` 2 ) =/= ( z / y ) ) )
51 50 ralrimdva 
 |-  ( y e. NN -> ( ( ( y / 2 ) e. NN -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / ( y / 2 ) ) ) -> A. z e. ZZ ( sqrt ` 2 ) =/= ( z / y ) ) )
52 24 51 syld 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> A. z e. ZZ ( sqrt ` 2 ) =/= ( z / y ) ) )
53 oveq1 
 |-  ( x = z -> ( x / y ) = ( z / y ) )
54 53 neeq2d 
 |-  ( x = z -> ( ( sqrt ` 2 ) =/= ( x / y ) <-> ( sqrt ` 2 ) =/= ( z / y ) ) )
55 54 cbvralvw 
 |-  ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / y ) <-> A. z e. ZZ ( sqrt ` 2 ) =/= ( z / y ) )
56 52 55 imbitrrdi 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / y ) ) )
57 oveq2 
 |-  ( z = y -> ( x / z ) = ( x / y ) )
58 57 neeq2d 
 |-  ( z = y -> ( ( sqrt ` 2 ) =/= ( x / z ) <-> ( sqrt ` 2 ) =/= ( x / y ) ) )
59 58 ralbidv 
 |-  ( z = y -> ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) <-> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / y ) ) )
60 59 ceqsralv 
 |-  ( y e. NN -> ( A. z e. NN ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / y ) ) )
61 56 60 sylibrd 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> A. z e. NN ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
62 61 ancld 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ A. z e. NN ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) ) )
63 nnleltp1 
 |-  ( ( z e. NN /\ y e. NN ) -> ( z <_ y <-> z < ( y + 1 ) ) )
64 nnre 
 |-  ( z e. NN -> z e. RR )
65 nnre 
 |-  ( y e. NN -> y e. RR )
66 leloe 
 |-  ( ( z e. RR /\ y e. RR ) -> ( z <_ y <-> ( z < y \/ z = y ) ) )
67 64 65 66 syl2an 
 |-  ( ( z e. NN /\ y e. NN ) -> ( z <_ y <-> ( z < y \/ z = y ) ) )
68 63 67 bitr3d 
 |-  ( ( z e. NN /\ y e. NN ) -> ( z < ( y + 1 ) <-> ( z < y \/ z = y ) ) )
69 68 ancoms 
 |-  ( ( y e. NN /\ z e. NN ) -> ( z < ( y + 1 ) <-> ( z < y \/ z = y ) ) )
70 69 imbi1d 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( ( z < y \/ z = y ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
71 jaob 
 |-  ( ( ( z < y \/ z = y ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
72 70 71 bitrdi 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) ) )
73 72 ralbidva 
 |-  ( y e. NN -> ( A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> A. z e. NN ( ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) ) )
74 r19.26 
 |-  ( A. z e. NN ( ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) <-> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ A. z e. NN ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
75 73 74 bitrdi 
 |-  ( y e. NN -> ( A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) /\ A. z e. NN ( z = y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) ) )
76 62 75 sylibrd 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) ) )
77 4 7 10 10 13 76 nnind 
 |-  ( ( y + 1 ) e. NN -> A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) )
78 1 77 syl 
 |-  ( y e. NN -> A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) )
79 65 ltp1d 
 |-  ( y e. NN -> y < ( y + 1 ) )
80 breq1 
 |-  ( z = y -> ( z < ( y + 1 ) <-> y < ( y + 1 ) ) )
81 df-ne 
 |-  ( ( sqrt ` 2 ) =/= ( x / y ) <-> -. ( sqrt ` 2 ) = ( x / y ) )
82 58 81 bitrdi 
 |-  ( z = y -> ( ( sqrt ` 2 ) =/= ( x / z ) <-> -. ( sqrt ` 2 ) = ( x / y ) ) )
83 82 ralbidv 
 |-  ( z = y -> ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) <-> A. x e. ZZ -. ( sqrt ` 2 ) = ( x / y ) ) )
84 ralnex 
 |-  ( A. x e. ZZ -. ( sqrt ` 2 ) = ( x / y ) <-> -. E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) )
85 83 84 bitrdi 
 |-  ( z = y -> ( A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) <-> -. E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) ) )
86 80 85 imbi12d 
 |-  ( z = y -> ( ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) <-> ( y < ( y + 1 ) -> -. E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) ) ) )
87 86 rspcv 
 |-  ( y e. NN -> ( A. z e. NN ( z < ( y + 1 ) -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ) -> ( y < ( y + 1 ) -> -. E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) ) ) )
88 78 79 87 mp2d 
 |-  ( y e. NN -> -. E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) )
89 88 nrex 
 |-  -. E. y e. NN E. x e. ZZ ( sqrt ` 2 ) = ( x / y )
90 elq 
 |-  ( ( sqrt ` 2 ) e. QQ <-> E. x e. ZZ E. y e. NN ( sqrt ` 2 ) = ( x / y ) )
91 rexcom 
 |-  ( E. x e. ZZ E. y e. NN ( sqrt ` 2 ) = ( x / y ) <-> E. y e. NN E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) )
92 90 91 bitri 
 |-  ( ( sqrt ` 2 ) e. QQ <-> E. y e. NN E. x e. ZZ ( sqrt ` 2 ) = ( x / y ) )
93 89 92 mtbir 
 |-  -. ( sqrt ` 2 ) e. QQ
94 93 nelir 
 |-  ( sqrt ` 2 ) e/ QQ