This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atantayl

Description: The Taylor series for arctan ( A ) . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Hypothesis atantayl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( i · ( ( - i ↑ 𝑛 ) − ( i ↑ 𝑛 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) )
Assertion atantayl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , 𝐹 ) ⇝ ( arctan ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 atantayl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( i · ( ( - i ↑ 𝑛 ) − ( i ↑ 𝑛 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) )
2 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
3 1zzd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℤ )
4 ax-icn ⊢ i ∈ ℂ
5 halfcl ⊢ ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
6 4 5 mp1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( i / 2 ) ∈ ℂ )
7 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
8 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
9 4 7 8 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( i · 𝐴 ) ∈ ℂ )
10 9 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → - ( i · 𝐴 ) ∈ ℂ )
11 9 absnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ - ( i · 𝐴 ) ) = ( abs ‘ ( i · 𝐴 ) ) )
12 absmul ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( i · 𝐴 ) ) = ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) )
13 4 7 12 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( i · 𝐴 ) ) = ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) )
14 absi ⊢ ( abs ‘ i ) = 1
15 14 oveq1i ⊢ ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) = ( 1 · ( abs ‘ 𝐴 ) )
16 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
18 17 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
19 18 mullidd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 · ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
20 15 19 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
21 11 13 20 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ - ( i · 𝐴 ) ) = ( abs ‘ 𝐴 ) )
22 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
23 21 22 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ - ( i · 𝐴 ) ) < 1 )
24 logtayl ⊢ ( ( - ( i · 𝐴 ) ∈ ℂ ∧ ( abs ‘ - ( i · 𝐴 ) ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ⇝ - ( log ‘ ( 1 − - ( i · 𝐴 ) ) ) )
25 10 23 24 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ⇝ - ( log ‘ ( 1 − - ( i · 𝐴 ) ) ) )
26 ax-1cn ⊢ 1 ∈ ℂ
27 subneg ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
28 26 9 27 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
29 28 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( log ‘ ( 1 − - ( i · 𝐴 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
30 29 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → - ( log ‘ ( 1 − - ( i · 𝐴 ) ) ) = - ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
31 25 30 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ⇝ - ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
32 seqex ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ) ∈ V
33 32 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ) ∈ V )
34 11 23 eqbrtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( i · 𝐴 ) ) < 1 )
35 logtayl ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( abs ‘ ( i · 𝐴 ) ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ⇝ - ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
36 9 34 35 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ⇝ - ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
37 oveq2 ⊢ ( 𝑛 = 𝑚 → ( - ( i · 𝐴 ) ↑ 𝑛 ) = ( - ( i · 𝐴 ) ↑ 𝑚 ) )
38 id ⊢ ( 𝑛 = 𝑚 → 𝑛 = 𝑚 )
39 37 38 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) = ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) )
40 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
41 ovex ⊢ ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ∈ V
42 39 40 41 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) )
43 42 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) )
44 nnnn0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
45 expcl ⊢ ( ( - ( i · 𝐴 ) ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( - ( i · 𝐴 ) ↑ 𝑚 ) ∈ ℂ )
46 10 44 45 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( - ( i · 𝐴 ) ↑ 𝑚 ) ∈ ℂ )
47 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
48 47 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
49 nnne0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
50 49 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
51 46 48 50 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ∈ ℂ )
52 43 51 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ∈ ℂ )
53 2 3 52 serf ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) : ℕ ⟶ ℂ )
54 53 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
55 oveq2 ⊢ ( 𝑛 = 𝑚 → ( ( i · 𝐴 ) ↑ 𝑛 ) = ( ( i · 𝐴 ) ↑ 𝑚 ) )
56 55 38 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) = ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) )
57 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
58 ovex ⊢ ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ∈ V
59 56 57 58 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) )
60 59 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) )
61 expcl ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 𝑚 ) ∈ ℂ )
62 9 44 61 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( i · 𝐴 ) ↑ 𝑚 ) ∈ ℂ )
63 62 48 50 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ∈ ℂ )
64 60 63 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ∈ ℂ )
65 2 3 64 serf ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) : ℕ ⟶ ℂ )
66 65 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
67 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
68 67 2 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
69 simpl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) )
70 elfznn ⊢ ( 𝑚 ∈ ( 1 ... 𝑘 ) → 𝑚 ∈ ℕ )
71 69 70 52 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ∈ ℂ )
72 69 70 64 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ∈ ℂ )
73 39 56 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) )
74 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) )
75 ovex ⊢ ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) ∈ V
76 73 74 75 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) )
77 76 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) )
78 43 60 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) )
79 77 78 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ) )
80 69 70 79 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑚 ) ) )
81 68 71 72 80 sersub ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ) ‘ 𝑘 ) = ( ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑘 ) − ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑘 ) ) )
82 2 3 31 33 36 54 66 81 climsub ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ) ⇝ ( - ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − - ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
83 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
84 26 9 83 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
85 bndatandm ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ dom arctan )
86 atandm2 ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
87 85 86 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
88 87 simp3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
89 84 88 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
90 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
91 26 9 90 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
92 87 simp2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
93 91 92 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
94 89 93 neg2subd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( - ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − - ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
95 82 94 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ) ⇝ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
96 51 63 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) ∈ ℂ )
97 77 96 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) ∈ ℂ )
98 4 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → i ∈ ℂ )
99 negicn ⊢ - i ∈ ℂ
100 44 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ0 )
101 expcl ⊢ ( ( - i ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( - i ↑ 𝑚 ) ∈ ℂ )
102 99 100 101 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( - i ↑ 𝑚 ) ∈ ℂ )
103 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( i ↑ 𝑚 ) ∈ ℂ )
104 4 100 103 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( i ↑ 𝑚 ) ∈ ℂ )
105 102 104 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ∈ ℂ )
106 2cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → 2 ∈ ℂ )
107 2ne0 ⊢ 2 ≠ 0
108 107 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → 2 ≠ 0 )
109 98 105 106 108 div23d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) = ( ( i / 2 ) · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) )
110 109 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) = ( ( ( i / 2 ) · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) )
111 6 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( i / 2 ) ∈ ℂ )
112 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑚 ) ∈ ℂ )
113 7 44 112 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( 𝐴 ↑ 𝑚 ) ∈ ℂ )
114 113 48 50 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ∈ ℂ )
115 111 105 114 mulassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( i / 2 ) · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) = ( ( i / 2 ) · ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) ) )
116 102 104 113 subdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( 𝐴 ↑ 𝑚 ) ) = ( ( ( - i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) − ( ( i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) ) )
117 7 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ℂ )
118 mulneg1 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = - ( i · 𝐴 ) )
119 4 117 118 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( - i · 𝐴 ) = - ( i · 𝐴 ) )
120 119 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( - i · 𝐴 ) ↑ 𝑚 ) = ( - ( i · 𝐴 ) ↑ 𝑚 ) )
121 99 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → - i ∈ ℂ )
122 121 117 100 mulexpd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( - i · 𝐴 ) ↑ 𝑚 ) = ( ( - i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) )
123 120 122 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( - ( i · 𝐴 ) ↑ 𝑚 ) = ( ( - i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) )
124 98 117 100 mulexpd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( i · 𝐴 ) ↑ 𝑚 ) = ( ( i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) )
125 123 124 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( - ( i · 𝐴 ) ↑ 𝑚 ) − ( ( i · 𝐴 ) ↑ 𝑚 ) ) = ( ( ( - i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) − ( ( i ↑ 𝑚 ) · ( 𝐴 ↑ 𝑚 ) ) ) )
126 116 125 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( 𝐴 ↑ 𝑚 ) ) = ( ( - ( i · 𝐴 ) ↑ 𝑚 ) − ( ( i · 𝐴 ) ↑ 𝑚 ) ) )
127 126 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( 𝐴 ↑ 𝑚 ) ) / 𝑚 ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) − ( ( i · 𝐴 ) ↑ 𝑚 ) ) / 𝑚 ) )
128 105 113 48 50 divassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( 𝐴 ↑ 𝑚 ) ) / 𝑚 ) = ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) )
129 46 62 48 50 divsubdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) − ( ( i · 𝐴 ) ↑ 𝑚 ) ) / 𝑚 ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) )
130 127 128 129 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) = ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) )
131 130 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( i / 2 ) · ( ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) ) = ( ( i / 2 ) · ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) ) )
132 110 115 131 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) = ( ( i / 2 ) · ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) ) )
133 oveq2 ⊢ ( 𝑛 = 𝑚 → ( - i ↑ 𝑛 ) = ( - i ↑ 𝑚 ) )
134 oveq2 ⊢ ( 𝑛 = 𝑚 → ( i ↑ 𝑛 ) = ( i ↑ 𝑚 ) )
135 133 134 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( - i ↑ 𝑛 ) − ( i ↑ 𝑛 ) ) = ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) )
136 135 oveq2d ⊢ ( 𝑛 = 𝑚 → ( i · ( ( - i ↑ 𝑛 ) − ( i ↑ 𝑛 ) ) ) = ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) )
137 136 oveq1d ⊢ ( 𝑛 = 𝑚 → ( ( i · ( ( - i ↑ 𝑛 ) − ( i ↑ 𝑛 ) ) ) / 2 ) = ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) )
138 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑚 ) )
139 138 38 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) = ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) )
140 137 139 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( i · ( ( - i ↑ 𝑛 ) − ( i ↑ 𝑛 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) = ( ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) )
141 ovex ⊢ ( ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) ∈ V
142 140 1 141 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( 𝐹 ‘ 𝑚 ) = ( ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) )
143 142 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) = ( ( ( i · ( ( - i ↑ 𝑚 ) − ( i ↑ 𝑚 ) ) ) / 2 ) · ( ( 𝐴 ↑ 𝑚 ) / 𝑚 ) ) )
144 77 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( ( i / 2 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) ) = ( ( i / 2 ) · ( ( ( - ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) − ( ( ( i · 𝐴 ) ↑ 𝑚 ) / 𝑚 ) ) ) )
145 132 143 144 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) = ( ( i / 2 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( - ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) − ( ( ( i · 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) ) ‘ 𝑚 ) ) )
146 2 3 6 95 97 145 isermulc2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , 𝐹 ) ⇝ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
147 atanval ⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
148 85 147 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
149 146 148 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , 𝐹 ) ⇝ ( arctan ‘ 𝐴 ) )