Step | Hyp | Ref
| Expression |
1 | | 2cnd 12297 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ∈
ℂ) |
2 | | simprr 770 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ) |
3 | 2 | nncnd 12235 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℂ) |
4 | | eluzge3nn 12881 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
5 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ) |
6 | 5 | nnnn0d 12539 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℕ0) |
7 | 3, 6 | expcld 14118 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℂ) |
8 | 2 | nnne0d 12269 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ≠ 0) |
9 | 5 | nnzd 12592 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℤ) |
10 | 3, 8, 9 | expne0d 14124 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ≠ 0) |
11 | 1, 7, 10 | divcan4d 12003 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) = 2) |
12 | 7 | 2timesd 12462 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 · (𝑞↑𝑁)) = ((𝑞↑𝑁) + (𝑞↑𝑁))) |
13 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
(ℤ≥‘3)) |
14 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ∈ ℕ) |
15 | | ax-flt 30007 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑞 ∈ ℕ ∧ 𝑞 ∈ ℕ ∧ 𝑝 ∈ ℕ)) → ((𝑞↑𝑁) + (𝑞↑𝑁)) ≠ (𝑝↑𝑁)) |
16 | 13, 2, 2, 14, 15 | syl13anc 1371 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑞↑𝑁) + (𝑞↑𝑁)) ≠ (𝑝↑𝑁)) |
17 | 12, 16 | eqnetrd 3007 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 · (𝑞↑𝑁)) ≠ (𝑝↑𝑁)) |
18 | 1, 7 | mulcld 11241 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 · (𝑞↑𝑁)) ∈ ℂ) |
19 | 14 | nncnd 12235 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ∈ ℂ) |
20 | 19, 6 | expcld 14118 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝↑𝑁) ∈ ℂ) |
21 | | div11 11907 |
. . . . . . . . . . . . 13
⊢ (((2
· (𝑞↑𝑁)) ∈ ℂ ∧ (𝑝↑𝑁) ∈ ℂ ∧ ((𝑞↑𝑁) ∈ ℂ ∧ (𝑞↑𝑁) ≠ 0)) → (((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) = ((𝑝↑𝑁) / (𝑞↑𝑁)) ↔ (2 · (𝑞↑𝑁)) = (𝑝↑𝑁))) |
22 | 18, 20, 7, 10, 21 | syl112anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) = ((𝑝↑𝑁) / (𝑞↑𝑁)) ↔ (2 · (𝑞↑𝑁)) = (𝑝↑𝑁))) |
23 | 22 | necon3bid 2984 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) ≠ ((𝑝↑𝑁) / (𝑞↑𝑁)) ↔ (2 · (𝑞↑𝑁)) ≠ (𝑝↑𝑁))) |
24 | 17, 23 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) ≠ ((𝑝↑𝑁) / (𝑞↑𝑁))) |
25 | 11, 24 | eqnetrrd 3008 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ≠ ((𝑝↑𝑁) / (𝑞↑𝑁))) |
26 | 19, 3, 8, 6 | expdivd 14132 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑁) = ((𝑝↑𝑁) / (𝑞↑𝑁))) |
27 | 25, 26 | neeqtrrd 3014 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ≠ ((𝑝 / 𝑞)↑𝑁)) |
28 | 19, 3, 8 | divcld 11997 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℂ) |
29 | 14 | nnne0d 12269 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ≠ 0) |
30 | 19, 3, 29, 8 | divne0d 12013 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ≠ 0) |
31 | 28, 30, 9 | cxpexpzd 26470 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐𝑁) = ((𝑝 / 𝑞)↑𝑁)) |
32 | 27, 31 | neeqtrrd 3014 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ≠ ((𝑝 / 𝑞)↑𝑐𝑁)) |
33 | | 2re 12293 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ∈
ℝ) |
35 | | 0le2 12321 |
. . . . . . . . . 10
⊢ 0 ≤
2 |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 0 ≤
2) |
37 | 14 | nnrpd 13021 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ∈ ℝ+) |
38 | 2 | nnrpd 13021 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℝ+) |
39 | 37, 38 | rpdivcld 13040 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈
ℝ+) |
40 | 39 | rpred 13023 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ) |
41 | 39 | rpge0d 13027 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 0 ≤ (𝑝 / 𝑞)) |
42 | 5 | nnred 12234 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℝ) |
43 | 40, 41, 42 | recxpcld 26482 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐𝑁) ∈ ℝ) |
44 | 40, 41, 42 | cxpge0d 26483 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 0 ≤ ((𝑝 / 𝑞)↑𝑐𝑁)) |
45 | 5 | nnrpd 13021 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℝ+) |
46 | 45 | rpreccld 13033 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (1 / 𝑁) ∈
ℝ+) |
47 | 34, 36, 43, 44, 46 | recxpf1lem 26488 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 = ((𝑝 / 𝑞)↑𝑐𝑁) ↔ (2↑𝑐(1 /
𝑁)) = (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁)))) |
48 | 47 | necon3bid 2984 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 ≠ ((𝑝 / 𝑞)↑𝑐𝑁) ↔ (2↑𝑐(1 /
𝑁)) ≠ (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁)))) |
49 | 32, 48 | mpbid 231 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) →
(2↑𝑐(1 / 𝑁)) ≠ (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁))) |
50 | 5 | nnrecred 12270 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (1 / 𝑁) ∈
ℝ) |
51 | 50 | recnd 11249 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (1 / 𝑁) ∈
ℂ) |
52 | 28, 51 | cxpcld 26467 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐(1 / 𝑁)) ∈
ℂ) |
53 | 28, 30, 51 | cxpne0d 26472 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐(1 / 𝑁)) ≠ 0) |
54 | 52, 53, 9 | cxpexpzd 26470 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑐𝑁) = (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑁)) |
55 | | cxpcom 26498 |
. . . . . . . 8
⊢ (((𝑝 / 𝑞) ∈ ℝ+ ∧ (1 / 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑐𝑁) = (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁))) |
56 | 39, 50, 42, 55 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑐𝑁) = (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁))) |
57 | | cxproot 26449 |
. . . . . . . 8
⊢ (((𝑝 / 𝑞) ∈ ℂ ∧ 𝑁 ∈ ℕ) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑁) = (𝑝 / 𝑞)) |
58 | 28, 5, 57 | syl2anc 583 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑁) = (𝑝 / 𝑞)) |
59 | 54, 56, 58 | 3eqtr3d 2779 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) |
60 | 49, 59 | neeqtrd 3009 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) →
(2↑𝑐(1 / 𝑁)) ≠ (𝑝 / 𝑞)) |
61 | 60 | neneqd 2944 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ¬
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) |
62 | 61 | ralrimivva 3199 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ∀𝑝 ∈ ℕ ∀𝑞 ∈ ℕ ¬
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) |
63 | | ralnex2 3132 |
. . 3
⊢
(∀𝑝 ∈
ℕ ∀𝑞 ∈
ℕ ¬ (2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞) ↔ ¬ ∃𝑝 ∈ ℕ ∃𝑞 ∈ ℕ
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) |
64 | 62, 63 | sylib 217 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ ∃𝑝 ∈ ℕ ∃𝑞 ∈ ℕ
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) |
65 | | 2rp 12986 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
66 | 65 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈
ℝ+) |
67 | 4 | nnrecred 12270 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 / 𝑁) ∈ ℝ) |
68 | 66, 67 | cxpgt0d 26497 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 0 < (2↑𝑐(1 /
𝑁))) |
69 | 68 | biantrud 531 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ((2↑𝑐(1 / 𝑁)) ∈ ℚ ↔
((2↑𝑐(1 / 𝑁)) ∈ ℚ ∧ 0 <
(2↑𝑐(1 / 𝑁))))) |
70 | | elpqb 12967 |
. . 3
⊢
(((2↑𝑐(1 / 𝑁)) ∈ ℚ ∧ 0 <
(2↑𝑐(1 / 𝑁))) ↔ ∃𝑝 ∈ ℕ ∃𝑞 ∈ ℕ
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) |
71 | 69, 70 | bitrdi 287 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ((2↑𝑐(1 / 𝑁)) ∈ ℚ ↔
∃𝑝 ∈ ℕ
∃𝑞 ∈ ℕ
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞))) |
72 | 64, 71 | mtbird 325 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ (2↑𝑐(1 /
𝑁)) ∈
ℚ) |