Metamath Proof Explorer

Theorem nrt2irr

Description: The N -th root of 2 is irrational for N greater than 2 . For N = 2 , see sqrt2irr . This short and rather elegant proof has the minor disadvantage that it refers to ax-flt , which is still to be formalized. For a proof not requiring ax-flt , see rtprmirr . (Contributed by Prof. Loof Lirpa, 1-Apr-2025) (Proof modification is discouraged.)

Ref Expression
Assertion nrt2irr 
|- ( N e. ( ZZ>= ` 3 ) -> -. ( 2 ^c ( 1 / N ) ) e. QQ )

Proof

Step Hyp Ref Expression
1 2cnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 2 e. CC )
2 simprr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> q e. NN )
3 2 nncnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> q e. CC )
4 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
5 4 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> N e. NN )
6 5 nnnn0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> N e. NN0 )
7 3 6 expcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( q ^ N ) e. CC )
8 2 nnne0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> q =/= 0 )
9 5 nnzd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> N e. ZZ )
10 3 8 9 expne0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( q ^ N ) =/= 0 )
11 1 7 10 divcan4d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( 2 x. ( q ^ N ) ) / ( q ^ N ) ) = 2 )
12 7 2timesd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 x. ( q ^ N ) ) = ( ( q ^ N ) + ( q ^ N ) ) )
13 simpl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> N e. ( ZZ>= ` 3 ) )
14 simprl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> p e. NN )
15 ax-flt 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( q e. NN /\ q e. NN /\ p e. NN ) ) -> ( ( q ^ N ) + ( q ^ N ) ) =/= ( p ^ N ) )
16 13 2 2 14 15 syl13anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( q ^ N ) + ( q ^ N ) ) =/= ( p ^ N ) )
17 12 16 eqnetrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 x. ( q ^ N ) ) =/= ( p ^ N ) )
18 1 7 mulcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 x. ( q ^ N ) ) e. CC )
19 14 nncnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> p e. CC )
20 19 6 expcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( p ^ N ) e. CC )
21 div11 
 |-  ( ( ( 2 x. ( q ^ N ) ) e. CC /\ ( p ^ N ) e. CC /\ ( ( q ^ N ) e. CC /\ ( q ^ N ) =/= 0 ) ) -> ( ( ( 2 x. ( q ^ N ) ) / ( q ^ N ) ) = ( ( p ^ N ) / ( q ^ N ) ) <-> ( 2 x. ( q ^ N ) ) = ( p ^ N ) ) )
22 18 20 7 10 21 syl112anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( ( 2 x. ( q ^ N ) ) / ( q ^ N ) ) = ( ( p ^ N ) / ( q ^ N ) ) <-> ( 2 x. ( q ^ N ) ) = ( p ^ N ) ) )
23 22 necon3bid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( ( 2 x. ( q ^ N ) ) / ( q ^ N ) ) =/= ( ( p ^ N ) / ( q ^ N ) ) <-> ( 2 x. ( q ^ N ) ) =/= ( p ^ N ) ) )
24 17 23 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( 2 x. ( q ^ N ) ) / ( q ^ N ) ) =/= ( ( p ^ N ) / ( q ^ N ) ) )
25 11 24 eqnetrrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 2 =/= ( ( p ^ N ) / ( q ^ N ) ) )
26 19 3 8 6 expdivd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( p / q ) ^ N ) = ( ( p ^ N ) / ( q ^ N ) ) )
27 25 26 neeqtrrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 2 =/= ( ( p / q ) ^ N ) )
28 19 3 8 divcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( p / q ) e. CC )
29 14 nnne0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> p =/= 0 )
30 19 3 29 8 divne0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( p / q ) =/= 0 )
31 28 30 9 cxpexpzd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( p / q ) ^c N ) = ( ( p / q ) ^ N ) )
32 27 31 neeqtrrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 2 =/= ( ( p / q ) ^c N ) )
33 2re 
 |-  2 e. RR
34 33 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 2 e. RR )
35 0le2 
 |-  0 <_ 2
