| Step | Hyp | Ref
| Expression |
| 1 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝑁 ∈ ℕ) |
| 2 | | nnm1nn0 12567 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝑁 − 1) ∈
ℕ0) |
| 4 | | nn0uz 12920 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
| 5 | 3, 4 | eleqtrdi 2851 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝑁 − 1) ∈
(ℤ≥‘0)) |
| 6 | | eluzfz1 13571 |
. . . . . 6
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑁 − 1))) |
| 7 | 5, 6 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 0 ∈ (0...(𝑁 − 1))) |
| 8 | | neg1cn 12380 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
| 9 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 10 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈
ℕ) |
| 11 | | nndivre 12307 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℕ) → (2 / 𝑁) ∈ ℝ) |
| 12 | 9, 10, 11 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 /
𝑁) ∈
ℝ) |
| 13 | 12 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 /
𝑁) ∈
ℂ) |
| 14 | | cxpcl 26716 |
. . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
| 15 | 8, 13, 14 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (-1↑𝑐(2 /
𝑁)) ∈
ℂ) |
| 17 | | 0nn0 12541 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
| 18 | | expcl 14120 |
. . . . . . . 8
⊢
(((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 0 ∈
ℕ0) → ((-1↑𝑐(2 / 𝑁))↑0) ∈
ℂ) |
| 19 | 16, 17, 18 | sylancl 586 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → ((-1↑𝑐(2 /
𝑁))↑0) ∈
ℂ) |
| 20 | 19 | mul02d 11459 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (0 ·
((-1↑𝑐(2 / 𝑁))↑0)) = 0) |
| 21 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝐴 = 0) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐴↑𝑁) = (0↑𝑁)) |
| 23 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐴↑𝑁) = 𝐵) |
| 24 | 1 | 0expd 14179 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (0↑𝑁) = 0) |
| 25 | 22, 23, 24 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝐵 = 0) |
| 26 | 25 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐵↑𝑐(1 / 𝑁)) =
(0↑𝑐(1 / 𝑁))) |
| 27 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 28 | | nnne0 12300 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 29 | | reccl 11929 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ∈
ℂ) |
| 30 | | recne0 11935 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ≠ 0) |
| 31 | 29, 30 | 0cxpd 26752 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) →
(0↑𝑐(1 / 𝑁)) = 0) |
| 32 | 27, 28, 31 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(0↑𝑐(1 / 𝑁)) = 0) |
| 33 | 1, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (0↑𝑐(1 /
𝑁)) = 0) |
| 34 | 26, 33 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐵↑𝑐(1 / 𝑁)) = 0) |
| 35 | 34 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0)) = (0 ·
((-1↑𝑐(2 / 𝑁))↑0))) |
| 36 | 20, 35, 21 | 3eqtr4rd 2788 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0))) |
| 37 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 0 →
((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑0)) |
| 38 | 37 | oveq2d 7447 |
. . . . . 6
⊢ (𝑛 = 0 → ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0))) |
| 39 | 38 | rspceeqv 3645 |
. . . . 5
⊢ ((0
∈ (0...(𝑁 − 1))
∧ 𝐴 = ((𝐵↑𝑐(1 /
𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0))) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
| 40 | 7, 36, 39 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
| 41 | 40 | expr 456 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 = 0) → ((𝐴↑𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 42 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
| 43 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
| 44 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℕ) |
| 45 | 44 | nnzd 12640 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℤ) |
| 46 | | explog 26636 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) |
| 47 | 42, 43, 45, 46 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) |
| 48 | 47 | eqcomd 2743 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
(exp‘(𝑁 ·
(log‘𝐴))) = (𝐴↑𝑁)) |
| 49 | 10 | nncnd 12282 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈
ℂ) |
| 50 | 49 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℂ) |
| 51 | 42, 43 | logcld 26612 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
| 52 | 50, 51 | mulcld 11281 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝑁 · (log‘𝐴)) ∈
ℂ) |
| 53 | 44 | nnnn0d 12587 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℕ0) |
| 54 | 42, 53 | expcld 14186 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴↑𝑁) ∈ ℂ) |
| 55 | 42, 43, 45 | expne0d 14192 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴↑𝑁) ≠ 0) |
| 56 | | eflogeq 26644 |
. . . . . . 7
⊢ (((𝑁 · (log‘𝐴)) ∈ ℂ ∧ (𝐴↑𝑁) ∈ ℂ ∧ (𝐴↑𝑁) ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴↑𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)))) |
| 57 | 52, 54, 55, 56 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
((exp‘(𝑁 ·
(log‘𝐴))) = (𝐴↑𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)))) |
| 58 | 48, 57 | mpbid 232 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚))) |
| 59 | 54, 55 | logcld 26612 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
(log‘(𝐴↑𝑁)) ∈
ℂ) |
| 60 | 59 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(log‘(𝐴↑𝑁)) ∈
ℂ) |
| 61 | | ax-icn 11214 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
| 62 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 63 | | picn 26501 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
| 64 | 62, 63 | mulcli 11268 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
| 65 | 61, 64 | mulcli 11268 |
. . . . . . . . . 10
⊢ (i
· (2 · π)) ∈ ℂ |
| 66 | | zcn 12618 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) |
| 67 | 66 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℂ) |
| 68 | | mulcl 11239 |
. . . . . . . . . 10
⊢ (((i
· (2 · π)) ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((i · (2
· π)) · 𝑚)
∈ ℂ) |
| 69 | 65, 67, 68 | sylancr 587 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i
· (2 · π)) · 𝑚) ∈ ℂ) |
| 70 | 60, 69 | addcld 11280 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) ∈
ℂ) |
| 71 | 50 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℂ) |
| 72 | 51 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(log‘𝐴) ∈
ℂ) |
| 73 | 10 | nnne0d 12316 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ≠ 0) |
| 74 | 73 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ≠ 0) |
| 75 | 70, 71, 72, 74 | divmuld 12065 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (log‘𝐴) ↔ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)))) |
| 76 | | fveq2 6906 |
. . . . . . . 8
⊢
((((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁) = (log‘𝐴) → (exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(log‘𝐴))) |
| 77 | 71, 74 | reccld 12036 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1 /
𝑁) ∈
ℂ) |
| 78 | 77, 60 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((1 /
𝑁) ·
(log‘(𝐴↑𝑁))) ∈
ℂ) |
| 79 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (2 /
𝑁) ∈
ℂ) |
| 80 | 79, 67 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 /
𝑁) · 𝑚) ∈
ℂ) |
| 81 | 61, 63 | mulcli 11268 |
. . . . . . . . . . . . 13
⊢ (i
· π) ∈ ℂ |
| 82 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((((2 /
𝑁) · 𝑚) ∈ ℂ ∧ (i
· π) ∈ ℂ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈
ℂ) |
| 83 | 80, 81, 82 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 /
𝑁) · 𝑚) · (i · π))
∈ ℂ) |
| 84 | | efadd 16130 |
. . . . . . . . . . . 12
⊢ ((((1 /
𝑁) ·
(log‘(𝐴↑𝑁))) ∈ ℂ ∧ (((2 /
𝑁) · 𝑚) · (i · π))
∈ ℂ) → (exp‘(((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) =
((exp‘((1 / 𝑁)
· (log‘(𝐴↑𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))))) |
| 85 | 78, 83, 84 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(((1 / 𝑁)
· (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) =
((exp‘((1 / 𝑁)
· (log‘(𝐴↑𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))))) |
| 86 | 60, 69, 71, 74 | divdird 12081 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (((log‘(𝐴↑𝑁)) / 𝑁) + (((i · (2 · π))
· 𝑚) / 𝑁))) |
| 87 | 60, 71, 74 | divrec2d 12047 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((log‘(𝐴↑𝑁)) / 𝑁) = ((1 / 𝑁) · (log‘(𝐴↑𝑁)))) |
| 88 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i
· (2 · π)) ∈ ℂ) |
| 89 | 88, 67, 71, 74 | div23d 12080 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i
· (2 · π)) · 𝑚) / 𝑁) = (((i · (2 · π)) / 𝑁) · 𝑚)) |
| 90 | 61, 62, 63 | mul12i 11456 |
. . . . . . . . . . . . . . . . . 18
⊢ (i
· (2 · π)) = (2 · (i · π)) |
| 91 | 90 | oveq1i 7441 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
· (2 · π)) / 𝑁) = ((2 · (i · π)) / 𝑁) |
| 92 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 2 ∈
ℂ) |
| 93 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i
· π) ∈ ℂ) |
| 94 | 92, 93, 71, 74 | div23d 12080 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2
· (i · π)) / 𝑁) = ((2 / 𝑁) · (i ·
π))) |
| 95 | 91, 94 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i
· (2 · π)) / 𝑁) = ((2 / 𝑁) · (i ·
π))) |
| 96 | 95 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i
· (2 · π)) / 𝑁) · 𝑚) = (((2 / 𝑁) · (i · π)) · 𝑚)) |
| 97 | 79, 93, 67 | mul32d 11471 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 /
𝑁) · (i ·
π)) · 𝑚) = (((2 /
𝑁) · 𝑚) · (i ·
π))) |
| 98 | 89, 96, 97 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i
· (2 · π)) · 𝑚) / 𝑁) = (((2 / 𝑁) · 𝑚) · (i ·
π))) |
| 99 | 87, 98 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((log‘(𝐴↑𝑁)) / 𝑁) + (((i · (2 · π))
· 𝑚) / 𝑁)) = (((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i ·
π)))) |
| 100 | 86, 99 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i ·
π)))) |
| 101 | 100 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i ·
π))))) |
| 102 | 54 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) |
| 103 | 55 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴↑𝑁) ≠ 0) |
| 104 | 102, 103,
77 | cxpefd 26754 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝐴↑𝑁)↑𝑐(1 / 𝑁)) = (exp‘((1 / 𝑁) · (log‘(𝐴↑𝑁))))) |
| 105 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1
∈ ℂ) |
| 106 | | neg1ne0 12382 |
. . . . . . . . . . . . . . 15
⊢ -1 ≠
0 |
| 107 | 106 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ≠
0) |
| 108 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℤ) |
| 109 | 105, 107,
79, 108 | cxpmul2zd 26758 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐((2 / 𝑁) · 𝑚)) = ((-1↑𝑐(2 / 𝑁))↑𝑚)) |
| 110 | 105, 107,
80 | cxpefd 26754 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1)))) |
| 111 | | logm1 26631 |
. . . . . . . . . . . . . . . 16
⊢
(log‘-1) = (i · π) |
| 112 | 111 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (((2 /
𝑁) · 𝑚) · (log‘-1)) =
(((2 / 𝑁) · 𝑚) · (i ·
π)) |
| 113 | 112 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(exp‘(((2 / 𝑁)
· 𝑚) ·
(log‘-1))) = (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))) |
| 114 | 110, 113 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π)))) |
| 115 | 105, 79 | cxpcld 26750 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
| 116 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1
∈ ℂ) |
| 117 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ≠
0) |
| 118 | 116, 117,
13 | cxpne0d 26755 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ≠ 0) |
| 119 | 118 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐(2 / 𝑁)) ≠ 0) |
| 120 | 115, 119,
108 | expclzd 14191 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑𝑚) ∈ ℂ) |
| 121 | 44 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℕ) |
| 122 | 108, 121 | zmodcld 13932 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈
ℕ0) |
| 123 | 115, 122 | expcld 14186 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ∈ ℂ) |
| 124 | 122 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℤ) |
| 125 | 115, 119,
124 | expne0d 14192 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ≠ 0) |
| 126 | 115, 119,
124, 108 | expsubd 14197 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = (((-1↑𝑐(2 /
𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))) |
| 127 | 121 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℤ) |
| 128 | | zre 12617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) |
| 129 | 121 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℝ+) |
| 130 | | moddifz 13923 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ) |
| 131 | 128, 129,
130 | syl2an2 686 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ) |
| 132 | | expmulz 14149 |
. . . . . . . . . . . . . . . . 17
⊢
((((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧
(-1↑𝑐(2 / 𝑁)) ≠ 0) ∧ (𝑁 ∈ ℤ ∧ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) |
| 133 | 115, 119,
127, 131, 132 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) |
| 134 | 122 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℂ) |
| 135 | 67, 134 | subcld 11620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 − (𝑚 mod 𝑁)) ∈ ℂ) |
| 136 | 135, 71, 74 | divcan2d 12045 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (𝑚 − (𝑚 mod 𝑁))) |
| 137 | 136 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = ((-1↑𝑐(2 /
𝑁))↑(𝑚 − (𝑚 mod 𝑁)))) |
| 138 | | root1id 26797 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ →
((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) |
| 139 | 121, 138 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) |
| 140 | 139 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) |
| 141 | | 1exp 14132 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1) |
| 142 | 131, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1) |
| 143 | 140, 142 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1) |
| 144 | 133, 137,
143 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = 1) |
| 145 | 126, 144 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 1) |
| 146 | 120, 123,
125, 145 | diveq1d 12051 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑𝑚) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) |
| 147 | 109, 114,
146 | 3eqtr3rd 2786 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) = (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π)))) |
| 148 | 104, 147 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = ((exp‘((1 / 𝑁) · (log‘(𝐴↑𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))))) |
| 149 | 85, 101, 148 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))) |
| 150 | | eflog 26618 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
| 151 | 42, 43, 150 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
| 152 | 151 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(log‘𝐴)) =
𝐴) |
| 153 | 149, 152 | eqeq12d 2753 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴)) |
| 154 | | zmodfz 13933 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1))) |
| 155 | 108, 121,
154 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1))) |
| 156 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢ (𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴) |
| 157 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑚 mod 𝑁) → ((-1↑𝑐(2 /
𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) |
| 158 | 157 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 mod 𝑁) → (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))) |
| 159 | 158 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑚 mod 𝑁) → ((((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴 ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴)) |
| 160 | 156, 159 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑚 mod 𝑁) → (𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴)) |
| 161 | 160 | rspcev 3622 |
. . . . . . . . . . 11
⊢ (((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) ∧ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
| 162 | 161 | ex 412 |
. . . . . . . . . 10
⊢ ((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) → ((((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 163 | 155, 162 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((((𝐴↑𝑁)↑𝑐(1 /
𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 164 | 153, 163 | sylbid 240 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 165 | 76, 164 | syl5 34 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (log‘𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 166 | 75, 165 | sylbird 260 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) →
∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 167 | 166 | rexlimdva 3155 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) →
∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 168 | 58, 167 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
| 169 | | oveq1 7438 |
. . . . . . 7
⊢ ((𝐴↑𝑁) = 𝐵 → ((𝐴↑𝑁)↑𝑐(1 / 𝑁)) = (𝐵↑𝑐(1 / 𝑁))) |
| 170 | 169 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐴↑𝑁) = 𝐵 → (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
| 171 | 170 | eqeq2d 2748 |
. . . . 5
⊢ ((𝐴↑𝑁) = 𝐵 → (𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 172 | 171 | rexbidv 3179 |
. . . 4
⊢ ((𝐴↑𝑁) = 𝐵 → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 173 | 168, 172 | syl5ibcom 245 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((𝐴↑𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 174 | 41, 173 | pm2.61dane 3029 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
| 175 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
| 176 | | nnrecre 12308 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 /
𝑁) ∈
ℝ) |
| 177 | 176 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 /
𝑁) ∈
ℝ) |
| 178 | 177 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 /
𝑁) ∈
ℂ) |
| 179 | 175, 178 | cxpcld 26750 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑐(1 /
𝑁)) ∈
ℂ) |
| 180 | 179 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵↑𝑐(1 / 𝑁)) ∈
ℂ) |
| 181 | | elfznn0 13660 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0) |
| 182 | | expcl 14120 |
. . . . . . 7
⊢
(((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ) |
| 183 | 15, 181, 182 | syl2an 596 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ) |
| 184 | 10 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
| 185 | 184 | nnnn0d 12587 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈
ℕ0) |
| 186 | 180, 183,
185 | mulexpd 14201 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = (((𝐵↑𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2
/ 𝑁))↑𝑛)↑𝑁))) |
| 187 | 175 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ) |
| 188 | | cxproot 26732 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐵↑𝑐(1 /
𝑁))↑𝑁) = 𝐵) |
| 189 | 187, 184,
188 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((𝐵↑𝑐(1 / 𝑁))↑𝑁) = 𝐵) |
| 190 | 181 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℕ0) |
| 191 | 190 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℂ) |
| 192 | 184 | nncnd 12282 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ) |
| 193 | 191, 192 | mulcomd 11282 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝑛 · 𝑁) = (𝑁 · 𝑛)) |
| 194 | 193 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = ((-1↑𝑐(2 /
𝑁))↑(𝑁 · 𝑛))) |
| 195 | 15 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
| 196 | 195, 185,
190 | expmuld 14189 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = (((-1↑𝑐(2 /
𝑁))↑𝑛)↑𝑁)) |
| 197 | 195, 190,
185 | expmuld 14189 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑𝑛)) |
| 198 | 194, 196,
197 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑𝑛)) |
| 199 | 184, 138 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) |
| 200 | 199 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛) = (1↑𝑛)) |
| 201 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℤ) |
| 202 | 201 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℤ) |
| 203 | | 1exp 14132 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
| 204 | 202, 203 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (1↑𝑛) = 1) |
| 205 | 198, 200,
204 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = 1) |
| 206 | 189, 205 | oveq12d 7449 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵↑𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2
/ 𝑁))↑𝑛)↑𝑁)) = (𝐵 · 1)) |
| 207 | 187 | mulridd 11278 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵 · 1) = 𝐵) |
| 208 | 186, 206,
207 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵) |
| 209 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴↑𝑁) = (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁)) |
| 210 | 209 | eqeq1d 2739 |
. . . 4
⊢ (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → ((𝐴↑𝑁) = 𝐵 ↔ (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵)) |
| 211 | 208, 210 | syl5ibrcom 247 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴↑𝑁) = 𝐵)) |
| 212 | 211 | rexlimdva 3155 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
(∃𝑛 ∈
(0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴↑𝑁) = 𝐵)) |
| 213 | 174, 212 | impbid 212 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |