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

Theorem cxpeq 24298
 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 1058 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝑁 ∈ ℕ)
2 nnm1nn0 11211 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
31, 2syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝑁 − 1) ∈ ℕ0)
4 nn0uz 11598 . . . . . . 7 0 = (ℤ‘0)
53, 4syl6eleq 2698 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝑁 − 1) ∈ (ℤ‘0))
6 eluzfz1 12219 . . . . . 6 ((𝑁 − 1) ∈ (ℤ‘0) → 0 ∈ (0...(𝑁 − 1)))
75, 6syl 17 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 0 ∈ (0...(𝑁 − 1)))
8 neg1cn 11001 . . . . . . . . . 10 -1 ∈ ℂ
9 2re 10967 . . . . . . . . . . . 12 2 ∈ ℝ
10 simp2 1055 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
11 nndivre 10933 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (2 / 𝑁) ∈ ℝ)
129, 10, 11sylancr 694 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 / 𝑁) ∈ ℝ)
1312recnd 9947 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 / 𝑁) ∈ ℂ)
14 cxpcl 24220 . . . . . . . . . 10 ((-1 ∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
158, 13, 14sylancr 694 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
1615adantr 480 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
17 0nn0 11184 . . . . . . . 8 0 ∈ ℕ0
18 expcl 12740 . . . . . . . 8 (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 0 ∈ ℕ0) → ((-1↑𝑐(2 / 𝑁))↑0) ∈ ℂ)
1916, 17, 18sylancl 693 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ((-1↑𝑐(2 / 𝑁))↑0) ∈ ℂ)
2019mul02d 10113 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0 · ((-1↑𝑐(2 / 𝑁))↑0)) = 0)
21 simprl 790 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐴 = 0)
2221oveq1d 6564 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐴𝑁) = (0↑𝑁))
23 simprr 792 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐴𝑁) = 𝐵)
2410expd 12886 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0↑𝑁) = 0)
2522, 23, 243eqtr3d 2652 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐵 = 0)
2625oveq1d 6564 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐵𝑐(1 / 𝑁)) = (0↑𝑐(1 / 𝑁)))
27 nncn 10905 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
28 nnne0 10930 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
29 reccl 10571 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ∈ ℂ)
30 recne0 10577 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ≠ 0)
3129, 300cxpd 24256 . . . . . . . . . 10 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (0↑𝑐(1 / 𝑁)) = 0)
3227, 28, 31syl2anc 691 . . . . . . . . 9 (𝑁 ∈ ℕ → (0↑𝑐(1 / 𝑁)) = 0)
331, 32syl 17 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0↑𝑐(1 / 𝑁)) = 0)
3426, 33eqtrd 2644 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐵𝑐(1 / 𝑁)) = 0)
3534oveq1d 6564 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)) = (0 · ((-1↑𝑐(2 / 𝑁))↑0)))
3620, 35, 213eqtr4rd 2655 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)))
37 oveq2 6557 . . . . . . . 8 (𝑛 = 0 → ((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑0))
3837oveq2d 6565 . . . . . . 7 (𝑛 = 0 → ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)))
3938eqeq2d 2620 . . . . . 6 (𝑛 = 0 → (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0))))
4039rspcev 3282 . . . . 5 ((0 ∈ (0...(𝑁 − 1)) ∧ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0))) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
417, 36, 40syl2anc 691 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
4241expr 641 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 = 0) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
43 simpl1 1057 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
44 simpr 476 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
45 simpl2 1058 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℕ)
4645nnzd 11357 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℤ)
47 explog 24144 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴𝑁) = (exp‘(𝑁 · (log‘𝐴))))
4843, 44, 46, 47syl3anc 1318 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) = (exp‘(𝑁 · (log‘𝐴))))
4948eqcomd 2616 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁))
5010nncnd 10913 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
5150adantr 480 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℂ)
5243, 44logcld 24121 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ)
5351, 52mulcld 9939 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝑁 · (log‘𝐴)) ∈ ℂ)
5445nnnn0d 11228 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℕ0)
5543, 54expcld 12870 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) ∈ ℂ)
5643, 44, 46expne0d 12876 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) ≠ 0)
57 eflogeq 24152 . . . . . . 7 (((𝑁 · (log‘𝐴)) ∈ ℂ ∧ (𝐴𝑁) ∈ ℂ ∧ (𝐴𝑁) ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
5853, 55, 56, 57syl3anc 1318 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
5949, 58mpbid 221 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)))
6055, 56logcld 24121 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘(𝐴𝑁)) ∈ ℂ)
6160adantr 480 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (log‘(𝐴𝑁)) ∈ ℂ)
62 ax-icn 9874 . . . . . . . . . . 11 i ∈ ℂ
63 2cn 10968 . . . . . . . . . . . 12 2 ∈ ℂ
64 picn 24015 . . . . . . . . . . . 12 π ∈ ℂ
6563, 64mulcli 9924 . . . . . . . . . . 11 (2 · π) ∈ ℂ
6662, 65mulcli 9924 . . . . . . . . . 10 (i · (2 · π)) ∈ ℂ
67 zcn 11259 . . . . . . . . . . 11 (𝑚 ∈ ℤ → 𝑚 ∈ ℂ)
6867adantl 481 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℂ)
69 mulcl 9899 . . . . . . . . . 10 (((i · (2 · π)) ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((i · (2 · π)) · 𝑚) ∈ ℂ)
7066, 68, 69sylancr 694 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i · (2 · π)) · 𝑚) ∈ ℂ)
7161, 70addcld 9938 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) ∈ ℂ)
7251adantr 480 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℂ)
7352adantr 480 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (log‘𝐴) ∈ ℂ)
7410nnne0d 10942 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ≠ 0)
7574ad2antrr 758 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ≠ 0)
7671, 72, 73, 75divmuld 10702 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) ↔ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
77 fveq2 6103 . . . . . . . 8 ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)))
7872, 75reccld 10673 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1 / 𝑁) ∈ ℂ)
7978, 61mulcld 9939 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((1 / 𝑁) · (log‘(𝐴𝑁))) ∈ ℂ)
8013ad2antrr 758 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (2 / 𝑁) ∈ ℂ)
8180, 68mulcld 9939 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 / 𝑁) · 𝑚) ∈ ℂ)
8262, 64mulcli 9924 . . . . . . . . . . . . 13 (i · π) ∈ ℂ
83 mulcl 9899 . . . . . . . . . . . . 13 ((((2 / 𝑁) · 𝑚) ∈ ℂ ∧ (i · π) ∈ ℂ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ)
8481, 82, 83sylancl 693 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ)
85 efadd 14663 . . . . . . . . . . . 12 ((((1 / 𝑁) · (log‘(𝐴𝑁))) ∈ ℂ ∧ (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ) → (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
8679, 84, 85syl2anc 691 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
8761, 70, 72, 75divdird 10718 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (((log‘(𝐴𝑁)) / 𝑁) + (((i · (2 · π)) · 𝑚) / 𝑁)))
8861, 72, 75divrec2d 10684 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((log‘(𝐴𝑁)) / 𝑁) = ((1 / 𝑁) · (log‘(𝐴𝑁))))
8966a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i · (2 · π)) ∈ ℂ)
9089, 68, 72, 75div23d 10717 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) · 𝑚) / 𝑁) = (((i · (2 · π)) / 𝑁) · 𝑚))
9162, 63, 64mul12i 10110 . . . . . . . . . . . . . . . . . 18 (i · (2 · π)) = (2 · (i · π))
9291oveq1i 6559 . . . . . . . . . . . . . . . . 17 ((i · (2 · π)) / 𝑁) = ((2 · (i · π)) / 𝑁)
9363a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 2 ∈ ℂ)
9482a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i · π) ∈ ℂ)
9593, 94, 72, 75div23d 10717 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 · (i · π)) / 𝑁) = ((2 / 𝑁) · (i · π)))
9692, 95syl5eq 2656 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i · (2 · π)) / 𝑁) = ((2 / 𝑁) · (i · π)))
9796oveq1d 6564 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) / 𝑁) · 𝑚) = (((2 / 𝑁) · (i · π)) · 𝑚))
9880, 94, 68mul32d 10125 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 / 𝑁) · (i · π)) · 𝑚) = (((2 / 𝑁) · 𝑚) · (i · π)))
9990, 97, 983eqtrd 2648 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) · 𝑚) / 𝑁) = (((2 / 𝑁) · 𝑚) · (i · π)))
10088, 99oveq12d 6567 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) / 𝑁) + (((i · (2 · π)) · 𝑚) / 𝑁)) = (((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π))))
10187, 100eqtrd 2644 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π))))
102101fveq2d 6107 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))))
10355adantr 480 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴𝑁) ∈ ℂ)
10456adantr 480 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴𝑁) ≠ 0)
105103, 104, 78cxpefd 24258 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝐴𝑁)↑𝑐(1 / 𝑁)) = (exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))))
1068a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ∈ ℂ)
107 neg1ne0 11003 . . . . . . . . . . . . . . 15 -1 ≠ 0
108107a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ≠ 0)
109 simpr 476 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ)
110106, 108, 80, 109cxpmul2zd 24262 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = ((-1↑𝑐(2 / 𝑁))↑𝑚))
111106, 108, 81cxpefd 24258 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1))))
112 logm1 24139 . . . . . . . . . . . . . . . 16 (log‘-1) = (i · π)
113112oveq2i 6560 . . . . . . . . . . . . . . 15 (((2 / 𝑁) · 𝑚) · (log‘-1)) = (((2 / 𝑁) · 𝑚) · (i · π))
114113fveq2i 6106 . . . . . . . . . . . . . 14 (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1))) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))
115111, 114syl6eq 2660 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π))))
116106, 80cxpcld 24254 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
1178a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ∈ ℂ)
118107a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ≠ 0)
119117, 118, 13cxpne0d 24259 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ≠ 0)
120119ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐(2 / 𝑁)) ≠ 0)
121116, 120, 109expclzd 12875 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑚) ∈ ℂ)
12245adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℕ)
123109, 122zmodcld 12553 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℕ0)
124116, 123expcld 12870 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ∈ ℂ)
125123nn0zd 11356 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℤ)
126116, 120, 125expne0d 12876 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ≠ 0)
127116, 120, 125, 109expsubd 12881 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
128122nnzd 11357 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℤ)
129 zre 11258 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℤ → 𝑚 ∈ ℝ)
130129adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℝ)
131122nnrpd 11746 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℝ+)
132 moddifz 12544 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)
133130, 131, 132syl2anc 691 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)
134 expmulz 12768 . . . . . . . . . . . . . . . . 17 ((((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ (-1↑𝑐(2 / 𝑁)) ≠ 0) ∧ (𝑁 ∈ ℤ ∧ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
135116, 120, 128, 133, 134syl22anc 1319 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
136123nn0cnd 11230 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℂ)
13768, 136subcld 10271 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 − (𝑚 mod 𝑁)) ∈ ℂ)
138137, 72, 75divcan2d 10682 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (𝑚 − (𝑚 mod 𝑁)))
139138oveq2d 6565 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))))
140 root1id 24295 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
141122, 140syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
142141oveq1d 6564 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
143 1exp 12751 . . . . . . . . . . . . . . . . . 18 (((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
144133, 143syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
145142, 144eqtrd 2644 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
146135, 139, 1453eqtr3d 2652 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = 1)
147127, 146eqtr3d 2646 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 1)
148121, 124, 126, 147diveq1d 10688 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑚) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))
149110, 115, 1483eqtr3rd 2653 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π))))
150105, 149oveq12d 6567 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
15186, 102, 1503eqtr4d 2654 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
152 eflog 24127 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
15343, 44, 152syl2anc 691 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
154153adantr 480 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(log‘𝐴)) = 𝐴)
155151, 154eqeq12d 2625 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
156 zmodfz 12554 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)))
157109, 122, 156syl2anc 691 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)))
158 eqcom 2617 . . . . . . . . . . . . 13 (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴)
159 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑛 = (𝑚 mod 𝑁) → ((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))
160159oveq2d 6565 . . . . . . . . . . . . . 14 (𝑛 = (𝑚 mod 𝑁) → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
161160eqeq1d 2612 . . . . . . . . . . . . 13 (𝑛 = (𝑚 mod 𝑁) → ((((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴 ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
162158, 161syl5bb 271 . . . . . . . . . . . 12 (𝑛 = (𝑚 mod 𝑁) → (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
163162rspcev 3282 . . . . . . . . . . 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 229 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
16777, 166syl5 33 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
16876, 167sylbird 249 . . . . . 6 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
169168rexlimdva 3013 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
17059, 169mpd 15 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
171 oveq1 6556 . . . . . . 7 ((𝐴𝑁) = 𝐵 → ((𝐴𝑁)↑𝑐(1 / 𝑁)) = (𝐵𝑐(1 / 𝑁)))
172171oveq1d 6564 . . . . . 6 ((𝐴𝑁) = 𝐵 → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
173172eqeq2d 2620 . . . . 5 ((𝐴𝑁) = 𝐵 → (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
174173rexbidv 3034 . . . 4 ((𝐴𝑁) = 𝐵 → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
175170, 174syl5ibcom 234 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
17642, 175pm2.61dane 2869 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
177 simp3 1056 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
178 nnrecre 10934 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
1791783ad2ant2 1076 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 / 𝑁) ∈ ℝ)
180179recnd 9947 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 / 𝑁) ∈ ℂ)
181177, 180cxpcld 24254 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝐵𝑐(1 / 𝑁)) ∈ ℂ)
182181adantr 480 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵𝑐(1 / 𝑁)) ∈ ℂ)
183 elfznn0 12302 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
184 expcl 12740 . . . . . . 7 (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ)
18515, 183, 184syl2an 493 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ)
18610adantr 480 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
187186nnnn0d 11228 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ0)
188182, 185, 187mulexpd 12885 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = (((𝐵𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁)))
189177adantr 480 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
190 cxproot 24236 . . . . . . 7 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐵𝑐(1 / 𝑁))↑𝑁) = 𝐵)
191189, 186, 190syl2anc 691 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((𝐵𝑐(1 / 𝑁))↑𝑁) = 𝐵)
192183adantl 481 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℕ0)
193192nn0cnd 11230 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℂ)
194186nncnd 10913 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
195193, 194mulcomd 9940 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝑛 · 𝑁) = (𝑁 · 𝑛))
196195oveq2d 6565 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = ((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)))
19715adantr 480 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
198197, 187, 192expmuld 12873 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁))
199197, 192, 187expmuld 12873 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛))
200196, 198, 1993eqtr3d 2652 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛))
201186, 140syl 17 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
202201oveq1d 6564 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛) = (1↑𝑛))
203 elfzelz 12213 . . . . . . . . 9 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℤ)
204203adantl 481 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℤ)
205 1exp 12751 . . . . . . . 8 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
206204, 205syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (1↑𝑛) = 1)
207200, 202, 2063eqtrd 2648 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = 1)
208191, 207oveq12d 6567 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁)) = (𝐵 · 1))
209189mulid1d 9936 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵 · 1) = 𝐵)
210188, 208, 2093eqtrd 2648 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵)
211 oveq1 6556 . . . . 5 (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁))
212211eqeq1d 2612 . . . 4 (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → ((𝐴𝑁) = 𝐵 ↔ (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵))
213210, 212syl5ibrcom 236 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = 𝐵))
214213rexlimdva 3013 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = 𝐵))
215176, 214impbid 201 1 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816  ici 9817   + caddc 9818   · cmul 9820   − cmin 10145  -cneg 10146   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  ...cfz 12197   mod cmo 12530  ↑cexp 12722  expce 14631  πcpi 14636  logclog 24105  ↑𝑐ccxp 24106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108 This theorem is referenced by:  1cubr  24369
 Copyright terms: Public domain W3C validator