36 35 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 0 <_ 2 )
37 14 nnrpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> p e. RR+ )
38 2 nnrpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> q e. RR+ )
39 37 38 rpdivcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( p / q ) e. RR+ )
40 39 rpred 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( p / q ) e. RR )
41 39 rpge0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 0 <_ ( p / q ) )
42 5 nnred 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> N e. RR )
43 40 41 42 recxpcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( p / q ) ^c N ) e. RR )
44 40 41 42 cxpge0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> 0 <_ ( ( p / q ) ^c N ) )
45 5 nnrpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> N e. RR+ )
46 45 rpreccld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 1 / N ) e. RR+ )
47 34 36 43 44 46 recxpf1lem 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 = ( ( p / q ) ^c N ) <-> ( 2 ^c ( 1 / N ) ) = ( ( ( p / q ) ^c N ) ^c ( 1 / N ) ) ) )
48 47 necon3bid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 =/= ( ( p / q ) ^c N ) <-> ( 2 ^c ( 1 / N ) ) =/= ( ( ( p / q ) ^c N ) ^c ( 1 / N ) ) ) )
49 32 48 mpbid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 ^c ( 1 / N ) ) =/= ( ( ( p / q ) ^c N ) ^c ( 1 / N ) ) )
50 5 nnrecred 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 1 / N ) e. RR )
51 50 recnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 1 / N ) e. CC )
52 28 51 cxpcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( p / q ) ^c ( 1 / N ) ) e. CC )
53 28 30 51 cxpne0d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( p / q ) ^c ( 1 / N ) ) =/= 0 )
54 52 53 9 cxpexpzd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( ( p / q ) ^c ( 1 / N ) ) ^c N ) = ( ( ( p / q ) ^c ( 1 / N ) ) ^ N ) )
55 cxpcom 
 |-  ( ( ( p / q ) e. RR+ /\ ( 1 / N ) e. RR /\ N e. RR ) -> ( ( ( p / q ) ^c ( 1 / N ) ) ^c N ) = ( ( ( p / q ) ^c N ) ^c ( 1 / N ) ) )
56 39 50 42 55 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( ( p / q ) ^c ( 1 / N ) ) ^c N ) = ( ( ( p / q ) ^c N ) ^c ( 1 / N ) ) )
57 cxproot 
 |-  ( ( ( p / q ) e. CC /\ N e. NN ) -> ( ( ( p / q ) ^c ( 1 / N ) ) ^ N ) = ( p / q ) )
58 28 5 57 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( ( p / q ) ^c ( 1 / N ) ) ^ N ) = ( p / q ) )
59 54 56 58 3eqtr3d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( ( ( p / q ) ^c N ) ^c ( 1 / N ) ) = ( p / q ) )
60 49 59 neeqtrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> ( 2 ^c ( 1 / N ) ) =/= ( p / q ) )
61 60 neneqd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( p e. NN /\ q e. NN ) ) -> -. ( 2 ^c ( 1 / N ) ) = ( p / q ) )
62 61 ralrimivva 
 |-  ( N e. ( ZZ>= ` 3 ) -> A. p e. NN A. q e. NN -. ( 2 ^c ( 1 / N ) ) = ( p / q ) )
63 ralnex2 
 |-  ( A. p e. NN A. q e. NN -. ( 2 ^c ( 1 / N ) ) = ( p / q ) <-> -. E. p e. NN E. q e. NN ( 2 ^c ( 1 / N ) ) = ( p / q ) )
64 62 63 sylib 
 |-  ( N e. ( ZZ>= ` 3 ) -> -. E. p e. NN E. q e. NN ( 2 ^c ( 1 / N ) ) = ( p / q ) )
65 2rp 
 |-  2 e. RR+
66 65 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. RR+ )
67 4 nnrecred 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 1 / N ) e. RR )
68 66 67 cxpgt0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 < ( 2 ^c ( 1 / N ) ) )
69 68 biantrud 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( 2 ^c ( 1 / N ) ) e. QQ <-> ( ( 2 ^c ( 1 / N ) ) e. QQ /\ 0 < ( 2 ^c ( 1 / N ) ) ) ) )
70 elpqb 
 |-  ( ( ( 2 ^c ( 1 / N ) ) e. QQ /\ 0 < ( 2 ^c ( 1 / N ) ) ) <-> E. p e. NN E. q e. NN ( 2 ^c ( 1 / N ) ) = ( p / q ) )
71 69 70 bitrdi 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( 2 ^c ( 1 / N ) ) e. QQ <-> E. p e. NN E. q e. NN ( 2 ^c ( 1 / N ) ) = ( p / q ) ) )
72 64 71 mtbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> -. ( 2 ^c ( 1 / N ) ) e. QQ )