| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12921 | . . 3
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12648 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ ℤ) | 
| 3 |  | ax-icn 11214 | . . . 4
⊢ i ∈
ℂ | 
| 4 |  | halfcl 12491 | . . . 4
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) | 
| 5 | 3, 4 | mp1i 13 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (i / 2) ∈ ℂ) | 
| 6 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐴 ∈
ℂ) | 
| 7 |  | mulcl 11239 | . . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 8 | 3, 6, 7 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (i · 𝐴)
∈ ℂ) | 
| 9 | 8 | negcld 11607 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ -(i · 𝐴)
∈ ℂ) | 
| 10 | 8 | absnegd 15488 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘-(i · 𝐴)) = (abs‘(i · 𝐴))) | 
| 11 |  | absmul 15333 | . . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (abs‘(i · 𝐴)) = ((abs‘i) ·
(abs‘𝐴))) | 
| 12 | 3, 6, 11 | sylancr 587 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(i · 𝐴)) = ((abs‘i) ·
(abs‘𝐴))) | 
| 13 |  | absi 15325 | . . . . . . . . . . 11
⊢
(abs‘i) = 1 | 
| 14 | 13 | oveq1i 7441 | . . . . . . . . . 10
⊢
((abs‘i) · (abs‘𝐴)) = (1 · (abs‘𝐴)) | 
| 15 |  | abscl 15317 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℝ) | 
| 17 | 16 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℂ) | 
| 18 | 17 | mullidd 11279 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 · (abs‘𝐴)) = (abs‘𝐴)) | 
| 19 | 14, 18 | eqtrid 2789 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘i) · (abs‘𝐴)) = (abs‘𝐴)) | 
| 20 | 10, 12, 19 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘-(i · 𝐴)) = (abs‘𝐴)) | 
| 21 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
1) | 
| 22 | 20, 21 | eqbrtrd 5165 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘-(i · 𝐴)) < 1) | 
| 23 |  | logtayl 26702 | . . . . . . 7
⊢ ((-(i
· 𝐴) ∈ ℂ
∧ (abs‘-(i · 𝐴)) < 1) → seq1( + , (𝑛 ∈ ℕ ↦ ((-(i
· 𝐴)↑𝑛) / 𝑛))) ⇝ -(log‘(1 − -(i
· 𝐴)))) | 
| 24 | 9, 22, 23 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛))) ⇝ -(log‘(1 − -(i
· 𝐴)))) | 
| 25 |  | ax-1cn 11213 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 26 |  | subneg 11558 | . . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − -(i
· 𝐴)) = (1 + (i
· 𝐴))) | 
| 27 | 25, 8, 26 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 − -(i · 𝐴)) = (1 + (i · 𝐴))) | 
| 28 | 27 | fveq2d 6910 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (log‘(1 − -(i · 𝐴))) = (log‘(1 + (i · 𝐴)))) | 
| 29 | 28 | negeqd 11502 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ -(log‘(1 − -(i · 𝐴))) = -(log‘(1 + (i · 𝐴)))) | 
| 30 | 24, 29 | breqtrd 5169 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛))) ⇝ -(log‘(1 + (i ·
𝐴)))) | 
| 31 |  | seqex 14044 | . . . . . 6
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))) ∈ V | 
| 32 | 31 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))) ∈ V) | 
| 33 | 10, 22 | eqbrtrrd 5167 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(i · 𝐴)) < 1) | 
| 34 |  | logtayl 26702 | . . . . . 6
⊢ (((i
· 𝐴) ∈ ℂ
∧ (abs‘(i · 𝐴)) < 1) → seq1( + , (𝑛 ∈ ℕ ↦ (((i
· 𝐴)↑𝑛) / 𝑛))) ⇝ -(log‘(1 − (i
· 𝐴)))) | 
| 35 | 8, 33, 34 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛))) ⇝ -(log‘(1 − (i
· 𝐴)))) | 
| 36 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (-(i · 𝐴)↑𝑛) = (-(i · 𝐴)↑𝑚)) | 
| 37 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → 𝑛 = 𝑚) | 
| 38 | 36, 37 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((-(i · 𝐴)↑𝑛) / 𝑛) = ((-(i · 𝐴)↑𝑚) / 𝑚)) | 
| 39 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ ((-(i
· 𝐴)↑𝑛) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛)) | 
| 40 |  | ovex 7464 | . . . . . . . . . 10
⊢ ((-(i
· 𝐴)↑𝑚) / 𝑚) ∈ V | 
| 41 | 38, 39, 40 | fvmpt 7016 | . . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((-(i
· 𝐴)↑𝑛) / 𝑛))‘𝑚) = ((-(i · 𝐴)↑𝑚) / 𝑚)) | 
| 42 | 41 | adantl 481 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
((-(i · 𝐴)↑𝑛) / 𝑛))‘𝑚) = ((-(i · 𝐴)↑𝑚) / 𝑚)) | 
| 43 |  | nnnn0 12533 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) | 
| 44 |  | expcl 14120 | . . . . . . . . . 10
⊢ ((-(i
· 𝐴) ∈ ℂ
∧ 𝑚 ∈
ℕ0) → (-(i · 𝐴)↑𝑚) ∈ ℂ) | 
| 45 | 9, 43, 44 | syl2an 596 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(-(i · 𝐴)↑𝑚) ∈
ℂ) | 
| 46 |  | nncn 12274 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) | 
| 47 | 46 | adantl 481 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
𝑚 ∈
ℂ) | 
| 48 |  | nnne0 12300 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0) | 
| 49 | 48 | adantl 481 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
𝑚 ≠ 0) | 
| 50 | 45, 47, 49 | divcld 12043 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((-(i · 𝐴)↑𝑚) / 𝑚) ∈ ℂ) | 
| 51 | 42, 50 | eqeltrd 2841 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
((-(i · 𝐴)↑𝑛) / 𝑛))‘𝑚) ∈ ℂ) | 
| 52 | 1, 2, 51 | serf 14071 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛))):ℕ⟶ℂ) | 
| 53 | 52 | ffvelcdmda 7104 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(seq1( + , (𝑛 ∈
ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛)))‘𝑘) ∈ ℂ) | 
| 54 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((i · 𝐴)↑𝑛) = ((i · 𝐴)↑𝑚)) | 
| 55 | 54, 37 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (((i · 𝐴)↑𝑛) / 𝑛) = (((i · 𝐴)↑𝑚) / 𝑚)) | 
| 56 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ (((i
· 𝐴)↑𝑛) / 𝑛)) = (𝑛 ∈ ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛)) | 
| 57 |  | ovex 7464 | . . . . . . . . . 10
⊢ (((i
· 𝐴)↑𝑚) / 𝑚) ∈ V | 
| 58 | 55, 56, 57 | fvmpt 7016 | . . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((i
· 𝐴)↑𝑛) / 𝑛))‘𝑚) = (((i · 𝐴)↑𝑚) / 𝑚)) | 
| 59 | 58 | adantl 481 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(((i · 𝐴)↑𝑛) / 𝑛))‘𝑚) = (((i · 𝐴)↑𝑚) / 𝑚)) | 
| 60 |  | expcl 14120 | . . . . . . . . . 10
⊢ (((i
· 𝐴) ∈ ℂ
∧ 𝑚 ∈
ℕ0) → ((i · 𝐴)↑𝑚) ∈ ℂ) | 
| 61 | 8, 43, 60 | syl2an 596 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((i · 𝐴)↑𝑚) ∈
ℂ) | 
| 62 | 61, 47, 49 | divcld 12043 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((i · 𝐴)↑𝑚) / 𝑚) ∈ ℂ) | 
| 63 | 59, 62 | eqeltrd 2841 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(((i · 𝐴)↑𝑛) / 𝑛))‘𝑚) ∈ ℂ) | 
| 64 | 1, 2, 63 | serf 14071 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛))):ℕ⟶ℂ) | 
| 65 | 64 | ffvelcdmda 7104 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(seq1( + , (𝑛 ∈
ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑘) ∈ ℂ) | 
| 66 |  | simpr 484 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ∈
ℕ) | 
| 67 | 66, 1 | eleqtrdi 2851 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ∈
(ℤ≥‘1)) | 
| 68 |  | simpl 482 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(𝐴 ∈ ℂ ∧
(abs‘𝐴) <
1)) | 
| 69 |  | elfznn 13593 | . . . . . . 7
⊢ (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ) | 
| 70 | 68, 69, 51 | syl2an 596 | . . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) ∧
𝑚 ∈ (1...𝑘)) → ((𝑛 ∈ ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛))‘𝑚) ∈ ℂ) | 
| 71 | 68, 69, 63 | syl2an 596 | . . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) ∧
𝑚 ∈ (1...𝑘)) → ((𝑛 ∈ ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛))‘𝑚) ∈ ℂ) | 
| 72 | 38, 55 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)) = (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚))) | 
| 73 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ (((-(i
· 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛))) = (𝑛 ∈ ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛))) | 
| 74 |  | ovex 7464 | . . . . . . . . . 10
⊢ (((-(i
· 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚)) ∈ V | 
| 75 | 72, 73, 74 | fvmpt 7016 | . . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((-(i
· 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚) = (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚))) | 
| 76 | 75 | adantl 481 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚) = (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚))) | 
| 77 | 42, 59 | oveq12d 7449 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((𝑛 ∈ ℕ ↦
((-(i · 𝐴)↑𝑛) / 𝑛))‘𝑚) − ((𝑛 ∈ ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛))‘𝑚)) = (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚))) | 
| 78 | 76, 77 | eqtr4d 2780 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚) = (((𝑛 ∈ ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛))‘𝑚) − ((𝑛 ∈ ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛))‘𝑚))) | 
| 79 | 68, 69, 78 | syl2an 596 | . . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) ∧
𝑚 ∈ (1...𝑘)) → ((𝑛 ∈ ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚) = (((𝑛 ∈ ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛))‘𝑚) − ((𝑛 ∈ ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛))‘𝑚))) | 
| 80 | 67, 70, 71, 79 | sersub 14086 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(seq1( + , (𝑛 ∈
ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛))))‘𝑘) = ((seq1( + , (𝑛 ∈ ℕ ↦ ((-(i · 𝐴)↑𝑛) / 𝑛)))‘𝑘) − (seq1( + , (𝑛 ∈ ℕ ↦ (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑘))) | 
| 81 | 1, 2, 30, 32, 35, 53, 65, 80 | climsub 15670 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))) ⇝ (-(log‘(1 + (i ·
𝐴))) − -(log‘(1
− (i · 𝐴))))) | 
| 82 |  | addcl 11237 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) | 
| 83 | 25, 8, 82 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 + (i · 𝐴))
∈ ℂ) | 
| 84 |  | bndatandm 26972 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐴 ∈ dom
arctan) | 
| 85 |  | atandm2 26920 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) | 
| 86 | 84, 85 | sylib 218 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴 ∈ ℂ
∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) | 
| 87 | 86 | simp3d 1145 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 + (i · 𝐴))
≠ 0) | 
| 88 | 83, 87 | logcld 26612 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (log‘(1 + (i · 𝐴))) ∈ ℂ) | 
| 89 |  | subcl 11507 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) | 
| 90 | 25, 8, 89 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 − (i · 𝐴)) ∈ ℂ) | 
| 91 | 86 | simp2d 1144 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 − (i · 𝐴)) ≠ 0) | 
| 92 | 90, 91 | logcld 26612 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (log‘(1 − (i · 𝐴))) ∈ ℂ) | 
| 93 | 88, 92 | neg2subd 11637 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (-(log‘(1 + (i · 𝐴))) − -(log‘(1 − (i
· 𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) | 
| 94 | 81, 93 | breqtrd 5169 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))) ⇝ ((log‘(1 − (i
· 𝐴))) −
(log‘(1 + (i · 𝐴))))) | 
| 95 | 50, 62 | subcld 11620 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚)) ∈ ℂ) | 
| 96 | 76, 95 | eqeltrd 2841 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚) ∈ ℂ) | 
| 97 | 3 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) → i
∈ ℂ) | 
| 98 |  | negicn 11509 | . . . . . . . . 9
⊢ -i ∈
ℂ | 
| 99 | 43 | adantl 481 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
𝑚 ∈
ℕ0) | 
| 100 |  | expcl 14120 | . . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝑚
∈ ℕ0) → (-i↑𝑚) ∈ ℂ) | 
| 101 | 98, 99, 100 | sylancr 587 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(-i↑𝑚) ∈
ℂ) | 
| 102 |  | expcl 14120 | . . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑚
∈ ℕ0) → (i↑𝑚) ∈ ℂ) | 
| 103 | 3, 99, 102 | sylancr 587 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(i↑𝑚) ∈
ℂ) | 
| 104 | 101, 103 | subcld 11620 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((-i↑𝑚) −
(i↑𝑚)) ∈
ℂ) | 
| 105 |  | 2cnd 12344 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) → 2
∈ ℂ) | 
| 106 |  | 2ne0 12370 | . . . . . . . 8
⊢ 2 ≠
0 | 
| 107 | 106 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) → 2
≠ 0) | 
| 108 | 97, 104, 105, 107 | div23d 12080 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((i · ((-i↑𝑚)
− (i↑𝑚))) / 2) =
((i / 2) · ((-i↑𝑚) − (i↑𝑚)))) | 
| 109 | 108 | oveq1d 7446 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((i · ((-i↑𝑚)
− (i↑𝑚))) / 2)
· ((𝐴↑𝑚) / 𝑚)) = (((i / 2) · ((-i↑𝑚) − (i↑𝑚))) · ((𝐴↑𝑚) / 𝑚))) | 
| 110 | 5 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) → (i
/ 2) ∈ ℂ) | 
| 111 |  | expcl 14120 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝐴↑𝑚) ∈
ℂ) | 
| 112 | 6, 43, 111 | syl2an 596 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(𝐴↑𝑚) ∈ ℂ) | 
| 113 | 112, 47, 49 | divcld 12043 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((𝐴↑𝑚) / 𝑚) ∈ ℂ) | 
| 114 | 110, 104,
113 | mulassd 11284 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((i / 2) · ((-i↑𝑚) − (i↑𝑚))) · ((𝐴↑𝑚) / 𝑚)) = ((i / 2) · (((-i↑𝑚) − (i↑𝑚)) · ((𝐴↑𝑚) / 𝑚)))) | 
| 115 | 101, 103,
112 | subdird 11720 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((-i↑𝑚) −
(i↑𝑚)) · (𝐴↑𝑚)) = (((-i↑𝑚) · (𝐴↑𝑚)) − ((i↑𝑚) · (𝐴↑𝑚)))) | 
| 116 | 6 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
𝐴 ∈
ℂ) | 
| 117 |  | mulneg1 11699 | . . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) = -(i · 𝐴)) | 
| 118 | 3, 116, 117 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(-i · 𝐴) = -(i
· 𝐴)) | 
| 119 | 118 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((-i · 𝐴)↑𝑚) = (-(i · 𝐴)↑𝑚)) | 
| 120 | 98 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) → -i
∈ ℂ) | 
| 121 | 120, 116,
99 | mulexpd 14201 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((-i · 𝐴)↑𝑚) = ((-i↑𝑚) · (𝐴↑𝑚))) | 
| 122 | 119, 121 | eqtr3d 2779 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(-(i · 𝐴)↑𝑚) = ((-i↑𝑚) · (𝐴↑𝑚))) | 
| 123 | 97, 116, 99 | mulexpd 14201 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((i · 𝐴)↑𝑚) = ((i↑𝑚) · (𝐴↑𝑚))) | 
| 124 | 122, 123 | oveq12d 7449 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((-(i · 𝐴)↑𝑚) − ((i · 𝐴)↑𝑚)) = (((-i↑𝑚) · (𝐴↑𝑚)) − ((i↑𝑚) · (𝐴↑𝑚)))) | 
| 125 | 115, 124 | eqtr4d 2780 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((-i↑𝑚) −
(i↑𝑚)) · (𝐴↑𝑚)) = ((-(i · 𝐴)↑𝑚) − ((i · 𝐴)↑𝑚))) | 
| 126 | 125 | oveq1d 7446 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((((-i↑𝑚) −
(i↑𝑚)) · (𝐴↑𝑚)) / 𝑚) = (((-(i · 𝐴)↑𝑚) − ((i · 𝐴)↑𝑚)) / 𝑚)) | 
| 127 | 104, 112,
47, 49 | divassd 12078 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((((-i↑𝑚) −
(i↑𝑚)) · (𝐴↑𝑚)) / 𝑚) = (((-i↑𝑚) − (i↑𝑚)) · ((𝐴↑𝑚) / 𝑚))) | 
| 128 | 45, 61, 47, 49 | divsubdird 12082 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((-(i · 𝐴)↑𝑚) − ((i · 𝐴)↑𝑚)) / 𝑚) = (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚))) | 
| 129 | 126, 127,
128 | 3eqtr3d 2785 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((-i↑𝑚) −
(i↑𝑚)) ·
((𝐴↑𝑚) / 𝑚)) = (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚))) | 
| 130 | 129 | oveq2d 7447 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((i / 2) · (((-i↑𝑚) − (i↑𝑚)) · ((𝐴↑𝑚) / 𝑚))) = ((i / 2) · (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚)))) | 
| 131 | 109, 114,
130 | 3eqtrd 2781 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(((i · ((-i↑𝑚)
− (i↑𝑚))) / 2)
· ((𝐴↑𝑚) / 𝑚)) = ((i / 2) · (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚)))) | 
| 132 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (-i↑𝑛) = (-i↑𝑚)) | 
| 133 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (i↑𝑛) = (i↑𝑚)) | 
| 134 | 132, 133 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑛 = 𝑚 → ((-i↑𝑛) − (i↑𝑛)) = ((-i↑𝑚) − (i↑𝑚))) | 
| 135 | 134 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → (i · ((-i↑𝑛) − (i↑𝑛))) = (i ·
((-i↑𝑚) −
(i↑𝑚)))) | 
| 136 | 135 | oveq1d 7446 | . . . . . . 7
⊢ (𝑛 = 𝑚 → ((i · ((-i↑𝑛) − (i↑𝑛))) / 2) = ((i ·
((-i↑𝑚) −
(i↑𝑚))) /
2)) | 
| 137 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝐴↑𝑛) = (𝐴↑𝑚)) | 
| 138 | 137, 37 | oveq12d 7449 | . . . . . . 7
⊢ (𝑛 = 𝑚 → ((𝐴↑𝑛) / 𝑛) = ((𝐴↑𝑚) / 𝑚)) | 
| 139 | 136, 138 | oveq12d 7449 | . . . . . 6
⊢ (𝑛 = 𝑚 → (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛)) = (((i · ((-i↑𝑚) − (i↑𝑚))) / 2) · ((𝐴↑𝑚) / 𝑚))) | 
| 140 |  | atantayl.1 | . . . . . 6
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i ·
((-i↑𝑛) −
(i↑𝑛))) / 2) ·
((𝐴↑𝑛) / 𝑛))) | 
| 141 |  | ovex 7464 | . . . . . 6
⊢ (((i
· ((-i↑𝑚)
− (i↑𝑚))) / 2)
· ((𝐴↑𝑚) / 𝑚)) ∈ V | 
| 142 | 139, 140,
141 | fvmpt 7016 | . . . . 5
⊢ (𝑚 ∈ ℕ → (𝐹‘𝑚) = (((i · ((-i↑𝑚) − (i↑𝑚))) / 2) · ((𝐴↑𝑚) / 𝑚))) | 
| 143 | 142 | adantl 481 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(𝐹‘𝑚) = (((i · ((-i↑𝑚) − (i↑𝑚))) / 2) · ((𝐴↑𝑚) / 𝑚))) | 
| 144 | 76 | oveq2d 7447 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
((i / 2) · ((𝑛
∈ ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚)) = ((i / 2) · (((-(i · 𝐴)↑𝑚) / 𝑚) − (((i · 𝐴)↑𝑚) / 𝑚)))) | 
| 145 | 131, 143,
144 | 3eqtr4d 2787 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑚 ∈ ℕ) →
(𝐹‘𝑚) = ((i / 2) · ((𝑛 ∈ ℕ ↦ (((-(i · 𝐴)↑𝑛) / 𝑛) − (((i · 𝐴)↑𝑛) / 𝑛)))‘𝑚))) | 
| 146 | 1, 2, 5, 94, 96, 145 | isermulc2 15694 | . 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , 𝐹) ⇝
((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) | 
| 147 |  | atanval 26927 | . . 3
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) | 
| 148 | 84, 147 | syl 17 | . 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (arctan‘𝐴) =
((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) | 
| 149 | 146, 148 | breqtrrd 5171 | 1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , 𝐹) ⇝
(arctan‘𝐴)) |