| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2cnd 12344 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ∈
ℂ) | 
| 2 |  | simprr 773 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ) | 
| 3 | 2 | nncnd 12282 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℂ) | 
| 4 |  | eluzge3nn 12932 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) | 
| 5 | 4 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ) | 
| 6 | 5 | nnnn0d 12587 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℕ0) | 
| 7 | 3, 6 | expcld 14186 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℂ) | 
| 8 | 2 | nnne0d 12316 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ≠ 0) | 
| 9 | 5 | nnzd 12640 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℤ) | 
| 10 | 3, 8, 9 | expne0d 14192 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ≠ 0) | 
| 11 | 1, 7, 10 | divcan4d 12049 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) = 2) | 
| 12 | 7 | 2timesd 12509 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 · (𝑞↑𝑁)) = ((𝑞↑𝑁) + (𝑞↑𝑁))) | 
| 13 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
(ℤ≥‘3)) | 
| 14 |  | simprl 771 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ∈ ℕ) | 
| 15 |  | ax-flt 30491 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑞 ∈ ℕ ∧ 𝑞 ∈ ℕ ∧ 𝑝 ∈ ℕ)) → ((𝑞↑𝑁) + (𝑞↑𝑁)) ≠ (𝑝↑𝑁)) | 
| 16 | 13, 2, 2, 14, 15 | syl13anc 1374 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑞↑𝑁) + (𝑞↑𝑁)) ≠ (𝑝↑𝑁)) | 
| 17 | 12, 16 | eqnetrd 3008 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 · (𝑞↑𝑁)) ≠ (𝑝↑𝑁)) | 
| 18 | 1, 7 | mulcld 11281 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 · (𝑞↑𝑁)) ∈ ℂ) | 
| 19 | 14 | nncnd 12282 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ∈ ℂ) | 
| 20 | 19, 6 | expcld 14186 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝↑𝑁) ∈ ℂ) | 
| 21 |  | div11 11950 | . . . . . . . . . . . . 13
⊢ (((2
· (𝑞↑𝑁)) ∈ ℂ ∧ (𝑝↑𝑁) ∈ ℂ ∧ ((𝑞↑𝑁) ∈ ℂ ∧ (𝑞↑𝑁) ≠ 0)) → (((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) = ((𝑝↑𝑁) / (𝑞↑𝑁)) ↔ (2 · (𝑞↑𝑁)) = (𝑝↑𝑁))) | 
| 22 | 18, 20, 7, 10, 21 | syl112anc 1376 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) = ((𝑝↑𝑁) / (𝑞↑𝑁)) ↔ (2 · (𝑞↑𝑁)) = (𝑝↑𝑁))) | 
| 23 | 22 | necon3bid 2985 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) ≠ ((𝑝↑𝑁) / (𝑞↑𝑁)) ↔ (2 · (𝑞↑𝑁)) ≠ (𝑝↑𝑁))) | 
| 24 | 17, 23 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((2 · (𝑞↑𝑁)) / (𝑞↑𝑁)) ≠ ((𝑝↑𝑁) / (𝑞↑𝑁))) | 
| 25 | 11, 24 | eqnetrrd 3009 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ≠ ((𝑝↑𝑁) / (𝑞↑𝑁))) | 
| 26 | 19, 3, 8, 6 | expdivd 14200 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑁) = ((𝑝↑𝑁) / (𝑞↑𝑁))) | 
| 27 | 25, 26 | neeqtrrd 3015 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ≠ ((𝑝 / 𝑞)↑𝑁)) | 
| 28 | 19, 3, 8 | divcld 12043 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℂ) | 
| 29 | 14 | nnne0d 12316 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ≠ 0) | 
| 30 | 19, 3, 29, 8 | divne0d 12059 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ≠ 0) | 
| 31 | 28, 30, 9 | cxpexpzd 26753 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐𝑁) = ((𝑝 / 𝑞)↑𝑁)) | 
| 32 | 27, 31 | neeqtrrd 3015 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ≠ ((𝑝 / 𝑞)↑𝑐𝑁)) | 
| 33 |  | 2re 12340 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 34 | 33 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 2 ∈
ℝ) | 
| 35 |  | 0le2 12368 | . . . . . . . . . 10
⊢ 0 ≤
2 | 
| 36 | 35 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 0 ≤
2) | 
| 37 | 14 | nnrpd 13075 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑝 ∈ ℝ+) | 
| 38 | 2 | nnrpd 13075 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℝ+) | 
| 39 | 37, 38 | rpdivcld 13094 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈
ℝ+) | 
| 40 | 39 | rpred 13077 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ) | 
| 41 | 39 | rpge0d 13081 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 0 ≤ (𝑝 / 𝑞)) | 
| 42 | 5 | nnred 12281 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℝ) | 
| 43 | 40, 41, 42 | recxpcld 26765 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐𝑁) ∈ ℝ) | 
| 44 | 40, 41, 42 | cxpge0d 26766 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 0 ≤ ((𝑝 / 𝑞)↑𝑐𝑁)) | 
| 45 | 5 | nnrpd 13075 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℝ+) | 
| 46 | 45 | rpreccld 13087 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (1 / 𝑁) ∈
ℝ+) | 
| 47 | 34, 36, 43, 44, 46 | recxpf1lem 26771 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 = ((𝑝 / 𝑞)↑𝑐𝑁) ↔ (2↑𝑐(1 /
𝑁)) = (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁)))) | 
| 48 | 47 | necon3bid 2985 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (2 ≠ ((𝑝 / 𝑞)↑𝑐𝑁) ↔ (2↑𝑐(1 /
𝑁)) ≠ (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁)))) | 
| 49 | 32, 48 | mpbid 232 | . . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) →
(2↑𝑐(1 / 𝑁)) ≠ (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁))) | 
| 50 | 5 | nnrecred 12317 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (1 / 𝑁) ∈
ℝ) | 
| 51 | 50 | recnd 11289 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (1 / 𝑁) ∈
ℂ) | 
| 52 | 28, 51 | cxpcld 26750 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐(1 / 𝑁)) ∈
ℂ) | 
| 53 | 28, 30, 51 | cxpne0d 26755 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝑝 / 𝑞)↑𝑐(1 / 𝑁)) ≠ 0) | 
| 54 | 52, 53, 9 | cxpexpzd 26753 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑐𝑁) = (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑁)) | 
| 55 |  | cxpcom 26781 | . . . . . . . 8
⊢ (((𝑝 / 𝑞) ∈ ℝ+ ∧ (1 / 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑐𝑁) = (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁))) | 
| 56 | 39, 50, 42, 55 | syl3anc 1373 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑐𝑁) = (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁))) | 
| 57 |  | cxproot 26732 | . . . . . . . 8
⊢ (((𝑝 / 𝑞) ∈ ℂ ∧ 𝑁 ∈ ℕ) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑁) = (𝑝 / 𝑞)) | 
| 58 | 28, 5, 57 | syl2anc 584 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐(1 / 𝑁))↑𝑁) = (𝑝 / 𝑞)) | 
| 59 | 54, 56, 58 | 3eqtr3d 2785 | . . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (((𝑝 / 𝑞)↑𝑐𝑁)↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) | 
| 60 | 49, 59 | neeqtrd 3010 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) →
(2↑𝑐(1 / 𝑁)) ≠ (𝑝 / 𝑞)) | 
| 61 | 60 | neneqd 2945 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ¬
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) | 
| 62 | 61 | ralrimivva 3202 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ∀𝑝 ∈ ℕ ∀𝑞 ∈ ℕ ¬
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) | 
| 63 |  | ralnex2 3133 | . . 3
⊢
(∀𝑝 ∈
ℕ ∀𝑞 ∈
ℕ ¬ (2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞) ↔ ¬ ∃𝑝 ∈ ℕ ∃𝑞 ∈ ℕ
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) | 
| 64 | 62, 63 | sylib 218 | . 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ ∃𝑝 ∈ ℕ ∃𝑞 ∈ ℕ
(2↑𝑐(1 / 𝑁)) = (𝑝 / 𝑞)) | 
| 65 |  | 2rp 13039 | . . . . . 6
⊢ 2 ∈
ℝ+ | 
| 66 | 65 | a1i 11 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈
ℝ+) | 
| 67 | 4 | nnrecred 12317 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 / 𝑁) ∈ ℝ) | 
| 68 | 66, 67 | cxpgt0d 26780 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 0 < (2↑𝑐(1 /
𝑁))) | 
| 69 | 68 | biantrud 531 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ((2↑𝑐(1 / 𝑁)) ∈ ℚ ↔
((2↑𝑐(1 / 𝑁)) ∈ ℚ ∧ 0 <
(2↑𝑐(1 / 𝑁))))) | 
| 70 |  | elpqb 13018 | . . 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 /
𝑁)) ∈
ℚ) |