Step | Hyp | Ref
| Expression |
1 | | simpl2 1065 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝑁 ∈ ℕ) |
2 | | nnm1nn0 11334 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝑁 − 1) ∈
ℕ0) |
4 | | nn0uz 11722 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
5 | 3, 4 | syl6eleq 2711 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝑁 − 1) ∈
(ℤ≥‘0)) |
6 | | eluzfz1 12348 |
. . . . . 6
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑁 − 1))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 0 ∈ (0...(𝑁 − 1))) |
8 | | neg1cn 11124 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
9 | | 2re 11090 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
10 | | simp2 1062 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈
ℕ) |
11 | | nndivre 11056 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℕ) → (2 / 𝑁) ∈ ℝ) |
12 | 9, 10, 11 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 /
𝑁) ∈
ℝ) |
13 | 12 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 /
𝑁) ∈
ℂ) |
14 | | cxpcl 24420 |
. . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
15 | 8, 13, 14 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
16 | 15 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (-1↑𝑐(2 /
𝑁)) ∈
ℂ) |
17 | | 0nn0 11307 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
18 | | expcl 12878 |
. . . . . . . 8
⊢
(((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 0 ∈
ℕ0) → ((-1↑𝑐(2 / 𝑁))↑0) ∈
ℂ) |
19 | 16, 17, 18 | sylancl 694 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → ((-1↑𝑐(2 /
𝑁))↑0) ∈
ℂ) |
20 | 19 | mul02d 10234 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (0 ·
((-1↑𝑐(2 / 𝑁))↑0)) = 0) |
21 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝐴 = 0) |
22 | 21 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐴↑𝑁) = (0↑𝑁)) |
23 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐴↑𝑁) = 𝐵) |
24 | 1 | 0expd 13024 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (0↑𝑁) = 0) |
25 | 22, 23, 24 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝐵 = 0) |
26 | 25 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐵↑𝑐(1 / 𝑁)) =
(0↑𝑐(1 / 𝑁))) |
27 | | nncn 11028 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
28 | | nnne0 11053 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
29 | | reccl 10692 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ∈
ℂ) |
30 | | recne0 10698 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ≠ 0) |
31 | 29, 30 | 0cxpd 24456 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) →
(0↑𝑐(1 / 𝑁)) = 0) |
32 | 27, 28, 31 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(0↑𝑐(1 / 𝑁)) = 0) |
33 | 1, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (0↑𝑐(1 /
𝑁)) = 0) |
34 | 26, 33 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → (𝐵↑𝑐(1 / 𝑁)) = 0) |
35 | 34 | oveq1d 6665 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0)) = (0 ·
((-1↑𝑐(2 / 𝑁))↑0))) |
36 | 20, 35, 21 | 3eqtr4rd 2667 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → 𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0))) |
37 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑛 = 0 →
((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑0)) |
38 | 37 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑛 = 0 → ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0))) |
39 | 38 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑛 = 0 → (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0)))) |
40 | 39 | rspcev 3309 |
. . . . 5
⊢ ((0
∈ (0...(𝑁 − 1))
∧ 𝐴 = ((𝐵↑𝑐(1 /
𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑0))) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
41 | 7, 36, 40 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴↑𝑁) = 𝐵)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
42 | 41 | expr 643 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 = 0) → ((𝐴↑𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
43 | | simpl1 1064 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
44 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
45 | | simpl2 1065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℕ) |
46 | 45 | nnzd 11481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℤ) |
47 | | explog 24340 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) |
48 | 43, 44, 46, 47 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) |
49 | 48 | eqcomd 2628 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
(exp‘(𝑁 ·
(log‘𝐴))) = (𝐴↑𝑁)) |
50 | 10 | nncnd 11036 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈
ℂ) |
51 | 50 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℂ) |
52 | 43, 44 | logcld 24317 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
53 | 51, 52 | mulcld 10060 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝑁 · (log‘𝐴)) ∈
ℂ) |
54 | 45 | nnnn0d 11351 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈
ℕ0) |
55 | 43, 54 | expcld 13008 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴↑𝑁) ∈ ℂ) |
56 | 43, 44, 46 | expne0d 13014 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴↑𝑁) ≠ 0) |
57 | | eflogeq 24348 |
. . . . . . 7
⊢ (((𝑁 · (log‘𝐴)) ∈ ℂ ∧ (𝐴↑𝑁) ∈ ℂ ∧ (𝐴↑𝑁) ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴↑𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)))) |
58 | 53, 55, 56, 57 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
((exp‘(𝑁 ·
(log‘𝐴))) = (𝐴↑𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)))) |
59 | 49, 58 | mpbid 222 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚))) |
60 | 55, 56 | logcld 24317 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
(log‘(𝐴↑𝑁)) ∈
ℂ) |
61 | 60 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(log‘(𝐴↑𝑁)) ∈
ℂ) |
62 | | ax-icn 9995 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
63 | | 2cn 11091 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
64 | | picn 24211 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
65 | 63, 64 | mulcli 10045 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
66 | 62, 65 | mulcli 10045 |
. . . . . . . . . 10
⊢ (i
· (2 · π)) ∈ ℂ |
67 | | zcn 11382 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) |
68 | 67 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℂ) |
69 | | mulcl 10020 |
. . . . . . . . . 10
⊢ (((i
· (2 · π)) ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((i · (2
· π)) · 𝑚)
∈ ℂ) |
70 | 66, 68, 69 | sylancr 695 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i
· (2 · π)) · 𝑚) ∈ ℂ) |
71 | 61, 70 | addcld 10059 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) ∈
ℂ) |
72 | 51 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℂ) |
73 | 52 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(log‘𝐴) ∈
ℂ) |
74 | 10 | nnne0d 11065 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ≠ 0) |
75 | 74 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ≠ 0) |
76 | 71, 72, 73, 75 | divmuld 10823 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (log‘𝐴) ↔ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)))) |
77 | | fveq2 6191 |
. . . . . . . 8
⊢
((((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁) = (log‘𝐴) → (exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(log‘𝐴))) |
78 | 72, 75 | reccld 10794 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1 /
𝑁) ∈
ℂ) |
79 | 78, 61 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((1 /
𝑁) ·
(log‘(𝐴↑𝑁))) ∈
ℂ) |
80 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (2 /
𝑁) ∈
ℂ) |
81 | 80, 68 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 /
𝑁) · 𝑚) ∈
ℂ) |
82 | 62, 64 | mulcli 10045 |
. . . . . . . . . . . . 13
⊢ (i
· π) ∈ ℂ |
83 | | mulcl 10020 |
. . . . . . . . . . . . 13
⊢ ((((2 /
𝑁) · 𝑚) ∈ ℂ ∧ (i
· π) ∈ ℂ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈
ℂ) |
84 | 81, 82, 83 | sylancl 694 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 /
𝑁) · 𝑚) · (i · π))
∈ ℂ) |
85 | | efadd 14824 |
. . . . . . . . . . . 12
⊢ ((((1 /
𝑁) ·
(log‘(𝐴↑𝑁))) ∈ ℂ ∧ (((2 /
𝑁) · 𝑚) · (i · π))
∈ ℂ) → (exp‘(((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) =
((exp‘((1 / 𝑁)
· (log‘(𝐴↑𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))))) |
86 | 79, 84, 85 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(((1 / 𝑁)
· (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) =
((exp‘((1 / 𝑁)
· (log‘(𝐴↑𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))))) |
87 | 61, 70, 72, 75 | divdird 10839 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (((log‘(𝐴↑𝑁)) / 𝑁) + (((i · (2 · π))
· 𝑚) / 𝑁))) |
88 | 61, 72, 75 | divrec2d 10805 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((log‘(𝐴↑𝑁)) / 𝑁) = ((1 / 𝑁) · (log‘(𝐴↑𝑁)))) |
89 | 66 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i
· (2 · π)) ∈ ℂ) |
90 | 89, 68, 72, 75 | div23d 10838 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i
· (2 · π)) · 𝑚) / 𝑁) = (((i · (2 · π)) / 𝑁) · 𝑚)) |
91 | 62, 63, 64 | mul12i 10231 |
. . . . . . . . . . . . . . . . . 18
⊢ (i
· (2 · π)) = (2 · (i · π)) |
92 | 91 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
· (2 · π)) / 𝑁) = ((2 · (i · π)) / 𝑁) |
93 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 2 ∈
ℂ) |
94 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i
· π) ∈ ℂ) |
95 | 93, 94, 72, 75 | div23d 10838 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2
· (i · π)) / 𝑁) = ((2 / 𝑁) · (i ·
π))) |
96 | 92, 95 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i
· (2 · π)) / 𝑁) = ((2 / 𝑁) · (i ·
π))) |
97 | 96 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i
· (2 · π)) / 𝑁) · 𝑚) = (((2 / 𝑁) · (i · π)) · 𝑚)) |
98 | 80, 94, 68 | mul32d 10246 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 /
𝑁) · (i ·
π)) · 𝑚) = (((2 /
𝑁) · 𝑚) · (i ·
π))) |
99 | 90, 97, 98 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i
· (2 · π)) · 𝑚) / 𝑁) = (((2 / 𝑁) · 𝑚) · (i ·
π))) |
100 | 88, 99 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((log‘(𝐴↑𝑁)) / 𝑁) + (((i · (2 · π))
· 𝑚) / 𝑁)) = (((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i ·
π)))) |
101 | 87, 100 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i ·
π)))) |
102 | 101 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(((1 / 𝑁) · (log‘(𝐴↑𝑁))) + (((2 / 𝑁) · 𝑚) · (i ·
π))))) |
103 | 55 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) |
104 | 56 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴↑𝑁) ≠ 0) |
105 | 103, 104,
78 | cxpefd 24458 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝐴↑𝑁)↑𝑐(1 / 𝑁)) = (exp‘((1 / 𝑁) · (log‘(𝐴↑𝑁))))) |
106 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1
∈ ℂ) |
107 | | neg1ne0 11126 |
. . . . . . . . . . . . . . 15
⊢ -1 ≠
0 |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ≠
0) |
109 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℤ) |
110 | 106, 108,
80, 109 | cxpmul2zd 24462 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐((2 / 𝑁) · 𝑚)) = ((-1↑𝑐(2 / 𝑁))↑𝑚)) |
111 | 106, 108,
81 | cxpefd 24458 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1)))) |
112 | | logm1 24335 |
. . . . . . . . . . . . . . . 16
⊢
(log‘-1) = (i · π) |
113 | 112 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
⊢ (((2 /
𝑁) · 𝑚) · (log‘-1)) =
(((2 / 𝑁) · 𝑚) · (i ·
π)) |
114 | 113 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢
(exp‘(((2 / 𝑁)
· 𝑚) ·
(log‘-1))) = (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))) |
115 | 111, 114 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π)))) |
116 | 106, 80 | cxpcld 24454 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
117 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1
∈ ℂ) |
118 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ≠
0) |
119 | 117, 118,
13 | cxpne0d 24459 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ≠ 0) |
120 | 119 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(-1↑𝑐(2 / 𝑁)) ≠ 0) |
121 | 116, 120,
109 | expclzd 13013 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑𝑚) ∈ ℂ) |
122 | 45 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℕ) |
123 | 109, 122 | zmodcld 12691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈
ℕ0) |
124 | 116, 123 | expcld 13008 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ∈ ℂ) |
125 | 123 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℤ) |
126 | 116, 120,
125 | expne0d 13014 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ≠ 0) |
127 | 116, 120,
125, 109 | expsubd 13019 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = (((-1↑𝑐(2 /
𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))) |
128 | 122 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℤ) |
129 | | zre 11381 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) |
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℝ) |
131 | 122 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈
ℝ+) |
132 | | moddifz 12682 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ) |
133 | 130, 131,
132 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ) |
134 | | expmulz 12906 |
. . . . . . . . . . . . . . . . 17
⊢
((((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧
(-1↑𝑐(2 / 𝑁)) ≠ 0) ∧ (𝑁 ∈ ℤ ∧ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) |
135 | 116, 120,
128, 133, 134 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) |
136 | 123 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℂ) |
137 | 68, 136 | subcld 10392 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 − (𝑚 mod 𝑁)) ∈ ℂ) |
138 | 137, 72, 75 | divcan2d 10803 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (𝑚 − (𝑚 mod 𝑁))) |
139 | 138 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = ((-1↑𝑐(2 /
𝑁))↑(𝑚 − (𝑚 mod 𝑁)))) |
140 | | root1id 24495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ →
((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) |
141 | 122, 140 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) |
142 | 141 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) |
143 | | 1exp 12889 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1) |
144 | 133, 143 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1) |
145 | 142, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1) |
146 | 135, 139,
145 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = 1) |
147 | 127, 146 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 1) |
148 | 121, 124,
126, 147 | diveq1d 10809 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑𝑚) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) |
149 | 110, 115,
148 | 3eqtr3rd 2665 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) = (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π)))) |
150 | 105, 149 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = ((exp‘((1 / 𝑁) · (log‘(𝐴↑𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i ·
π))))) |
151 | 86, 102, 150 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))) |
152 | | eflog 24323 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
153 | 43, 44, 152 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
154 | 153 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
(exp‘(log‘𝐴)) =
𝐴) |
155 | 151, 154 | eqeq12d 2637 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴)) |
156 | | zmodfz 12692 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1))) |
157 | 109, 122,
156 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1))) |
158 | | eqcom 2629 |
. . . . . . . . . . . . 13
⊢ (𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴) |
159 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑚 mod 𝑁) → ((-1↑𝑐(2 /
𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) |
160 | 159 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 mod 𝑁) → (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))) |
161 | 160 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑚 mod 𝑁) → ((((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴 ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴)) |
162 | 158, 161 | syl5bb 272 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑚 mod 𝑁) → (𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴)) |
163 | 162 | rspcev 3309 |
. . . . . . . . . . 11
⊢ (((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) ∧ (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
164 | 163 | ex 450 |
. . . . . . . . . 10
⊢ ((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) → ((((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
165 | 157, 164 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((((𝐴↑𝑁)↑𝑐(1 /
𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
166 | 155, 165 | sylbid 230 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((exp‘(((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
167 | 77, 166 | syl5 34 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) →
((((log‘(𝐴↑𝑁)) + ((i · (2 ·
π)) · 𝑚)) / 𝑁) = (log‘𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
168 | 76, 167 | sylbird 250 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) →
∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
169 | 168 | rexlimdva 3031 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴↑𝑁)) + ((i · (2 · π))
· 𝑚)) →
∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
170 | 59, 169 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
171 | | oveq1 6657 |
. . . . . . 7
⊢ ((𝐴↑𝑁) = 𝐵 → ((𝐴↑𝑁)↑𝑐(1 / 𝑁)) = (𝐵↑𝑐(1 / 𝑁))) |
172 | 171 | oveq1d 6665 |
. . . . . 6
⊢ ((𝐴↑𝑁) = 𝐵 → (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))) |
173 | 172 | eqeq2d 2632 |
. . . . 5
⊢ ((𝐴↑𝑁) = 𝐵 → (𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
174 | 173 | rexbidv 3052 |
. . . 4
⊢ ((𝐴↑𝑁) = 𝐵 → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴↑𝑁)↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
175 | 170, 174 | syl5ibcom 235 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((𝐴↑𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
176 | 42, 175 | pm2.61dane 2881 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |
177 | | simp3 1063 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
178 | | nnrecre 11057 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 /
𝑁) ∈
ℝ) |
179 | 178 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 /
𝑁) ∈
ℝ) |
180 | 179 | recnd 10068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 /
𝑁) ∈
ℂ) |
181 | 177, 180 | cxpcld 24454 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝐵↑𝑐(1 /
𝑁)) ∈
ℂ) |
182 | 181 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵↑𝑐(1 / 𝑁)) ∈
ℂ) |
183 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0) |
184 | | expcl 12878 |
. . . . . . 7
⊢
(((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ) |
185 | 15, 183, 184 | syl2an 494 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ) |
186 | 10 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
187 | 186 | nnnn0d 11351 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈
ℕ0) |
188 | 182, 185,
187 | mulexpd 13023 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = (((𝐵↑𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2
/ 𝑁))↑𝑛)↑𝑁))) |
189 | 177 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ) |
190 | | cxproot 24436 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐵↑𝑐(1 /
𝑁))↑𝑁) = 𝐵) |
191 | 189, 186,
190 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((𝐵↑𝑐(1 / 𝑁))↑𝑁) = 𝐵) |
192 | 183 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℕ0) |
193 | 192 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℂ) |
194 | 186 | nncnd 11036 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ) |
195 | 193, 194 | mulcomd 10061 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝑛 · 𝑁) = (𝑁 · 𝑛)) |
196 | 195 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = ((-1↑𝑐(2 /
𝑁))↑(𝑁 · 𝑛))) |
197 | 15 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) |
198 | 197, 187,
192 | expmuld 13011 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = (((-1↑𝑐(2 /
𝑁))↑𝑛)↑𝑁)) |
199 | 197, 192,
187 | expmuld 13011 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑𝑛)) |
200 | 196, 198,
199 | 3eqtr3d 2664 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = (((-1↑𝑐(2 /
𝑁))↑𝑁)↑𝑛)) |
201 | 186, 140 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) |
202 | 201 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛) = (1↑𝑛)) |
203 | | elfzelz 12342 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℤ) |
204 | 203 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℤ) |
205 | | 1exp 12889 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
206 | 204, 205 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (1↑𝑛) = 1) |
207 | 200, 202,
206 | 3eqtrd 2660 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) →
(((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = 1) |
208 | 191, 207 | oveq12d 6668 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵↑𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2
/ 𝑁))↑𝑛)↑𝑁)) = (𝐵 · 1)) |
209 | 189 | mulid1d 10057 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵 · 1) = 𝐵) |
210 | 188, 208,
209 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵) |
211 | | oveq1 6657 |
. . . . 5
⊢ (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴↑𝑁) = (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁)) |
212 | 211 | eqeq1d 2624 |
. . . 4
⊢ (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → ((𝐴↑𝑁) = 𝐵 ↔ (((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵)) |
213 | 210, 212 | syl5ibrcom 237 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴↑𝑁) = 𝐵)) |
214 | 213 | rexlimdva 3031 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
(∃𝑛 ∈
(0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴↑𝑁) = 𝐵)) |
215 | 176, 214 | impbid 202 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) ·
((-1↑𝑐(2 / 𝑁))↑𝑛)))) |