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 ‘ 𝐴 ) )