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 ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ )

Proof

Step Hyp Ref Expression
1 2cnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ∈ ℂ )
2 simprr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℕ )
3 2 nncnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℂ )
4 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
5 4 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ )
6 5 nnnn0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ0 )
7 3 6 expcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℂ )
8 2 nnne0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ≠ 0 )
9 5 nnzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℤ )
10 3 8 9 expne0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ≠ 0 )
11 1 7 10 divcan4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) = 2 )
12 7 2timesd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 · ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑞 ↑ 𝑁 ) + ( 𝑞 ↑ 𝑁 ) ) )
13 simpl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
14 simprl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ∈ ℕ )
15 ax-flt ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑞 ∈ ℕ ∧ 𝑞 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( ( 𝑞 ↑ 𝑁 ) + ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) )
16 13 2 2 14 15 syl13anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑞 ↑ 𝑁 ) + ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) )
17 12 16 eqnetrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 · ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) )
18 1 7 mulcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 · ( 𝑞 ↑ 𝑁 ) ) ∈ ℂ )
19 14 nncnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ∈ ℂ )
20 19 6 expcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 ↑ 𝑁 ) ∈ ℂ )
21 div11 ⊢ ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) ∈ ℂ ∧ ( 𝑝 ↑ 𝑁 ) ∈ ℂ ∧ ( ( 𝑞 ↑ 𝑁 ) ∈ ℂ ∧ ( 𝑞 ↑ 𝑁 ) ≠ 0 ) ) → ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) ↔ ( 2 · ( 𝑞 ↑ 𝑁 ) ) = ( 𝑝 ↑ 𝑁 ) ) )
22 18 20 7 10 21 syl112anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) ↔ ( 2 · ( 𝑞 ↑ 𝑁 ) ) = ( 𝑝 ↑ 𝑁 ) ) )
23 22 necon3bid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) ≠ ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) ↔ ( 2 · ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) ) )
24 17 23 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) ≠ ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) )
25 11 24 eqnetrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ≠ ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) )
26 19 3 8 6 expdivd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑ 𝑁 ) = ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) )
27 25 26 neeqtrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ≠ ( ( 𝑝 / 𝑞 ) ↑ 𝑁 ) )
28 19 3 8 divcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℂ )
29 14 nnne0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ≠ 0 )
30 19 3 29 8 divne0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ≠ 0 )
31 28 30 9 cxpexpzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) = ( ( 𝑝 / 𝑞 ) ↑ 𝑁 ) )
32 27 31 neeqtrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ≠ ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) )
33 2re ⊢ 2 ∈ ℝ
34 33 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ∈ ℝ )
35 0le2 ⊢ 0 ≤ 2
36 35 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 0 ≤ 2 )
37 14 nnrpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ∈ ℝ+ )
38 2 nnrpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℝ+ )
39 37 38 rpdivcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ+ )
40 39 rpred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
41 39 rpge0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 0 ≤ ( 𝑝 / 𝑞 ) )
42 5 nnred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
43 40 41 42 recxpcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ∈ ℝ )
44 40 41 42 cxpge0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 0 ≤ ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) )
45 5 nnrpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℝ+ )
46 45 rpreccld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / 𝑁 ) ∈ ℝ+ )
47 34 36 43 44 46 recxpf1lem ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 = ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↔ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) ) )
48 47 necon3bid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 ≠ ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↔ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) ) )
49 32 48 mpbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) )
50 5 nnrecred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / 𝑁 ) ∈ ℝ )
51 50 recnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / 𝑁 ) ∈ ℂ )
52 28 51 cxpcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℂ )
53 28 30 51 cxpne0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ≠ 0 )
54 52 53 9 cxpexpzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑𝑐 𝑁 ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) )
55 cxpcom ⊢ ( ( ( 𝑝 / 𝑞 ) ∈ ℝ+ ∧ ( 1 / 𝑁 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑𝑐 𝑁 ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) )
56 39 50 42 55 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑𝑐 𝑁 ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) )
57 cxproot ⊢ ( ( ( 𝑝 / 𝑞 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = ( 𝑝 / 𝑞 ) )
58 28 5 57 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = ( 𝑝 / 𝑞 ) )
59 54 56 58 3eqtr3d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
60 49 59 neeqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( 𝑝 / 𝑞 ) )
61 60 neneqd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
62 61 ralrimivva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ℕ ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
63 ralnex2 ⊢ ( ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ℕ ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) ↔ ¬ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
64 62 63 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
65 2rp ⊢ 2 ∈ ℝ+
66 65 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℝ+ )
67 4 nnrecred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 / 𝑁 ) ∈ ℝ )
68 66 67 cxpgt0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 0 < ( 2 ↑𝑐 ( 1 / 𝑁 ) ) )
69 68 biantrud ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ↔ ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ∧ 0 < ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ) ) )
70 elpqb ⊢ ( ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ∧ 0 < ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ) ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
71 69 70 bitrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) ) )
72 64 71 mtbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ )