MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cxpeq Structured version   Visualization version   GIF version

Theorem cxpeq 24697
Description: Solve an equation involving an 𝑁-th power. The expression -1↑𝑐(2 / 𝑁) = exp(2πi / 𝑁) is a way to write the primitive 𝑁-th root of unity with the smallest positive argument. (Contributed by Mario Carneiro, 23-Apr-2015.)
Assertion
Ref Expression
cxpeq ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝑛,𝑁

Proof of Theorem cxpeq
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 simpl2 1230 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝑁 ∈ ℕ)
2 nnm1nn0 11526 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
31, 2syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝑁 − 1) ∈ ℕ0)
4 nn0uz 11915 . . . . . . 7 0 = (ℤ‘0)
53, 4syl6eleq 2849 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝑁 − 1) ∈ (ℤ‘0))
6 eluzfz1 12541 . . . . . 6 ((𝑁 − 1) ∈ (ℤ‘0) → 0 ∈ (0...(𝑁 − 1)))
75, 6syl 17 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 0 ∈ (0...(𝑁 − 1)))
8 neg1cn 11316 . . . . . . . . . 10 -1 ∈ ℂ
9 2re 11282 . . . . . . . . . . . 12 2 ∈ ℝ
10 simp2 1132 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
11 nndivre 11248 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (2 / 𝑁) ∈ ℝ)
129, 10, 11sylancr 698 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 / 𝑁) ∈ ℝ)
1312recnd 10260 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 / 𝑁) ∈ ℂ)
14 cxpcl 24619 . . . . . . . . . 10 ((-1 ∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
158, 13, 14sylancr 698 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
1615adantr 472 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
17 0nn0 11499 . . . . . . . 8 0 ∈ ℕ0
18 expcl 13072 . . . . . . . 8 (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 0 ∈ ℕ0) → ((-1↑𝑐(2 / 𝑁))↑0) ∈ ℂ)
1916, 17, 18sylancl 697 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ((-1↑𝑐(2 / 𝑁))↑0) ∈ ℂ)
2019mul02d 10426 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0 · ((-1↑𝑐(2 / 𝑁))↑0)) = 0)
21 simprl 811 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐴 = 0)
2221oveq1d 6828 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐴𝑁) = (0↑𝑁))
23 simprr 813 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐴𝑁) = 𝐵)
2410expd 13218 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0↑𝑁) = 0)
2522, 23, 243eqtr3d 2802 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐵 = 0)
2625oveq1d 6828 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐵𝑐(1 / 𝑁)) = (0↑𝑐(1 / 𝑁)))
27 nncn 11220 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
28 nnne0 11245 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
29 reccl 10884 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ∈ ℂ)
30 recne0 10890 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ≠ 0)
3129, 300cxpd 24655 . . . . . . . . . 10 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (0↑𝑐(1 / 𝑁)) = 0)
3227, 28, 31syl2anc 696 . . . . . . . . 9 (𝑁 ∈ ℕ → (0↑𝑐(1 / 𝑁)) = 0)
331, 32syl 17 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0↑𝑐(1 / 𝑁)) = 0)
3426, 33eqtrd 2794 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐵𝑐(1 / 𝑁)) = 0)
3534oveq1d 6828 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)) = (0 · ((-1↑𝑐(2 / 𝑁))↑0)))
3620, 35, 213eqtr4rd 2805 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)))
37 oveq2 6821 . . . . . . . 8 (𝑛 = 0 → ((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑0))
3837oveq2d 6829 . . . . . . 7 (𝑛 = 0 → ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)))
3938eqeq2d 2770 . . . . . 6 (𝑛 = 0 → (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0))))
4039rspcev 3449 . . . . 5 ((0 ∈ (0...(𝑁 − 1)) ∧ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0))) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
417, 36, 40syl2anc 696 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
4241expr 644 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 = 0) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
43 simpl1 1228 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
44 simpr 479 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
45 simpl2 1230 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℕ)
4645nnzd 11673 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℤ)
47 explog 24539 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴𝑁) = (exp‘(𝑁 · (log‘𝐴))))
4843, 44, 46, 47syl3anc 1477 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) = (exp‘(𝑁 · (log‘𝐴))))
4948eqcomd 2766 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁))
5010nncnd 11228 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
5150adantr 472 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℂ)
5243, 44logcld 24516 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ)
5351, 52mulcld 10252 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝑁 · (log‘𝐴)) ∈ ℂ)
5445nnnn0d 11543 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℕ0)
5543, 54expcld 13202 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) ∈ ℂ)
5643, 44, 46expne0d 13208 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) ≠ 0)
57 eflogeq 24547 . . . . . . 7 (((𝑁 · (log‘𝐴)) ∈ ℂ ∧ (𝐴𝑁) ∈ ℂ ∧ (𝐴𝑁) ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
5853, 55, 56, 57syl3anc 1477 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
5949, 58mpbid 222 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)))
6055, 56logcld 24516 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘(𝐴𝑁)) ∈ ℂ)
6160adantr 472 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (log‘(𝐴𝑁)) ∈ ℂ)
62 ax-icn 10187 . . . . . . . . . . 11 i ∈ ℂ
63 2cn 11283 . . . . . . . . . . . 12 2 ∈ ℂ
64 picn 24410 . . . . . . . . . . . 12 π ∈ ℂ
6563, 64mulcli 10237 . . . . . . . . . . 11 (2 · π) ∈ ℂ
6662, 65mulcli 10237 . . . . . . . . . 10 (i · (2 · π)) ∈ ℂ
67 zcn 11574 . . . . . . . . . . 11 (𝑚 ∈ ℤ → 𝑚 ∈ ℂ)
6867adantl 473 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℂ)
69 mulcl 10212 . . . . . . . . . 10 (((i · (2 · π)) ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((i · (2 · π)) · 𝑚) ∈ ℂ)
7066, 68, 69sylancr 698 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i · (2 · π)) · 𝑚) ∈ ℂ)
7161, 70addcld 10251 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) ∈ ℂ)
7251adantr 472 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℂ)
7352adantr 472 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (log‘𝐴) ∈ ℂ)
7410nnne0d 11257 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ≠ 0)
7574ad2antrr 764 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ≠ 0)
7671, 72, 73, 75divmuld 11015 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) ↔ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
77 fveq2 6352 . . . . . . . 8 ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)))
7872, 75reccld 10986 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1 / 𝑁) ∈ ℂ)
7978, 61mulcld 10252 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((1 / 𝑁) · (log‘(𝐴𝑁))) ∈ ℂ)
8013ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (2 / 𝑁) ∈ ℂ)
8180, 68mulcld 10252 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 / 𝑁) · 𝑚) ∈ ℂ)
8262, 64mulcli 10237 . . . . . . . . . . . . 13 (i · π) ∈ ℂ
83 mulcl 10212 . . . . . . . . . . . . 13 ((((2 / 𝑁) · 𝑚) ∈ ℂ ∧ (i · π) ∈ ℂ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ)
8481, 82, 83sylancl 697 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ)
85 efadd 15023 . . . . . . . . . . . 12 ((((1 / 𝑁) · (log‘(𝐴𝑁))) ∈ ℂ ∧ (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ) → (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
8679, 84, 85syl2anc 696 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
8761, 70, 72, 75divdird 11031 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (((log‘(𝐴𝑁)) / 𝑁) + (((i · (2 · π)) · 𝑚) / 𝑁)))
8861, 72, 75divrec2d 10997 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((log‘(𝐴𝑁)) / 𝑁) = ((1 / 𝑁) · (log‘(𝐴𝑁))))
8966a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i · (2 · π)) ∈ ℂ)
9089, 68, 72, 75div23d 11030 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) · 𝑚) / 𝑁) = (((i · (2 · π)) / 𝑁) · 𝑚))
9162, 63, 64mul12i 10423 . . . . . . . . . . . . . . . . . 18 (i · (2 · π)) = (2 · (i · π))
9291oveq1i 6823 . . . . . . . . . . . . . . . . 17 ((i · (2 · π)) / 𝑁) = ((2 · (i · π)) / 𝑁)
9363a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 2 ∈ ℂ)
9482a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i · π) ∈ ℂ)
9593, 94, 72, 75div23d 11030 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 · (i · π)) / 𝑁) = ((2 / 𝑁) · (i · π)))
9692, 95syl5eq 2806 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i · (2 · π)) / 𝑁) = ((2 / 𝑁) · (i · π)))
9796oveq1d 6828 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) / 𝑁) · 𝑚) = (((2 / 𝑁) · (i · π)) · 𝑚))
9880, 94, 68mul32d 10438 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 / 𝑁) · (i · π)) · 𝑚) = (((2 / 𝑁) · 𝑚) · (i · π)))
9990, 97, 983eqtrd 2798 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) · 𝑚) / 𝑁) = (((2 / 𝑁) · 𝑚) · (i · π)))
10088, 99oveq12d 6831 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) / 𝑁) + (((i · (2 · π)) · 𝑚) / 𝑁)) = (((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π))))
10187, 100eqtrd 2794 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π))))
102101fveq2d 6356 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))))
10355adantr 472 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴𝑁) ∈ ℂ)
10456adantr 472 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴𝑁) ≠ 0)
105103, 104, 78cxpefd 24657 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝐴𝑁)↑𝑐(1 / 𝑁)) = (exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))))
1068a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ∈ ℂ)
107 neg1ne0 11318 . . . . . . . . . . . . . . 15 -1 ≠ 0
108107a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ≠ 0)
109 simpr 479 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ)
110106, 108, 80, 109cxpmul2zd 24661 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = ((-1↑𝑐(2 / 𝑁))↑𝑚))
111106, 108, 81cxpefd 24657 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1))))
112 logm1 24534 . . . . . . . . . . . . . . . 16 (log‘-1) = (i · π)
113112oveq2i 6824 . . . . . . . . . . . . . . 15 (((2 / 𝑁) · 𝑚) · (log‘-1)) = (((2 / 𝑁) · 𝑚) · (i · π))
114113fveq2i 6355 . . . . . . . . . . . . . 14 (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1))) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))
115111, 114syl6eq 2810 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π))))
116106, 80cxpcld 24653 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
1178a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ∈ ℂ)
118107a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ≠ 0)
119117, 118, 13cxpne0d 24658 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ≠ 0)
120119ad2antrr 764 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐(2 / 𝑁)) ≠ 0)
121116, 120, 109expclzd 13207 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑚) ∈ ℂ)
12245adantr 472 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℕ)
123109, 122zmodcld 12885 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℕ0)
124116, 123expcld 13202 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ∈ ℂ)
125123nn0zd 11672 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℤ)
126116, 120, 125expne0d 13208 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ≠ 0)
127116, 120, 125, 109expsubd 13213 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
128122nnzd 11673 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℤ)
129 zre 11573 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℤ → 𝑚 ∈ ℝ)
130129adantl 473 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℝ)
131122nnrpd 12063 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℝ+)
132 moddifz 12876 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)
133130, 131, 132syl2anc 696 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)
134 expmulz 13100 . . . . . . . . . . . . . . . . 17 ((((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ (-1↑𝑐(2 / 𝑁)) ≠ 0) ∧ (𝑁 ∈ ℤ ∧ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
135116, 120, 128, 133, 134syl22anc 1478 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
136123nn0cnd 11545 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℂ)
13768, 136subcld 10584 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 − (𝑚 mod 𝑁)) ∈ ℂ)
138137, 72, 75divcan2d 10995 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (𝑚 − (𝑚 mod 𝑁)))
139138oveq2d 6829 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))))
140 root1id 24694 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
141122, 140syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
142141oveq1d 6828 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
143 1exp 13083 . . . . . . . . . . . . . . . . . 18 (((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
144133, 143syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
145142, 144eqtrd 2794 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
146135, 139, 1453eqtr3d 2802 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = 1)
147127, 146eqtr3d 2796 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 1)
148121, 124, 126, 147diveq1d 11001 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑚) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))
149110, 115, 1483eqtr3rd 2803 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π))))
150105, 149oveq12d 6831 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
15186, 102, 1503eqtr4d 2804 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
152 eflog 24522 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
15343, 44, 152syl2anc 696 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
154153adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(log‘𝐴)) = 𝐴)
155151, 154eqeq12d 2775 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
156 zmodfz 12886 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)))
157109, 122, 156syl2anc 696 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)))
158 eqcom 2767 . . . . . . . . . . . . 13 (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴)
159 oveq2 6821 . . . . . . . . . . . . . . 15 (𝑛 = (𝑚 mod 𝑁) → ((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))
160159oveq2d 6829 . . . . . . . . . . . . . 14 (𝑛 = (𝑚 mod 𝑁) → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
161160eqeq1d 2762 . . . . . . . . . . . . 13 (𝑛 = (𝑚 mod 𝑁) → ((((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴 ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
162158, 161syl5bb 272 . . . . . . . . . . . 12 (𝑛 = (𝑚 mod 𝑁) → (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
163162rspcev 3449 . . . . . . . . . . 11 (((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) ∧ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
164163ex 449 . . . . . . . . . 10 ((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) → ((((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
165157, 164syl 17 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
166155, 165sylbid 230 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
16777, 166syl5 34 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
16876, 167sylbird 250 . . . . . 6 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
169168rexlimdva 3169 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
17059, 169mpd 15 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
171 oveq1 6820 . . . . . . 7 ((𝐴𝑁) = 𝐵 → ((𝐴𝑁)↑𝑐(1 / 𝑁)) = (𝐵𝑐(1 / 𝑁)))
172171oveq1d 6828 . . . . . 6 ((𝐴𝑁) = 𝐵 → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
173172eqeq2d 2770 . . . . 5 ((𝐴𝑁) = 𝐵 → (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
174173rexbidv 3190 . . . 4 ((𝐴𝑁) = 𝐵 → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
175170, 174syl5ibcom 235 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
17642, 175pm2.61dane 3019 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
177 simp3 1133 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
178 nnrecre 11249 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
1791783ad2ant2 1129 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 / 𝑁) ∈ ℝ)
180179recnd 10260 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 / 𝑁) ∈ ℂ)
181177, 180cxpcld 24653 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝐵𝑐(1 / 𝑁)) ∈ ℂ)
182181adantr 472 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵𝑐(1 / 𝑁)) ∈ ℂ)
183 elfznn0 12626 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
184 expcl 13072 . . . . . . 7 (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ)
18515, 183, 184syl2an 495 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ)
18610adantr 472 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
187186nnnn0d 11543 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ0)
188182, 185, 187mulexpd 13217 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = (((𝐵𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁)))
189177adantr 472 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
190 cxproot 24635 . . . . . . 7 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐵𝑐(1 / 𝑁))↑𝑁) = 𝐵)
191189, 186, 190syl2anc 696 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((𝐵𝑐(1 / 𝑁))↑𝑁) = 𝐵)
192183adantl 473 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℕ0)
193192nn0cnd 11545 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℂ)
194186nncnd 11228 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
195193, 194mulcomd 10253 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝑛 · 𝑁) = (𝑁 · 𝑛))
196195oveq2d 6829 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = ((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)))
19715adantr 472 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
198197, 187, 192expmuld 13205 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁))
199197, 192, 187expmuld 13205 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛))
200196, 198, 1993eqtr3d 2802 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛))
201186, 140syl 17 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
202201oveq1d 6828 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛) = (1↑𝑛))
203 elfzelz 12535 . . . . . . . . 9 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℤ)
204203adantl 473 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℤ)
205 1exp 13083 . . . . . . . 8 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
206204, 205syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (1↑𝑛) = 1)
207200, 202, 2063eqtrd 2798 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = 1)
208191, 207oveq12d 6831 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁)) = (𝐵 · 1))
209189mulid1d 10249 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵 · 1) = 𝐵)
210188, 208, 2093eqtrd 2798 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵)
211 oveq1 6820 . . . . 5 (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁))
212211eqeq1d 2762 . . . 4 (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → ((𝐴𝑁) = 𝐵 ↔ (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵))
213210, 212syl5ibrcom 237 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = 𝐵))
214213rexlimdva 3169 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = 𝐵))
215176, 214impbid 202 1 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wrex 3051  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129  ici 10130   + caddc 10131   · cmul 10133  cmin 10458  -cneg 10459   / cdiv 10876  cn 11212  2c2 11262  0cn0 11484  cz 11569  cuz 11879  +crp 12025  ...cfz 12519   mod cmo 12862  cexp 13054  expce 14991  πcpi 14996  logclog 24500  𝑐ccxp 24501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-ef 14997  df-sin 14999  df-cos 15000  df-pi 15002  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830  df-log 24502  df-cxp 24503
This theorem is referenced by:  1cubr  24768
  Copyright terms: Public domain W3C validator