Theorem log2cnv

Description: Using the Taylor series for arctan ( _i / 3 ) , produce a rapidly convergent series for log 2 . (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypothesis	log2cnv.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{2}{3\left(2n+1\right)9^n}\right)$$
Assertion	log2cnv	$$⊢seq0\left(+,F\right)⇝\log 2$$

Proof

Step	Hyp	Ref	Expression
1		log2cnv.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{2}{3\left(2n+1\right)9^n}\right)$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3		0zd	$$⊢\top \to 0\in \mathbb{Z}$$
4		2cn	$$⊢2\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6		ine0	$$⊢\mathrm{i}\ne 0$$
7	4 5 6	divcli	$$⊢\frac{2}{\mathrm{i}}\in ℂ$$
8	7	a1i	$$⊢\top \to \frac{2}{\mathrm{i}}\in ℂ$$
9		3cn	$$⊢3\in ℂ$$
10		3ne0	$$⊢3\ne 0$$
11	5 9 10	divcli	$$⊢\frac{\mathrm{i}}{3}\in ℂ$$
12		absdiv	$$⊢\left(\mathrm{i}\in ℂ\wedge 3\in ℂ\wedge 3\ne 0\right)\to \left|\frac{\mathrm{i}}{3}\right|=\frac{\left|\mathrm{i}\right|}{\left|3\right|}$$
13	5 9 10 12	mp3an	$$⊢\left|\frac{\mathrm{i}}{3}\right|=\frac{\left|\mathrm{i}\right|}{\left|3\right|}$$
14		absi	$$⊢\left|\mathrm{i}\right|=1$$
15		3re	$$⊢3\in ℝ$$
16		0re	$$⊢0\in ℝ$$
17		3pos	$$⊢0<3$$
18	16 15 17	ltleii	$$⊢0\le 3$$
19		absid	$$⊢\left(3\in ℝ\wedge 0\le 3\right)\to \left|3\right|=3$$
20	15 18 19	mp2an	$$⊢\left|3\right|=3$$
21	14 20	oveq12i	$$⊢\frac{\left|\mathrm{i}\right|}{\left|3\right|}=\frac{1}{3}$$
22	13 21	eqtri	$$⊢\left|\frac{\mathrm{i}}{3}\right|=\frac{1}{3}$$
23		1lt3	$$⊢1<3$$
24		recgt1	$$⊢\left(3\in ℝ\wedge 0<3\right)\to \left(1<3\leftrightarrow \frac{1}{3}<1\right)$$
25	15 17 24	mp2an	$$⊢1<3\leftrightarrow \frac{1}{3}<1$$
26	23 25	mpbi	$$⊢\frac{1}{3}<1$$
27	22 26	eqbrtri	$$⊢\left|\frac{\mathrm{i}}{3}\right|<1$$
28		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)=\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)$$
29	28	atantayl3	$$⊢\left(\frac{\mathrm{i}}{3}\in ℂ\wedge \left|\frac{\mathrm{i}}{3}\right|<1\right)\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\right)⇝arctan\left(\frac{\mathrm{i}}{3}\right)$$
30	11 27 29	mp2an	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\right)⇝arctan\left(\frac{\mathrm{i}}{3}\right)$$
31	30	a1i	$$⊢\top \to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\right)⇝arctan\left(\frac{\mathrm{i}}{3}\right)$$
32		oveq2	$$⊢n=k\to {\left(-1\right)}^n={\left(-1\right)}^k$$
33		oveq2	$$⊢n=k\to 2n=2k$$
34	33	oveq1d	$$⊢n=k\to 2n+1=2k+1$$
35	34	oveq2d	$$⊢n=k\to {\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}={\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}$$
36	35 34	oveq12d	$$⊢n=k\to \frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}=\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}$$
37	32 36	oveq12d	$$⊢n=k\to {\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)={\left(-1\right)}^k\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}\right)$$
38		ovex	$$⊢{\left(-1\right)}^k\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}\right)\in \mathrm{V}$$
39	37 28 38	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)={\left(-1\right)}^k\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}\right)$$
40	5	a1i	$$⊢k\in {\mathbb{N}}_0\to \mathrm{i}\in ℂ$$
41	9	a1i	$$⊢k\in {\mathbb{N}}_0\to 3\in ℂ$$
42	10	a1i	$$⊢k\in {\mathbb{N}}_0\to 3\ne 0$$
43		2nn0	$$⊢2\in {\mathbb{N}}_0$$
44		nn0mulcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to 2k\in {\mathbb{N}}_0$$
45	43 44	mpan	$$⊢k\in {\mathbb{N}}_0\to 2k\in {\mathbb{N}}_0$$
46		peano2nn0	$$⊢2k\in {\mathbb{N}}_0\to 2k+1\in {\mathbb{N}}_0$$
47	45 46	syl	$$⊢k\in {\mathbb{N}}_0\to 2k+1\in {\mathbb{N}}_0$$
48	40 41 42 47	expdivd	$$⊢k\in {\mathbb{N}}_0\to {\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}=\frac{{\mathrm{i}}^{2k+1}}{3^{2k+1}}$$
49	48	oveq2d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}={\left(-1\right)}^k\left(\frac{{\mathrm{i}}^{2k+1}}{3^{2k+1}}\right)$$
50		neg1cn	$$⊢-1\in ℂ$$
51		expcl	$$⊢\left(-1\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\left(-1\right)}^k\in ℂ$$
52	50 51	mpan	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k\in ℂ$$
53		expcl	$$⊢\left(\mathrm{i}\in ℂ\wedge 2k+1\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^{2k+1}\in ℂ$$
54	5 47 53	sylancr	$$⊢k\in {\mathbb{N}}_0\to {\mathrm{i}}^{2k+1}\in ℂ$$
55		3nn	$$⊢3\in \mathbb{N}$$
56		nnexpcl	$$⊢\left(3\in \mathbb{N}\wedge 2k+1\in {\mathbb{N}}_0\right)\to 3^{2k+1}\in \mathbb{N}$$
57	55 47 56	sylancr	$$⊢k\in {\mathbb{N}}_0\to 3^{2k+1}\in \mathbb{N}$$
58	57	nncnd	$$⊢k\in {\mathbb{N}}_0\to 3^{2k+1}\in ℂ$$
59	57	nnne0d	$$⊢k\in {\mathbb{N}}_0\to 3^{2k+1}\ne 0$$
60	52 54 58 59	divassd	$$⊢k\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^k{\mathrm{i}}^{2k+1}}{3^{2k+1}}={\left(-1\right)}^k\left(\frac{{\mathrm{i}}^{2k+1}}{3^{2k+1}}\right)$$
61		expp1	$$⊢\left(\mathrm{i}\in ℂ\wedge 2k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^{2k+1}={\mathrm{i}}^{2k}\mathrm{i}$$
62	5 45 61	sylancr	$$⊢k\in {\mathbb{N}}_0\to {\mathrm{i}}^{2k+1}={\mathrm{i}}^{2k}\mathrm{i}$$
63		expmul	$$⊢\left(\mathrm{i}\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^{2k}={\left({\mathrm{i}}^2\right)}^k$$
64	5 43 63	mp3an12	$$⊢k\in {\mathbb{N}}_0\to {\mathrm{i}}^{2k}={\left({\mathrm{i}}^2\right)}^k$$
65		i2	$$⊢{\mathrm{i}}^2=-1$$
66	65	oveq1i	$$⊢{\left({\mathrm{i}}^2\right)}^k={\left(-1\right)}^k$$
67	64 66	eqtrdi	$$⊢k\in {\mathbb{N}}_0\to {\mathrm{i}}^{2k}={\left(-1\right)}^k$$
68	67	oveq1d	$$⊢k\in {\mathbb{N}}_0\to {\mathrm{i}}^{2k}\mathrm{i}={\left(-1\right)}^k\mathrm{i}$$
69	62 68	eqtrd	$$⊢k\in {\mathbb{N}}_0\to {\mathrm{i}}^{2k+1}={\left(-1\right)}^k\mathrm{i}$$
70	69	oveq2d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\mathrm{i}}^{2k+1}={\left(-1\right)}^k{\left(-1\right)}^k\mathrm{i}$$
71	52 52 40	mulassd	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(-1\right)}^k\mathrm{i}={\left(-1\right)}^k{\left(-1\right)}^k\mathrm{i}$$
72	50	a1i	$$⊢k\in {\mathbb{N}}_0\to -1\in ℂ$$
73		id	$$⊢k\in {\mathbb{N}}_0\to k\in {\mathbb{N}}_0$$
74	72 73 73	expaddd	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^{k+k}={\left(-1\right)}^k{\left(-1\right)}^k$$
75		expmul	$$⊢\left(-1\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to {\left(-1\right)}^{2k}={\left({-1}^2\right)}^k$$
76	50 43 75	mp3an12	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^{2k}={\left({-1}^2\right)}^k$$
77		neg1sqe1	$$⊢{\left(-1\right)}^2=1$$
78	77	oveq1i	$$⊢{\left({-1}^2\right)}^k=1^k$$
79	76 78	eqtrdi	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^{2k}=1^k$$
80		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
81	80	2timesd	$$⊢k\in {\mathbb{N}}_0\to 2k=k+k$$
82	81	oveq2d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^{2k}={\left(-1\right)}^{k+k}$$
83		nn0z	$$⊢k\in {\mathbb{N}}_0\to k\in \mathbb{Z}$$
84		1exp	$$⊢k\in \mathbb{Z}\to 1^k=1$$
85	83 84	syl	$$⊢k\in {\mathbb{N}}_0\to 1^k=1$$
86	79 82 85	3eqtr3d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^{k+k}=1$$
87	74 86	eqtr3d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(-1\right)}^k=1$$
88	87	oveq1d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(-1\right)}^k\mathrm{i}=1\mathrm{i}$$
89	5	mullidi	$$⊢1\mathrm{i}=\mathrm{i}$$
90	88 89	eqtrdi	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(-1\right)}^k\mathrm{i}=\mathrm{i}$$
91	70 71 90	3eqtr2d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\mathrm{i}}^{2k+1}=\mathrm{i}$$
92	91	oveq1d	$$⊢k\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^k{\mathrm{i}}^{2k+1}}{3^{2k+1}}=\frac{\mathrm{i}}{3^{2k+1}}$$
93	49 60 92	3eqtr2d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}=\frac{\mathrm{i}}{3^{2k+1}}$$
94	93	oveq1d	$$⊢k\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^k{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}=\frac{\frac{\mathrm{i}}{3^{2k+1}}}{2k+1}$$
95		expcl	$$⊢\left(\frac{\mathrm{i}}{3}\in ℂ\wedge 2k+1\in {\mathbb{N}}_0\right)\to {\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}\in ℂ$$
96	11 47 95	sylancr	$$⊢k\in {\mathbb{N}}_0\to {\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}\in ℂ$$
97		nn0p1nn	$$⊢2k\in {\mathbb{N}}_0\to 2k+1\in \mathbb{N}$$
98	45 97	syl	$$⊢k\in {\mathbb{N}}_0\to 2k+1\in \mathbb{N}$$
99	98	nncnd	$$⊢k\in {\mathbb{N}}_0\to 2k+1\in ℂ$$
100	98	nnne0d	$$⊢k\in {\mathbb{N}}_0\to 2k+1\ne 0$$
101	52 96 99 100	divassd	$$⊢k\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^k{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}={\left(-1\right)}^k\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}\right)$$
102	40 58 99 59 100	divdiv1d	$$⊢k\in {\mathbb{N}}_0\to \frac{\frac{\mathrm{i}}{3^{2k+1}}}{2k+1}=\frac{\mathrm{i}}{3^{2k+1}\left(2k+1\right)}$$
103	94 101 102	3eqtr3d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}\right)=\frac{\mathrm{i}}{3^{2k+1}\left(2k+1\right)}$$
104	58 99	mulcomd	$$⊢k\in {\mathbb{N}}_0\to 3^{2k+1}\left(2k+1\right)=\left(2k+1\right)3^{2k+1}$$
105	104	oveq2d	$$⊢k\in {\mathbb{N}}_0\to \frac{\mathrm{i}}{3^{2k+1}\left(2k+1\right)}=\frac{\mathrm{i}}{\left(2k+1\right)3^{2k+1}}$$
106	39 103 105	3eqtrd	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)=\frac{\mathrm{i}}{\left(2k+1\right)3^{2k+1}}$$
107	98 57	nnmulcld	$$⊢k\in {\mathbb{N}}_0\to \left(2k+1\right)3^{2k+1}\in \mathbb{N}$$
108	107	nncnd	$$⊢k\in {\mathbb{N}}_0\to \left(2k+1\right)3^{2k+1}\in ℂ$$
109	107	nnne0d	$$⊢k\in {\mathbb{N}}_0\to \left(2k+1\right)3^{2k+1}\ne 0$$
110	40 108 109	divcld	$$⊢k\in {\mathbb{N}}_0\to \frac{\mathrm{i}}{\left(2k+1\right)3^{2k+1}}\in ℂ$$
111	106 110	eqeltrd	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)\in ℂ$$
112	111	adantl	$$⊢\left(\top \wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)\in ℂ$$
113	34	oveq2d	$$⊢n=k\to 3\left(2n+1\right)=3\left(2k+1\right)$$
114		oveq2	$$⊢n=k\to 9^n=9^k$$
115	113 114	oveq12d	$$⊢n=k\to 3\left(2n+1\right)9^n=3\left(2k+1\right)9^k$$
116	115	oveq2d	$$⊢n=k\to \frac{2}{3\left(2n+1\right)9^n}=\frac{2}{3\left(2k+1\right)9^k}$$
117		ovex	$$⊢\frac{2}{3\left(2k+1\right)9^k}\in \mathrm{V}$$
118	116 1 117	fvmpt	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{2}{3\left(2k+1\right)9^k}$$
119		expp1	$$⊢\left(3\in ℂ\wedge 2k\in {\mathbb{N}}_0\right)\to 3^{2k+1}=3^{2k}\cdot 3$$
120	9 45 119	sylancr	$$⊢k\in {\mathbb{N}}_0\to 3^{2k+1}=3^{2k}\cdot 3$$
121		expmul	$$⊢\left(3\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to 3^{2k}={\left(3^2\right)}^k$$
122	9 43 121	mp3an12	$$⊢k\in {\mathbb{N}}_0\to 3^{2k}={\left(3^2\right)}^k$$
123		sq3	$$⊢3^2=9$$
124	123	oveq1i	$$⊢{\left(3^2\right)}^k=9^k$$
125	122 124	eqtrdi	$$⊢k\in {\mathbb{N}}_0\to 3^{2k}=9^k$$
126	125	oveq1d	$$⊢k\in {\mathbb{N}}_0\to 3^{2k}\cdot 3=9^k\cdot 3$$
127		9nn	$$⊢9\in \mathbb{N}$$
128		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge k\in {\mathbb{N}}_0\right)\to 9^k\in \mathbb{N}$$
129	127 128	mpan	$$⊢k\in {\mathbb{N}}_0\to 9^k\in \mathbb{N}$$
130	129	nncnd	$$⊢k\in {\mathbb{N}}_0\to 9^k\in ℂ$$
131		mulcom	$$⊢\left(9^k\in ℂ\wedge 3\in ℂ\right)\to 9^k\cdot 3=39^k$$
132	130 9 131	sylancl	$$⊢k\in {\mathbb{N}}_0\to 9^k\cdot 3=39^k$$
133	120 126 132	3eqtrd	$$⊢k\in {\mathbb{N}}_0\to 3^{2k+1}=39^k$$
134	91 133	oveq12d	$$⊢k\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^k{\mathrm{i}}^{2k+1}}{3^{2k+1}}=\frac{\mathrm{i}}{39^k}$$
135	49 60 134	3eqtr2d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}=\frac{\mathrm{i}}{39^k}$$
136	135	oveq1d	$$⊢k\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^k{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}=\frac{\frac{\mathrm{i}}{39^k}}{2k+1}$$
137		nnmulcl	$$⊢\left(3\in \mathbb{N}\wedge 9^k\in \mathbb{N}\right)\to 39^k\in \mathbb{N}$$
138	55 129 137	sylancr	$$⊢k\in {\mathbb{N}}_0\to 39^k\in \mathbb{N}$$
139	138	nncnd	$$⊢k\in {\mathbb{N}}_0\to 39^k\in ℂ$$
140	138	nnne0d	$$⊢k\in {\mathbb{N}}_0\to 39^k\ne 0$$
141	40 139 99 140 100	divdiv1d	$$⊢k\in {\mathbb{N}}_0\to \frac{\frac{\mathrm{i}}{39^k}}{2k+1}=\frac{\mathrm{i}}{39^k\left(2k+1\right)}$$
142	136 101 141	3eqtr3d	$$⊢k\in {\mathbb{N}}_0\to {\left(-1\right)}^k\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2k+1}}{2k+1}\right)=\frac{\mathrm{i}}{39^k\left(2k+1\right)}$$
143	41 130 99	mul32d	$$⊢k\in {\mathbb{N}}_0\to 39^k\left(2k+1\right)=3\left(2k+1\right)9^k$$
144	143	oveq2d	$$⊢k\in {\mathbb{N}}_0\to \frac{\mathrm{i}}{39^k\left(2k+1\right)}=\frac{\mathrm{i}}{3\left(2k+1\right)9^k}$$
145	39 142 144	3eqtrd	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)=\frac{\mathrm{i}}{3\left(2k+1\right)9^k}$$
146	145	oveq2d	$$⊢k\in {\mathbb{N}}_0\to \left(\frac{2}{\mathrm{i}}\right)\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)=\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\right)$$
147		nnmulcl	$$⊢\left(3\in \mathbb{N}\wedge 2k+1\in \mathbb{N}\right)\to 3\left(2k+1\right)\in \mathbb{N}$$
148	55 98 147	sylancr	$$⊢k\in {\mathbb{N}}_0\to 3\left(2k+1\right)\in \mathbb{N}$$
149	148 129	nnmulcld	$$⊢k\in {\mathbb{N}}_0\to 3\left(2k+1\right)9^k\in \mathbb{N}$$
150	149	nncnd	$$⊢k\in {\mathbb{N}}_0\to 3\left(2k+1\right)9^k\in ℂ$$
151	149	nnne0d	$$⊢k\in {\mathbb{N}}_0\to 3\left(2k+1\right)9^k\ne 0$$
152	40 150 151	divcld	$$⊢k\in {\mathbb{N}}_0\to \frac{\mathrm{i}}{3\left(2k+1\right)9^k}\in ℂ$$
153		mulcom	$$⊢\left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\in ℂ\wedge \frac{2}{\mathrm{i}}\in ℂ\right)\to \left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\right)\left(\frac{2}{\mathrm{i}}\right)=\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\right)$$
154	152 7 153	sylancl	$$⊢k\in {\mathbb{N}}_0\to \left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\right)\left(\frac{2}{\mathrm{i}}\right)=\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\right)$$
155	4	a1i	$$⊢k\in {\mathbb{N}}_0\to 2\in ℂ$$
156	6	a1i	$$⊢k\in {\mathbb{N}}_0\to \mathrm{i}\ne 0$$
157	155 40 150 156 151	dmdcand	$$⊢k\in {\mathbb{N}}_0\to \left(\frac{\mathrm{i}}{3\left(2k+1\right)9^k}\right)\left(\frac{2}{\mathrm{i}}\right)=\frac{2}{3\left(2k+1\right)9^k}$$
158	146 154 157	3eqtr2d	$$⊢k\in {\mathbb{N}}_0\to \left(\frac{2}{\mathrm{i}}\right)\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)=\frac{2}{3\left(2k+1\right)9^k}$$
159	118 158	eqtr4d	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\left(\frac{2}{\mathrm{i}}\right)\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)$$
160	159	adantl	$$⊢\left(\top \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=\left(\frac{2}{\mathrm{i}}\right)\left(n\in {\mathbb{N}}_0⟼{\left(-1\right)}^n\left(\frac{{\left(\frac{\mathrm{i}}{3}\right)}^{2n+1}}{2n+1}\right)\right)\left(k\right)$$
161	2 3 8 31 112 160	isermulc2	$$⊢\top \to seq0\left(+,F\right)⇝\left(\frac{2}{\mathrm{i}}\right)arctan\left(\frac{\mathrm{i}}{3}\right)$$
162	161	mptru	$$⊢seq0\left(+,F\right)⇝\left(\frac{2}{\mathrm{i}}\right)arctan\left(\frac{\mathrm{i}}{3}\right)$$
163		bndatandm	$$⊢\left(\frac{\mathrm{i}}{3}\in ℂ\wedge \left|\frac{\mathrm{i}}{3}\right|<1\right)\to \frac{\mathrm{i}}{3}\in \mathrm{dom}arctan$$
164	11 27 163	mp2an	$$⊢\frac{\mathrm{i}}{3}\in \mathrm{dom}arctan$$
165		atanval	$$⊢\frac{\mathrm{i}}{3}\in \mathrm{dom}arctan\to arctan\left(\frac{\mathrm{i}}{3}\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)-\log \left(1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)\right)$$
166	164 165	ax-mp	$$⊢arctan\left(\frac{\mathrm{i}}{3}\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)-\log \left(1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)\right)$$
167		df-4	$$⊢4=3+1$$
168	167	oveq1i	$$⊢\frac{4}{3}=\frac{3+1}{3}$$
169		ax-1cn	$$⊢1\in ℂ$$
170	9 169 9 10	divdiri	$$⊢\frac{3+1}{3}=\left(\frac{3}{3}\right)+\left(\frac{1}{3}\right)$$
171	9 10	dividi	$$⊢\frac{3}{3}=1$$
172	171	oveq1i	$$⊢\left(\frac{3}{3}\right)+\left(\frac{1}{3}\right)=1+\left(\frac{1}{3}\right)$$
173	168 170 172	3eqtri	$$⊢\frac{4}{3}=1+\left(\frac{1}{3}\right)$$
174	169 9 10	divcli	$$⊢\frac{1}{3}\in ℂ$$
175	169 174	subnegi	$$⊢1-\left(-\frac{1}{3}\right)=1+\left(\frac{1}{3}\right)$$
176		divneg	$$⊢\left(1\in ℂ\wedge 3\in ℂ\wedge 3\ne 0\right)\to -\frac{1}{3}=\frac{-1}{3}$$
177	169 9 10 176	mp3an	$$⊢-\frac{1}{3}=\frac{-1}{3}$$
178		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
179	178	oveq1i	$$⊢\frac{\mathrm{i}\mathrm{i}}{3}=\frac{-1}{3}$$
180	5 5 9 10	divassi	$$⊢\frac{\mathrm{i}\mathrm{i}}{3}=\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)$$
181	177 179 180	3eqtr2i	$$⊢-\frac{1}{3}=\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)$$
182	181	oveq2i	$$⊢1-\left(-\frac{1}{3}\right)=1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)$$
183	173 175 182	3eqtr2ri	$$⊢1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)=\frac{4}{3}$$
184	183	fveq2i	$$⊢\log \left(1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)=\log \left(\frac{4}{3}\right)$$
185	9 10	pm3.2i	$$⊢\left(3\in ℂ\wedge 3\ne 0\right)$$
186		divsubdir	$$⊢\left(3\in ℂ\wedge 1\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{3-1}{3}=\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)$$
187	9 169 185 186	mp3an	$$⊢\frac{3-1}{3}=\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)$$
188		3m1e2	$$⊢3-1=2$$
189	188	oveq1i	$$⊢\frac{3-1}{3}=\frac{2}{3}$$
190	171	oveq1i	$$⊢\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)=1-\left(\frac{1}{3}\right)$$
191	187 189 190	3eqtr3i	$$⊢\frac{2}{3}=1-\left(\frac{1}{3}\right)$$
192	169 174	negsubi	$$⊢1+\left(-\frac{1}{3}\right)=1-\left(\frac{1}{3}\right)$$
193	181	oveq2i	$$⊢1+\left(-\frac{1}{3}\right)=1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)$$
194	191 192 193	3eqtr2ri	$$⊢1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)=\frac{2}{3}$$
195	194	fveq2i	$$⊢\log \left(1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)=\log \left(\frac{2}{3}\right)$$
196	184 195	oveq12i	$$⊢\log \left(1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)-\log \left(1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)=\log \left(\frac{4}{3}\right)-\log \left(\frac{2}{3}\right)$$
197		4re	$$⊢4\in ℝ$$
198		4pos	$$⊢0<4$$
199	197 198	elrpii	$$⊢4\in {ℝ}^{+}$$
200		3rp	$$⊢3\in {ℝ}^{+}$$
201		rpdivcl	$$⊢\left(4\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to \frac{4}{3}\in {ℝ}^{+}$$
202	199 200 201	mp2an	$$⊢\frac{4}{3}\in {ℝ}^{+}$$
203		2rp	$$⊢2\in {ℝ}^{+}$$
204		rpdivcl	$$⊢\left(2\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to \frac{2}{3}\in {ℝ}^{+}$$
205	203 200 204	mp2an	$$⊢\frac{2}{3}\in {ℝ}^{+}$$
206		relogdiv	$$⊢\left(\frac{4}{3}\in {ℝ}^{+}\wedge \frac{2}{3}\in {ℝ}^{+}\right)\to \log \left(\frac{\frac{4}{3}}{\frac{2}{3}}\right)=\log \left(\frac{4}{3}\right)-\log \left(\frac{2}{3}\right)$$
207	202 205 206	mp2an	$$⊢\log \left(\frac{\frac{4}{3}}{\frac{2}{3}}\right)=\log \left(\frac{4}{3}\right)-\log \left(\frac{2}{3}\right)$$
208		4cn	$$⊢4\in ℂ$$
209		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
210		divcan7	$$⊢\left(4\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{\frac{4}{3}}{\frac{2}{3}}=\frac{4}{2}$$
211	208 209 185 210	mp3an	$$⊢\frac{\frac{4}{3}}{\frac{2}{3}}=\frac{4}{2}$$
212		4div2e2	$$⊢\frac{4}{2}=2$$
213	211 212	eqtri	$$⊢\frac{\frac{4}{3}}{\frac{2}{3}}=2$$
214	213	fveq2i	$$⊢\log \left(\frac{\frac{4}{3}}{\frac{2}{3}}\right)=\log 2$$
215	196 207 214	3eqtr2i	$$⊢\log \left(1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)-\log \left(1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)=\log 2$$
216	215	oveq2i	$$⊢\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)-\log \left(1+\mathrm{i}\left(\frac{\mathrm{i}}{3}\right)\right)\right)=\left(\frac{\mathrm{i}}{2}\right)\log 2$$
217	166 216	eqtri	$$⊢arctan\left(\frac{\mathrm{i}}{3}\right)=\left(\frac{\mathrm{i}}{2}\right)\log 2$$
218	217	oveq2i	$$⊢\left(\frac{2}{\mathrm{i}}\right)arctan\left(\frac{\mathrm{i}}{3}\right)=\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)\log 2$$
219		2ne0	$$⊢2\ne 0$$
220	5 4 219	divcli	$$⊢\frac{\mathrm{i}}{2}\in ℂ$$
221		logcl	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)\to \log 2\in ℂ$$
222	4 219 221	mp2an	$$⊢\log 2\in ℂ$$
223	7 220 222	mulassi	$$⊢\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)\log 2=\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)\log 2$$
224	218 223	eqtr4i	$$⊢\left(\frac{2}{\mathrm{i}}\right)arctan\left(\frac{\mathrm{i}}{3}\right)=\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)\log 2$$
225		divcan6	$$⊢\left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\right)\to \left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)=1$$
226	4 219 5 6 225	mp4an	$$⊢\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)=1$$
227	226	oveq1i	$$⊢\left(\frac{2}{\mathrm{i}}\right)\left(\frac{\mathrm{i}}{2}\right)\log 2=1\log 2$$
228	222	mullidi	$$⊢1\log 2=\log 2$$
229	224 227 228	3eqtri	$$⊢\left(\frac{2}{\mathrm{i}}\right)arctan\left(\frac{\mathrm{i}}{3}\right)=\log 2$$
230	162 229	breqtri	$$⊢seq0\left(+,F\right)⇝\log 2$$