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

Theorem cxpeq 24398
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 1063 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝑁 ∈ ℕ)
2 nnm1nn0 11278 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
31, 2syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝑁 − 1) ∈ ℕ0)
4 nn0uz 11666 . . . . . . 7 0 = (ℤ‘0)
53, 4syl6eleq 2708 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝑁 − 1) ∈ (ℤ‘0))
6 eluzfz1 12290 . . . . . 6 ((𝑁 − 1) ∈ (ℤ‘0) → 0 ∈ (0...(𝑁 − 1)))
75, 6syl 17 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 0 ∈ (0...(𝑁 − 1)))
8 neg1cn 11068 . . . . . . . . . 10 -1 ∈ ℂ
9 2re 11034 . . . . . . . . . . . 12 2 ∈ ℝ
10 simp2 1060 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℕ)
11 nndivre 11000 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (2 / 𝑁) ∈ ℝ)
129, 10, 11sylancr 694 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 / 𝑁) ∈ ℝ)
1312recnd 10012 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (2 / 𝑁) ∈ ℂ)
14 cxpcl 24320 . . . . . . . . . 10 ((-1 ∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
158, 13, 14sylancr 694 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
1615adantr 481 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
17 0nn0 11251 . . . . . . . 8 0 ∈ ℕ0
18 expcl 12818 . . . . . . . 8 (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 0 ∈ ℕ0) → ((-1↑𝑐(2 / 𝑁))↑0) ∈ ℂ)
1916, 17, 18sylancl 693 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ((-1↑𝑐(2 / 𝑁))↑0) ∈ ℂ)
2019mul02d 10178 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0 · ((-1↑𝑐(2 / 𝑁))↑0)) = 0)
21 simprl 793 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐴 = 0)
2221oveq1d 6619 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐴𝑁) = (0↑𝑁))
23 simprr 795 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐴𝑁) = 𝐵)
2410expd 12964 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0↑𝑁) = 0)
2522, 23, 243eqtr3d 2663 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐵 = 0)
2625oveq1d 6619 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐵𝑐(1 / 𝑁)) = (0↑𝑐(1 / 𝑁)))
27 nncn 10972 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
28 nnne0 10997 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
29 reccl 10636 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ∈ ℂ)
30 recne0 10642 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (1 / 𝑁) ≠ 0)
3129, 300cxpd 24356 . . . . . . . . . 10 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) → (0↑𝑐(1 / 𝑁)) = 0)
3227, 28, 31syl2anc 692 . . . . . . . . 9 (𝑁 ∈ ℕ → (0↑𝑐(1 / 𝑁)) = 0)
331, 32syl 17 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (0↑𝑐(1 / 𝑁)) = 0)
3426, 33eqtrd 2655 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → (𝐵𝑐(1 / 𝑁)) = 0)
3534oveq1d 6619 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)) = (0 · ((-1↑𝑐(2 / 𝑁))↑0)))
3620, 35, 213eqtr4rd 2666 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)))
37 oveq2 6612 . . . . . . . 8 (𝑛 = 0 → ((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑0))
3837oveq2d 6620 . . . . . . 7 (𝑛 = 0 → ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0)))
3938eqeq2d 2631 . . . . . 6 (𝑛 = 0 → (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0))))
4039rspcev 3295 . . . . 5 ((0 ∈ (0...(𝑁 − 1)) ∧ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑0))) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
417, 36, 40syl2anc 692 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 = 0 ∧ (𝐴𝑁) = 𝐵)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
4241expr 642 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 = 0) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
43 simpl1 1062 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
44 simpr 477 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
45 simpl2 1063 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℕ)
4645nnzd 11425 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℤ)
47 explog 24244 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴𝑁) = (exp‘(𝑁 · (log‘𝐴))))
4843, 44, 46, 47syl3anc 1323 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) = (exp‘(𝑁 · (log‘𝐴))))
4948eqcomd 2627 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁))
5010nncnd 10980 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ∈ ℂ)
5150adantr 481 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℂ)
5243, 44logcld 24221 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ)
5351, 52mulcld 10004 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝑁 · (log‘𝐴)) ∈ ℂ)
5445nnnn0d 11295 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → 𝑁 ∈ ℕ0)
5543, 54expcld 12948 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) ∈ ℂ)
5643, 44, 46expne0d 12954 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐴𝑁) ≠ 0)
57 eflogeq 24252 . . . . . . 7 (((𝑁 · (log‘𝐴)) ∈ ℂ ∧ (𝐴𝑁) ∈ ℂ ∧ (𝐴𝑁) ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
5853, 55, 56, 57syl3anc 1323 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((exp‘(𝑁 · (log‘𝐴))) = (𝐴𝑁) ↔ ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
5949, 58mpbid 222 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)))
6055, 56logcld 24221 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (log‘(𝐴𝑁)) ∈ ℂ)
6160adantr 481 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (log‘(𝐴𝑁)) ∈ ℂ)
62 ax-icn 9939 . . . . . . . . . . 11 i ∈ ℂ
63 2cn 11035 . . . . . . . . . . . 12 2 ∈ ℂ
64 picn 24115 . . . . . . . . . . . 12 π ∈ ℂ
6563, 64mulcli 9989 . . . . . . . . . . 11 (2 · π) ∈ ℂ
6662, 65mulcli 9989 . . . . . . . . . 10 (i · (2 · π)) ∈ ℂ
67 zcn 11326 . . . . . . . . . . 11 (𝑚 ∈ ℤ → 𝑚 ∈ ℂ)
6867adantl 482 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℂ)
69 mulcl 9964 . . . . . . . . . 10 (((i · (2 · π)) ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((i · (2 · π)) · 𝑚) ∈ ℂ)
7066, 68, 69sylancr 694 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i · (2 · π)) · 𝑚) ∈ ℂ)
7161, 70addcld 10003 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) ∈ ℂ)
7251adantr 481 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℂ)
7352adantr 481 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (log‘𝐴) ∈ ℂ)
7410nnne0d 11009 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝑁 ≠ 0)
7574ad2antrr 761 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ≠ 0)
7671, 72, 73, 75divmuld 10767 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) ↔ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚))))
77 fveq2 6148 . . . . . . . 8 ((((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (log‘𝐴) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)))
7872, 75reccld 10738 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1 / 𝑁) ∈ ℂ)
7978, 61mulcld 10004 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((1 / 𝑁) · (log‘(𝐴𝑁))) ∈ ℂ)
8013ad2antrr 761 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (2 / 𝑁) ∈ ℂ)
8180, 68mulcld 10004 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 / 𝑁) · 𝑚) ∈ ℂ)
8262, 64mulcli 9989 . . . . . . . . . . . . 13 (i · π) ∈ ℂ
83 mulcl 9964 . . . . . . . . . . . . 13 ((((2 / 𝑁) · 𝑚) ∈ ℂ ∧ (i · π) ∈ ℂ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ)
8481, 82, 83sylancl 693 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ)
85 efadd 14749 . . . . . . . . . . . 12 ((((1 / 𝑁) · (log‘(𝐴𝑁))) ∈ ℂ ∧ (((2 / 𝑁) · 𝑚) · (i · π)) ∈ ℂ) → (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
8679, 84, 85syl2anc 692 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
8761, 70, 72, 75divdird 10783 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (((log‘(𝐴𝑁)) / 𝑁) + (((i · (2 · π)) · 𝑚) / 𝑁)))
8861, 72, 75divrec2d 10749 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((log‘(𝐴𝑁)) / 𝑁) = ((1 / 𝑁) · (log‘(𝐴𝑁))))
8966a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i · (2 · π)) ∈ ℂ)
9089, 68, 72, 75div23d 10782 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) · 𝑚) / 𝑁) = (((i · (2 · π)) / 𝑁) · 𝑚))
9162, 63, 64mul12i 10175 . . . . . . . . . . . . . . . . . 18 (i · (2 · π)) = (2 · (i · π))
9291oveq1i 6614 . . . . . . . . . . . . . . . . 17 ((i · (2 · π)) / 𝑁) = ((2 · (i · π)) / 𝑁)
9363a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 2 ∈ ℂ)
9482a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (i · π) ∈ ℂ)
9593, 94, 72, 75div23d 10782 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((2 · (i · π)) / 𝑁) = ((2 / 𝑁) · (i · π)))
9692, 95syl5eq 2667 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((i · (2 · π)) / 𝑁) = ((2 / 𝑁) · (i · π)))
9796oveq1d 6619 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) / 𝑁) · 𝑚) = (((2 / 𝑁) · (i · π)) · 𝑚))
9880, 94, 68mul32d 10190 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((2 / 𝑁) · (i · π)) · 𝑚) = (((2 / 𝑁) · 𝑚) · (i · π)))
9990, 97, 983eqtrd 2659 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((i · (2 · π)) · 𝑚) / 𝑁) = (((2 / 𝑁) · 𝑚) · (i · π)))
10088, 99oveq12d 6622 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) / 𝑁) + (((i · (2 · π)) · 𝑚) / 𝑁)) = (((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π))))
10187, 100eqtrd 2655 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁) = (((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π))))
102101fveq2d 6152 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(((1 / 𝑁) · (log‘(𝐴𝑁))) + (((2 / 𝑁) · 𝑚) · (i · π)))))
10355adantr 481 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴𝑁) ∈ ℂ)
10456adantr 481 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝐴𝑁) ≠ 0)
105103, 104, 78cxpefd 24358 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝐴𝑁)↑𝑐(1 / 𝑁)) = (exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))))
1068a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ∈ ℂ)
107 neg1ne0 11070 . . . . . . . . . . . . . . 15 -1 ≠ 0
108107a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → -1 ≠ 0)
109 simpr 477 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ)
110106, 108, 80, 109cxpmul2zd 24362 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = ((-1↑𝑐(2 / 𝑁))↑𝑚))
111106, 108, 81cxpefd 24358 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1))))
112 logm1 24239 . . . . . . . . . . . . . . . 16 (log‘-1) = (i · π)
113112oveq2i 6615 . . . . . . . . . . . . . . 15 (((2 / 𝑁) · 𝑚) · (log‘-1)) = (((2 / 𝑁) · 𝑚) · (i · π))
114113fveq2i 6151 . . . . . . . . . . . . . 14 (exp‘(((2 / 𝑁) · 𝑚) · (log‘-1))) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))
115111, 114syl6eq 2671 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐((2 / 𝑁) · 𝑚)) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π))))
116106, 80cxpcld 24354 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
1178a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ∈ ℂ)
118107a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → -1 ≠ 0)
119117, 118, 13cxpne0d 24359 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ≠ 0)
120119ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (-1↑𝑐(2 / 𝑁)) ≠ 0)
121116, 120, 109expclzd 12953 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑚) ∈ ℂ)
12245adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℕ)
123109, 122zmodcld 12631 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℕ0)
124116, 123expcld 12948 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ∈ ℂ)
125123nn0zd 11424 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℤ)
126116, 120, 125expne0d 12954 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) ≠ 0)
127116, 120, 125, 109expsubd 12959 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
128122nnzd 11425 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℤ)
129 zre 11325 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℤ → 𝑚 ∈ ℝ)
130129adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℝ)
131122nnrpd 11814 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℝ+)
132 moddifz 12622 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)
133130, 131, 132syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)
134 expmulz 12846 . . . . . . . . . . . . . . . . 17 ((((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ (-1↑𝑐(2 / 𝑁)) ≠ 0) ∧ (𝑁 ∈ ℤ ∧ ((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ)) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
135116, 120, 128, 133, 134syl22anc 1324 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
136123nn0cnd 11297 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ ℂ)
13768, 136subcld 10336 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 − (𝑚 mod 𝑁)) ∈ ℂ)
138137, 72, 75divcan2d 10747 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (𝑚 − (𝑚 mod 𝑁)))
139138oveq2d 6620 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · ((𝑚 − (𝑚 mod 𝑁)) / 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))))
140 root1id 24395 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
141122, 140syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
142141oveq1d 6619 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)))
143 1exp 12829 . . . . . . . . . . . . . . . . . 18 (((𝑚 − (𝑚 mod 𝑁)) / 𝑁) ∈ ℤ → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
144133, 143syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (1↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
145142, 144eqtrd 2655 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑((𝑚 − (𝑚 mod 𝑁)) / 𝑁)) = 1)
146135, 139, 1453eqtr3d 2663 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 − (𝑚 mod 𝑁))) = 1)
147127, 146eqtr3d 2657 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝑚) / ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 1)
148121, 124, 126, 147diveq1d 10753 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑𝑚) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))
149110, 115, 1483eqtr3rd 2664 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)) = (exp‘(((2 / 𝑁) · 𝑚) · (i · π))))
150105, 149oveq12d 6622 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = ((exp‘((1 / 𝑁) · (log‘(𝐴𝑁)))) · (exp‘(((2 / 𝑁) · 𝑚) · (i · π)))))
15186, 102, 1503eqtr4d 2665 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
152 eflog 24227 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
15343, 44, 152syl2anc 692 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
154153adantr 481 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (exp‘(log‘𝐴)) = 𝐴)
155151, 154eqeq12d 2636 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → ((exp‘(((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) / 𝑁)) = (exp‘(log‘𝐴)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
156 zmodfz 12632 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)))
157109, 122, 156syl2anc 692 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℤ) → (𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)))
158 eqcom 2628 . . . . . . . . . . . . 13 (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴)
159 oveq2 6612 . . . . . . . . . . . . . . 15 (𝑛 = (𝑚 mod 𝑁) → ((-1↑𝑐(2 / 𝑁))↑𝑛) = ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁)))
160159oveq2d 6620 . . . . . . . . . . . . . 14 (𝑛 = (𝑚 mod 𝑁) → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))))
161160eqeq1d 2623 . . . . . . . . . . . . 13 (𝑛 = (𝑚 mod 𝑁) → ((((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = 𝐴 ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
162158, 161syl5bb 272 . . . . . . . . . . . 12 (𝑛 = (𝑚 mod 𝑁) → (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴))
163162rspcev 3295 . . . . . . . . . . 11 (((𝑚 mod 𝑁) ∈ (0...(𝑁 − 1)) ∧ (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑(𝑚 mod 𝑁))) = 𝐴) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
164163ex 450 . . . . . . . . . 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 3024 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (∃𝑚 ∈ ℤ (𝑁 · (log‘𝐴)) = ((log‘(𝐴𝑁)) + ((i · (2 · π)) · 𝑚)) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
17059, 169mpd 15 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
171 oveq1 6611 . . . . . . 7 ((𝐴𝑁) = 𝐵 → ((𝐴𝑁)↑𝑐(1 / 𝑁)) = (𝐵𝑐(1 / 𝑁)))
172171oveq1d 6619 . . . . . 6 ((𝐴𝑁) = 𝐵 → (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))
173172eqeq2d 2631 . . . . 5 ((𝐴𝑁) = 𝐵 → (𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ 𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
174173rexbidv 3045 . . . 4 ((𝐴𝑁) = 𝐵 → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = (((𝐴𝑁)↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
175170, 174syl5ibcom 235 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
17642, 175pm2.61dane 2877 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴𝑁) = 𝐵 → ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
177 simp3 1061 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
178 nnrecre 11001 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
1791783ad2ant2 1081 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 / 𝑁) ∈ ℝ)
180179recnd 10012 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (1 / 𝑁) ∈ ℂ)
181177, 180cxpcld 24354 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝐵𝑐(1 / 𝑁)) ∈ ℂ)
182181adantr 481 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵𝑐(1 / 𝑁)) ∈ ℂ)
183 elfznn0 12374 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
184 expcl 12818 . . . . . . 7 (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ)
18515, 183, 184syl2an 494 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑𝑛) ∈ ℂ)
18610adantr 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
187186nnnn0d 11295 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ0)
188182, 185, 187mulexpd 12963 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = (((𝐵𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁)))
189177adantr 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝐵 ∈ ℂ)
190 cxproot 24336 . . . . . . 7 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐵𝑐(1 / 𝑁))↑𝑁) = 𝐵)
191189, 186, 190syl2anc 692 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((𝐵𝑐(1 / 𝑁))↑𝑁) = 𝐵)
192183adantl 482 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℕ0)
193192nn0cnd 11297 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℂ)
194186nncnd 10980 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℂ)
195193, 194mulcomd 10005 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝑛 · 𝑁) = (𝑁 · 𝑛))
196195oveq2d 6620 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = ((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)))
19715adantr 481 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
198197, 187, 192expmuld 12951 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑛 · 𝑁)) = (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁))
199197, 192, 187expmuld 12951 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑(𝑁 · 𝑛)) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛))
200196, 198, 1993eqtr3d 2663 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛))
201186, 140syl 17 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
202201oveq1d 6619 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑁)↑𝑛) = (1↑𝑛))
203 elfzelz 12284 . . . . . . . . 9 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℤ)
204203adantl 482 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 𝑛 ∈ ℤ)
205 1exp 12829 . . . . . . . 8 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
206204, 205syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (1↑𝑛) = 1)
207200, 202, 2063eqtrd 2659 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁) = 1)
208191, 207oveq12d 6622 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁))↑𝑁) · (((-1↑𝑐(2 / 𝑁))↑𝑛)↑𝑁)) = (𝐵 · 1))
209189mulid1d 10001 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐵 · 1) = 𝐵)
210188, 208, 2093eqtrd 2659 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵)
211 oveq1 6611 . . . . 5 (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁))
212211eqeq1d 2623 . . . 4 (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → ((𝐴𝑁) = 𝐵 ↔ (((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))↑𝑁) = 𝐵))
213210, 212syl5ibrcom 237 . . 3 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (𝐴 = ((𝐵𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)) → (𝐴𝑁) = 𝐵))
214213rexlimdva 3024 . 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 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wrex 2908  cfv 5847  (class class class)co 6604  cc 9878  cr 9879  0cc0 9880  1c1 9881  ici 9882   + caddc 9883   · cmul 9885  cmin 10210  -cneg 10211   / cdiv 10628  cn 10964  2c2 11014  0cn0 11236  cz 11321  cuz 11631  +crp 11776  ...cfz 12268   mod cmo 12608  cexp 12800  expce 14717  πcpi 14722  logclog 24205  𝑐ccxp 24206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ioc 12122  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-fac 13001  df-bc 13030  df-hash 13058  df-shft 13741  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-limsup 14136  df-clim 14153  df-rlim 14154  df-sum 14351  df-ef 14723  df-sin 14725  df-cos 14726  df-pi 14728  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-fbas 19662  df-fg 19663  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-lp 20850  df-perf 20851  df-cn 20941  df-cnp 20942  df-haus 21029  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-xms 22035  df-ms 22036  df-tms 22037  df-cncf 22589  df-limc 23536  df-dv 23537  df-log 24207  df-cxp 24208
This theorem is referenced by:  1cubr  24469
  Copyright terms: Public domain W3C validator