stirlinglem5

Description: If T is between 0 and 1 , then a series (without alternating negative and positive terms) is given that converges to log((1+T)/(1-T)). (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem5.1	$⊢ D = (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j}))$
	stirlinglem5.2	$⊢ E = (j \in ℕ ⟼ \frac{T^{j}}{j})$
	stirlinglem5.3	$⊢ F = (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j}) + (\frac{T^{j}}{j}))$
	stirlinglem5.4	$⊢ H = (j \in ℕ_{0} ⟼ 2 (\frac{1}{2 j + 1}) T^{2 j + 1})$
	stirlinglem5.5	$⊢ G = (j \in ℕ_{0} ⟼ 2 j + 1)$
	stirlinglem5.6	$⊢ φ \to T \in ℝ^{+}$
	stirlinglem5.7	$⊢ φ \to \|T\| < 1$
Assertion	stirlinglem5	$⊢ φ \to seq 0 (+ H) ⇝ \log (\frac{1 + T}{1 - T})$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem5.1	$⊢ D = (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j}))$
2		stirlinglem5.2	$⊢ E = (j \in ℕ ⟼ \frac{T^{j}}{j})$
3		stirlinglem5.3	$⊢ F = (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j}) + (\frac{T^{j}}{j}))$
4		stirlinglem5.4	$⊢ H = (j \in ℕ_{0} ⟼ 2 (\frac{1}{2 j + 1}) T^{2 j + 1})$
5		stirlinglem5.5	$⊢ G = (j \in ℕ_{0} ⟼ 2 j + 1)$
6		stirlinglem5.6	$⊢ φ \to T \in ℝ^{+}$
7		stirlinglem5.7	$⊢ φ \to \|T\| < 1$
8		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
9		1zzd	$⊢ φ \to 1 \in ℤ$
10	1	a1i	$⊢ φ \to D = (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j}))$
11		1cnd	$⊢ (φ \land j \in ℕ) \to 1 \in ℂ$
12	11	negcld	$⊢ (φ \land j \in ℕ) \to - 1 \in ℂ$
13		nnm1nn0	$⊢ j \in ℕ \to j - 1 \in ℕ_{0}$
14	13	adantl	$⊢ (φ \land j \in ℕ) \to j - 1 \in ℕ_{0}$
15	12 14	expcld	$⊢ (φ \land j \in ℕ) \to {(- 1)}^{j - 1} \in ℂ$
16		nncn	$⊢ j \in ℕ \to j \in ℂ$
17	16	adantl	$⊢ (φ \land j \in ℕ) \to j \in ℂ$
18	6	rpred	$⊢ φ \to T \in ℝ$
19	18	recnd	$⊢ φ \to T \in ℂ$
20	19	adantr	$⊢ (φ \land j \in ℕ) \to T \in ℂ$
21		nnnn0	$⊢ j \in ℕ \to j \in ℕ_{0}$
22	21	adantl	$⊢ (φ \land j \in ℕ) \to j \in ℕ_{0}$
23	20 22	expcld	$⊢ (φ \land j \in ℕ) \to T^{j} \in ℂ$
24		nnne0	$⊢ j \in ℕ \to j \neq 0$
25	24	adantl	$⊢ (φ \land j \in ℕ) \to j \neq 0$
26	15 17 23 25	div32d	$⊢ (φ \land j \in ℕ) \to (\frac{{(- 1)}^{j - 1}}{j}) T^{j} = {(- 1)}^{j - 1} (\frac{T^{j}}{j})$
27	11 20	pncan2d	$⊢ (φ \land j \in ℕ) \to 1 + T - 1 = T$
28	27	eqcomd	$⊢ (φ \land j \in ℕ) \to T = 1 + T - 1$
29	28	oveq1d	$⊢ (φ \land j \in ℕ) \to T^{j} = {(1 + T - 1)}^{j}$
30	29	oveq2d	$⊢ (φ \land j \in ℕ) \to (\frac{{(- 1)}^{j - 1}}{j}) T^{j} = (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j}$
31	26 30	eqtr3d	$⊢ (φ \land j \in ℕ) \to {(- 1)}^{j - 1} (\frac{T^{j}}{j}) = (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j}$
32	31	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j})) = (j \in ℕ ⟼ (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j})$
33	10 32	eqtrd	$⊢ φ \to D = (j \in ℕ ⟼ (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j})$
34	33	seqeq3d	$⊢ φ \to seq 1 (+ D) = seq 1 (+ (j \in ℕ ⟼ (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j}))$
35		1cnd	$⊢ φ \to 1 \in ℂ$
36	35 19	addcld	$⊢ φ \to 1 + T \in ℂ$
37		eqid	$⊢ abs \circ - = abs \circ -$
38	37	cnmetdval	$⊢ (1 \in ℂ \land 1 + T \in ℂ) \to 1 (abs \circ -) (1 + T) = \|1 - (1 + T)\|$
39	35 36 38	syl2anc	$⊢ φ \to 1 (abs \circ -) (1 + T) = \|1 - (1 + T)\|$
40		1m1e0	$⊢ 1 - 1 = 0$
41	40	a1i	$⊢ φ \to 1 - 1 = 0$
42	41	oveq1d	$⊢ φ \to 1 - 1 - T = 0 - T$
43	35 35 19	subsub4d	$⊢ φ \to 1 - 1 - T = 1 - (1 + T)$
44		df-neg	$⊢ - T = 0 - T$
45	44	eqcomi	$⊢ 0 - T = - T$
46	45	a1i	$⊢ φ \to 0 - T = - T$
47	42 43 46	3eqtr3d	$⊢ φ \to 1 - (1 + T) = - T$
48	47	fveq2d	$⊢ φ \to \|1 - (1 + T)\| = \|- T\|$
49	19	absnegd	$⊢ φ \to \|- T\| = \|T\|$
50	49 7	eqbrtrd	$⊢ φ \to \|- T\| < 1$
51	48 50	eqbrtrd	$⊢ φ \to \|1 - (1 + T)\| < 1$
52	39 51	eqbrtrd	$⊢ φ \to 1 (abs \circ -) (1 + T) < 1$
53		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
54	53	a1i	$⊢ φ \to abs \circ - \in ∞Met (ℂ)$
55		1red	$⊢ φ \to 1 \in ℝ$
56	55	rexrd	$⊢ φ \to 1 \in ℝ^{*}$
57		elbl2	$⊢ ((abs \circ - \in ∞Met (ℂ) \land 1 \in ℝ^{*}) \land (1 \in ℂ \land 1 + T \in ℂ)) \to (1 + T \in (1 ball (abs \circ -) 1) \leftrightarrow 1 (abs \circ -) (1 + T) < 1)$
58	54 56 35 36 57	syl22anc	$⊢ φ \to (1 + T \in (1 ball (abs \circ -) 1) \leftrightarrow 1 (abs \circ -) (1 + T) < 1)$
59	52 58	mpbird	$⊢ φ \to 1 + T \in (1 ball (abs \circ -) 1)$
60		eqid	$⊢ 1 ball (abs \circ -) 1 = 1 ball (abs \circ -) 1$
61	60	logtayl2	$⊢ 1 + T \in (1 ball (abs \circ -) 1) \to seq 1 (+ (j \in ℕ ⟼ (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j})) ⇝ \log (1 + T)$
62	59 61	syl	$⊢ φ \to seq 1 (+ (j \in ℕ ⟼ (\frac{{(- 1)}^{j - 1}}{j}) {(1 + T - 1)}^{j})) ⇝ \log (1 + T)$
63	34 62	eqbrtrd	$⊢ φ \to seq 1 (+ D) ⇝ \log (1 + T)$
64		seqex	$⊢ seq 1 (+ F) \in V$
65	64	a1i	$⊢ φ \to seq 1 (+ F) \in V$
66	2	a1i	$⊢ φ \to E = (j \in ℕ ⟼ \frac{T^{j}}{j})$
67	66	seqeq3d	$⊢ φ \to seq 1 (+ E) = seq 1 (+ (j \in ℕ ⟼ \frac{T^{j}}{j}))$
68		logtayl	$⊢ (T \in ℂ \land \|T\| < 1) \to seq 1 (+ (j \in ℕ ⟼ \frac{T^{j}}{j})) ⇝ (- \log (1 - T))$
69	19 7 68	syl2anc	$⊢ φ \to seq 1 (+ (j \in ℕ ⟼ \frac{T^{j}}{j})) ⇝ (- \log (1 - T))$
70	67 69	eqbrtrd	$⊢ φ \to seq 1 (+ E) ⇝ (- \log (1 - T))$
71		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
72	71 8	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
73		oveq1	$⊢ j = n \to j - 1 = n - 1$
74	73	oveq2d	$⊢ j = n \to {(- 1)}^{j - 1} = {(- 1)}^{n - 1}$
75		oveq2	$⊢ j = n \to T^{j} = T^{n}$
76		id	$⊢ j = n \to j = n$
77	75 76	oveq12d	$⊢ j = n \to \frac{T^{j}}{j} = \frac{T^{n}}{n}$
78	74 77	oveq12d	$⊢ j = n \to {(- 1)}^{j - 1} (\frac{T^{j}}{j}) = {(- 1)}^{n - 1} (\frac{T^{n}}{n})$
79		elfznn	$⊢ n \in (1 \dots k) \to n \in ℕ$
80	79	adantl	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \in ℕ$
81		1cnd	$⊢ n \in ℕ \to 1 \in ℂ$
82	81	negcld	$⊢ n \in ℕ \to - 1 \in ℂ$
83		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
84	82 83	expcld	$⊢ n \in ℕ \to {(- 1)}^{n - 1} \in ℂ$
85	80 84	syl	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to {(- 1)}^{n - 1} \in ℂ$
86	19	ad2antrr	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to T \in ℂ$
87	80	nnnn0d	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \in ℕ_{0}$
88	86 87	expcld	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to T^{n} \in ℂ$
89	80	nncnd	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \in ℂ$
90	80	nnne0d	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \neq 0$
91	88 89 90	divcld	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to \frac{T^{n}}{n} \in ℂ$
92	85 91	mulcld	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) \in ℂ$
93	1 78 80 92	fvmptd3	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to D (n) = {(- 1)}^{n - 1} (\frac{T^{n}}{n})$
94	93 92	eqeltrd	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to D (n) \in ℂ$
95		addcl	$⊢ (n \in ℂ \land i \in ℂ) \to n + i \in ℂ$
96	95	adantl	$⊢ ((φ \land k \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to n + i \in ℂ$
97	72 94 96	seqcl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ D) (k) \in ℂ$
98	2 77 80 91	fvmptd3	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to E (n) = \frac{T^{n}}{n}$
99	98 91	eqeltrd	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to E (n) \in ℂ$
100	72 99 96	seqcl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ E) (k) \in ℂ$
101		simpll	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to φ$
102	78 77	oveq12d	$⊢ j = n \to {(- 1)}^{j - 1} (\frac{T^{j}}{j}) + (\frac{T^{j}}{j}) = {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n})$
103		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
104	84	adantl	$⊢ (φ \land n \in ℕ) \to {(- 1)}^{n - 1} \in ℂ$
105	19	adantr	$⊢ (φ \land n \in ℕ) \to T \in ℂ$
106	103	nnnn0d	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
107	105 106	expcld	$⊢ (φ \land n \in ℕ) \to T^{n} \in ℂ$
108	103	nncnd	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
109	103	nnne0d	$⊢ (φ \land n \in ℕ) \to n \neq 0$
110	107 108 109	divcld	$⊢ (φ \land n \in ℕ) \to \frac{T^{n}}{n} \in ℂ$
111	104 110	mulcld	$⊢ (φ \land n \in ℕ) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) \in ℂ$
112	111 110	addcld	$⊢ (φ \land n \in ℕ) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) \in ℂ$
113	3 102 103 112	fvmptd3	$⊢ (φ \land n \in ℕ) \to F (n) = {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n})$
114	1 78 103 111	fvmptd3	$⊢ (φ \land n \in ℕ) \to D (n) = {(- 1)}^{n - 1} (\frac{T^{n}}{n})$
115	114	eqcomd	$⊢ (φ \land n \in ℕ) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) = D (n)$
116	2 77 103 110	fvmptd3	$⊢ (φ \land n \in ℕ) \to E (n) = \frac{T^{n}}{n}$
117	116	eqcomd	$⊢ (φ \land n \in ℕ) \to \frac{T^{n}}{n} = E (n)$
118	115 117	oveq12d	$⊢ (φ \land n \in ℕ) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) = D (n) + E (n)$
119	113 118	eqtrd	$⊢ (φ \land n \in ℕ) \to F (n) = D (n) + E (n)$
120	101 80 119	syl2anc	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to F (n) = D (n) + E (n)$
121	72 94 99 120	seradd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ F) (k) = seq 1 (+ D) (k) + seq 1 (+ E) (k)$
122	8 9 63 65 70 97 100 121	climadd	$⊢ φ \to seq 1 (+ F) ⇝ (\log (1 + T) + (- \log (1 - T)))$
123		1rp	$⊢ 1 \in ℝ^{+}$
124	123	a1i	$⊢ φ \to 1 \in ℝ^{+}$
125	124 6	rpaddcld	$⊢ φ \to 1 + T \in ℝ^{+}$
126	125	rpne0d	$⊢ φ \to 1 + T \neq 0$
127	36 126	logcld	$⊢ φ \to \log (1 + T) \in ℂ$
128	35 19	subcld	$⊢ φ \to 1 - T \in ℂ$
129	18 55	absltd	$⊢ φ \to (\|T\| < 1 \leftrightarrow (- 1 < T \land T < 1))$
130	7 129	mpbid	$⊢ φ \to (- 1 < T \land T < 1)$
131	130	simprd	$⊢ φ \to T < 1$
132	18 131	gtned	$⊢ φ \to 1 \neq T$
133	35 19 132	subne0d	$⊢ φ \to 1 - T \neq 0$
134	128 133	logcld	$⊢ φ \to \log (1 - T) \in ℂ$
135	127 134	negsubd	$⊢ φ \to \log (1 + T) + (- \log (1 - T)) = \log (1 + T) - \log (1 - T)$
136	122 135	breqtrd	$⊢ φ \to seq 1 (+ F) ⇝ (\log (1 + T) - \log (1 - T))$
137		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
138		0zd	$⊢ φ \to 0 \in ℤ$
139		2nn0	$⊢ 2 \in ℕ_{0}$
140	139	a1i	$⊢ j \in ℕ_{0} \to 2 \in ℕ_{0}$
141		id	$⊢ j \in ℕ_{0} \to j \in ℕ_{0}$
142	140 141	nn0mulcld	$⊢ j \in ℕ_{0} \to 2 j \in ℕ_{0}$
143		nn0p1nn	$⊢ 2 j \in ℕ_{0} \to 2 j + 1 \in ℕ$
144	142 143	syl	$⊢ j \in ℕ_{0} \to 2 j + 1 \in ℕ$
145	5 144	fmpti	$⊢ G : ℕ_{0} ⟶ ℕ$
146	145	a1i	$⊢ φ \to G : ℕ_{0} ⟶ ℕ$
147		2re	$⊢ 2 \in ℝ$
148	147	a1i	$⊢ k \in ℕ_{0} \to 2 \in ℝ$
149		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
150	148 149	remulcld	$⊢ k \in ℕ_{0} \to 2 k \in ℝ$
151		1red	$⊢ k \in ℕ_{0} \to 1 \in ℝ$
152	149 151	readdcld	$⊢ k \in ℕ_{0} \to k + 1 \in ℝ$
153	148 152	remulcld	$⊢ k \in ℕ_{0} \to 2 (k + 1) \in ℝ$
154		2rp	$⊢ 2 \in ℝ^{+}$
155	154	a1i	$⊢ k \in ℕ_{0} \to 2 \in ℝ^{+}$
156	149	ltp1d	$⊢ k \in ℕ_{0} \to k < k + 1$
157	149 152 155 156	ltmul2dd	$⊢ k \in ℕ_{0} \to 2 k < 2 (k + 1)$
158	150 153 151 157	ltadd1dd	$⊢ k \in ℕ_{0} \to 2 k + 1 < 2 (k + 1) + 1$
159	5	a1i	$⊢ k \in ℕ_{0} \to G = (j \in ℕ_{0} ⟼ 2 j + 1)$
160		simpr	$⊢ (k \in ℕ_{0} \land j = k) \to j = k$
161	160	oveq2d	$⊢ (k \in ℕ_{0} \land j = k) \to 2 j = 2 k$
162	161	oveq1d	$⊢ (k \in ℕ_{0} \land j = k) \to 2 j + 1 = 2 k + 1$
163		id	$⊢ k \in ℕ_{0} \to k \in ℕ_{0}$
164		2cnd	$⊢ k \in ℕ_{0} \to 2 \in ℂ$
165		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
166	164 165	mulcld	$⊢ k \in ℕ_{0} \to 2 k \in ℂ$
167		1cnd	$⊢ k \in ℕ_{0} \to 1 \in ℂ$
168	166 167	addcld	$⊢ k \in ℕ_{0} \to 2 k + 1 \in ℂ$
169	159 162 163 168	fvmptd	$⊢ k \in ℕ_{0} \to G (k) = 2 k + 1$
170		simpr	$⊢ (k \in ℕ_{0} \land j = k + 1) \to j = k + 1$
171	170	oveq2d	$⊢ (k \in ℕ_{0} \land j = k + 1) \to 2 j = 2 (k + 1)$
172	171	oveq1d	$⊢ (k \in ℕ_{0} \land j = k + 1) \to 2 j + 1 = 2 (k + 1) + 1$
173		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
174	165 167	addcld	$⊢ k \in ℕ_{0} \to k + 1 \in ℂ$
175	164 174	mulcld	$⊢ k \in ℕ_{0} \to 2 (k + 1) \in ℂ$
176	175 167	addcld	$⊢ k \in ℕ_{0} \to 2 (k + 1) + 1 \in ℂ$
177	159 172 173 176	fvmptd	$⊢ k \in ℕ_{0} \to G (k + 1) = 2 (k + 1) + 1$
178	158 169 177	3brtr4d	$⊢ k \in ℕ_{0} \to G (k) < G (k + 1)$
179	178	adantl	$⊢ (φ \land k \in ℕ_{0}) \to G (k) < G (k + 1)$
180		eldifi	$⊢ n \in (ℕ ∖ ran G) \to n \in ℕ$
181	180	adantl	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to n \in ℕ$
182		1cnd	$⊢ n \in (ℕ ∖ ran G) \to 1 \in ℂ$
183	182	negcld	$⊢ n \in (ℕ ∖ ran G) \to - 1 \in ℂ$
184	180 83	syl	$⊢ n \in (ℕ ∖ ran G) \to n - 1 \in ℕ_{0}$
185	183 184	expcld	$⊢ n \in (ℕ ∖ ran G) \to {(- 1)}^{n - 1} \in ℂ$
186	185	adantl	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to {(- 1)}^{n - 1} \in ℂ$
187	19	adantr	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to T \in ℂ$
188	181	nnnn0d	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to n \in ℕ_{0}$
189	187 188	expcld	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to T^{n} \in ℂ$
190	181	nncnd	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to n \in ℂ$
191	181	nnne0d	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to n \neq 0$
192	189 190 191	divcld	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to \frac{T^{n}}{n} \in ℂ$
193	186 192	mulcld	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) \in ℂ$
194	193 192	addcld	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) \in ℂ$
195	3 102 181 194	fvmptd3	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to F (n) = {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n})$
196		eldifn	$⊢ n \in (ℕ ∖ ran G) \to \neg n \in ran G$
197		0nn0	$⊢ 0 \in ℕ_{0}$
198		1nn0	$⊢ 1 \in ℕ_{0}$
199	139 198	num0h	$⊢ 1 = 2 \cdot 0 + 1$
200		oveq2	$⊢ j = 0 \to 2 j = 2 \cdot 0$
201	200	oveq1d	$⊢ j = 0 \to 2 j + 1 = 2 \cdot 0 + 1$
202	201	eqeq2d	$⊢ j = 0 \to (1 = 2 j + 1 \leftrightarrow 1 = 2 \cdot 0 + 1)$
203	202	rspcev	$⊢ (0 \in ℕ_{0} \land 1 = 2 \cdot 0 + 1) \to \exists j \in ℕ_{0} 1 = 2 j + 1$
204	197 199 203	mp2an	$⊢ \exists j \in ℕ_{0} 1 = 2 j + 1$
205		ax-1cn	$⊢ 1 \in ℂ$
206	5	elrnmpt	$⊢ 1 \in ℂ \to (1 \in ran G \leftrightarrow \exists j \in ℕ_{0} 1 = 2 j + 1)$
207	205 206	ax-mp	$⊢ 1 \in ran G \leftrightarrow \exists j \in ℕ_{0} 1 = 2 j + 1$
208	204 207	mpbir	$⊢ 1 \in ran G$
209	208	a1i	$⊢ n = 1 \to 1 \in ran G$
210		eleq1	$⊢ n = 1 \to (n \in ran G \leftrightarrow 1 \in ran G)$
211	209 210	mpbird	$⊢ n = 1 \to n \in ran G$
212	196 211	nsyl	$⊢ n \in (ℕ ∖ ran G) \to \neg n = 1$
213		nn1m1nn	$⊢ n \in ℕ \to (n = 1 \lor n - 1 \in ℕ)$
214	180 213	syl	$⊢ n \in (ℕ ∖ ran G) \to (n = 1 \lor n - 1 \in ℕ)$
215	214	ord	$⊢ n \in (ℕ ∖ ran G) \to (\neg n = 1 \to n - 1 \in ℕ)$
216	212 215	mpd	$⊢ n \in (ℕ ∖ ran G) \to n - 1 \in ℕ$
217		nfcv	$⊢ \underline{Ⅎ} j ℕ$
218		nfmpt1	$⊢ \underline{Ⅎ} j (j \in ℕ_{0} ⟼ 2 j + 1)$
219	5 218	nfcxfr	$⊢ \underline{Ⅎ} j G$
220	219	nfrn	$⊢ \underline{Ⅎ} j ran G$
221	217 220	nfdif	$⊢ \underline{Ⅎ} j (ℕ ∖ ran G)$
222	221	nfcri	$⊢ Ⅎ j n \in (ℕ ∖ ran G)$
223	5	elrnmpt	$⊢ n \in (ℕ ∖ ran G) \to (n \in ran G \leftrightarrow \exists j \in ℕ_{0} n = 2 j + 1)$
224	196 223	mtbid	$⊢ n \in (ℕ ∖ ran G) \to \neg \exists j \in ℕ_{0} n = 2 j + 1$
225		ralnex	$⊢ \forall j \in ℕ_{0} \neg n = 2 j + 1 \leftrightarrow \neg \exists j \in ℕ_{0} n = 2 j + 1$
226	224 225	sylibr	$⊢ n \in (ℕ ∖ ran G) \to \forall j \in ℕ_{0} \neg n = 2 j + 1$
227	226	r19.21bi	$⊢ (n \in (ℕ ∖ ran G) \land j \in ℕ_{0}) \to \neg n = 2 j + 1$
228	227	neqned	$⊢ (n \in (ℕ ∖ ran G) \land j \in ℕ_{0}) \to n \neq 2 j + 1$
229	228	necomd	$⊢ (n \in (ℕ ∖ ran G) \land j \in ℕ_{0}) \to 2 j + 1 \neq n$
230	229	adantlr	$⊢ ((n \in (ℕ ∖ ran G) \land j \in ℤ) \land j \in ℕ_{0}) \to 2 j + 1 \neq n$
231		simplr	$⊢ ((n \in (ℕ ∖ ran G) \land j \in ℤ) \land \neg j \in ℕ_{0}) \to j \in ℤ$
232		simpr	$⊢ ((n \in (ℕ ∖ ran G) \land j \in ℤ) \land \neg j \in ℕ_{0}) \to \neg j \in ℕ_{0}$
233	180	ad2antrr	$⊢ ((n \in (ℕ ∖ ran G) \land j \in ℤ) \land \neg j \in ℕ_{0}) \to n \in ℕ$
234	147	a1i	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 \in ℝ$
235		simpl	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to j \in ℤ$
236	235	zred	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to j \in ℝ$
237	234 236	remulcld	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 j \in ℝ$
238		0red	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 0 \in ℝ$
239		1red	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 1 \in ℝ$
240		2cnd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 \in ℂ$
241	236	recnd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to j \in ℂ$
242	240 241	mulcomd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 j = j \cdot 2$
243		simpr	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to \neg j \in ℕ_{0}$
244		elnn0z	$⊢ j \in ℕ_{0} \leftrightarrow (j \in ℤ \land 0 \leq j)$
245	243 244	sylnib	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to \neg (j \in ℤ \land 0 \leq j)$
246		nan	$⊢ ((j \in ℤ \land \neg j \in ℕ_{0}) \to \neg (j \in ℤ \land 0 \leq j)) \leftrightarrow (((j \in ℤ \land \neg j \in ℕ_{0}) \land j \in ℤ) \to \neg 0 \leq j)$
247	245 246	mpbi	$⊢ ((j \in ℤ \land \neg j \in ℕ_{0}) \land j \in ℤ) \to \neg 0 \leq j$
248	247	anabss1	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to \neg 0 \leq j$
249	236 238	ltnled	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to (j < 0 \leftrightarrow \neg 0 \leq j)$
250	248 249	mpbird	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to j < 0$
251	154	a1i	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 \in ℝ^{+}$
252	251	rpregt0d	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to (2 \in ℝ \land 0 < 2)$
253		mulltgt0	$⊢ ((j \in ℝ \land j < 0) \land (2 \in ℝ \land 0 < 2)) \to j \cdot 2 < 0$
254	236 250 252 253	syl21anc	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to j \cdot 2 < 0$
255	242 254	eqbrtrd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 j < 0$
256	237 238 239 255	ltadd1dd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 j + 1 < 0 + 1$
257		1cnd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 1 \in ℂ$
258	257	addlidd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 0 + 1 = 1$
259	256 258	breqtrd	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 j + 1 < 1$
260	237 239	readdcld	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to 2 j + 1 \in ℝ$
261	260 239	ltnled	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to (2 j + 1 < 1 \leftrightarrow \neg 1 \leq 2 j + 1)$
262	259 261	mpbid	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to \neg 1 \leq 2 j + 1$
263		nnge1	$⊢ 2 j + 1 \in ℕ \to 1 \leq 2 j + 1$
264	262 263	nsyl	$⊢ (j \in ℤ \land \neg j \in ℕ_{0}) \to \neg 2 j + 1 \in ℕ$
265	264	adantr	$⊢ ((j \in ℤ \land \neg j \in ℕ_{0}) \land n \in ℕ) \to \neg 2 j + 1 \in ℕ$
266		simpr	$⊢ (n \in ℕ \land 2 j + 1 = n) \to 2 j + 1 = n$
267		simpl	$⊢ (n \in ℕ \land 2 j + 1 = n) \to n \in ℕ$
268	266 267	eqeltrd	$⊢ (n \in ℕ \land 2 j + 1 = n) \to 2 j + 1 \in ℕ$
269	268	adantll	$⊢ (((j \in ℤ \land \neg j \in ℕ_{0}) \land n \in ℕ) \land 2 j + 1 = n) \to 2 j + 1 \in ℕ$
270	265 269	mtand	$⊢ ((j \in ℤ \land \neg j \in ℕ_{0}) \land n \in ℕ) \to \neg 2 j + 1 = n$
271	270	neqned	$⊢ ((j \in ℤ \land \neg j \in ℕ_{0}) \land n \in ℕ) \to 2 j + 1 \neq n$
272	231 232 233 271	syl21anc	$⊢ ((n \in (ℕ ∖ ran G) \land j \in ℤ) \land \neg j \in ℕ_{0}) \to 2 j + 1 \neq n$
273	230 272	pm2.61dan	$⊢ (n \in (ℕ ∖ ran G) \land j \in ℤ) \to 2 j + 1 \neq n$
274	273	neneqd	$⊢ (n \in (ℕ ∖ ran G) \land j \in ℤ) \to \neg 2 j + 1 = n$
275	274	ex	$⊢ n \in (ℕ ∖ ran G) \to (j \in ℤ \to \neg 2 j + 1 = n)$
276	222 275	ralrimi	$⊢ n \in (ℕ ∖ ran G) \to \forall j \in ℤ \neg 2 j + 1 = n$
277		ralnex	$⊢ \forall j \in ℤ \neg 2 j + 1 = n \leftrightarrow \neg \exists j \in ℤ 2 j + 1 = n$
278	276 277	sylib	$⊢ n \in (ℕ ∖ ran G) \to \neg \exists j \in ℤ 2 j + 1 = n$
279	180	nnzd	$⊢ n \in (ℕ ∖ ran G) \to n \in ℤ$
280		odd2np1	$⊢ n \in ℤ \to (\neg 2 ∥ n \leftrightarrow \exists j \in ℤ 2 j + 1 = n)$
281	279 280	syl	$⊢ n \in (ℕ ∖ ran G) \to (\neg 2 ∥ n \leftrightarrow \exists j \in ℤ 2 j + 1 = n)$
282	278 281	mtbird	$⊢ n \in (ℕ ∖ ran G) \to \neg \neg 2 ∥ n$
283	282	notnotrd	$⊢ n \in (ℕ ∖ ran G) \to 2 ∥ n$
284	180	nncnd	$⊢ n \in (ℕ ∖ ran G) \to n \in ℂ$
285	284 182	npcand	$⊢ n \in (ℕ ∖ ran G) \to n - 1 + 1 = n$
286	283 285	breqtrrd	$⊢ n \in (ℕ ∖ ran G) \to 2 ∥ (n - 1 + 1)$
287	184	nn0zd	$⊢ n \in (ℕ ∖ ran G) \to n - 1 \in ℤ$
288		oddp1even	$⊢ n - 1 \in ℤ \to (\neg 2 ∥ (n - 1) \leftrightarrow 2 ∥ (n - 1 + 1))$
289	287 288	syl	$⊢ n \in (ℕ ∖ ran G) \to (\neg 2 ∥ (n - 1) \leftrightarrow 2 ∥ (n - 1 + 1))$
290	286 289	mpbird	$⊢ n \in (ℕ ∖ ran G) \to \neg 2 ∥ (n - 1)$
291		oexpneg	$⊢ (1 \in ℂ \land n - 1 \in ℕ \land \neg 2 ∥ (n - 1)) \to {(- 1)}^{n - 1} = - 1^{n - 1}$
292	182 216 290 291	syl3anc	$⊢ n \in (ℕ ∖ ran G) \to {(- 1)}^{n - 1} = - 1^{n - 1}$
293		1exp	$⊢ n - 1 \in ℤ \to 1^{n - 1} = 1$
294	287 293	syl	$⊢ n \in (ℕ ∖ ran G) \to 1^{n - 1} = 1$
295	294	negeqd	$⊢ n \in (ℕ ∖ ran G) \to - 1^{n - 1} = - 1$
296	292 295	eqtrd	$⊢ n \in (ℕ ∖ ran G) \to {(- 1)}^{n - 1} = - 1$
297	296	adantl	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to {(- 1)}^{n - 1} = - 1$
298	297	oveq1d	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) = -1 (\frac{T^{n}}{n})$
299	298	oveq1d	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to {(- 1)}^{n - 1} (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) = -1 (\frac{T^{n}}{n}) + (\frac{T^{n}}{n})$
300	192	mulm1d	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to -1 (\frac{T^{n}}{n}) = - \frac{T^{n}}{n}$
301	300	oveq1d	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to -1 (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) = - (\frac{T^{n}}{n}) + (\frac{T^{n}}{n})$
302	192	negcld	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to - \frac{T^{n}}{n} \in ℂ$
303	302 192	addcomd	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to - (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) = (\frac{T^{n}}{n}) + (- \frac{T^{n}}{n})$
304	192	negidd	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to (\frac{T^{n}}{n}) + (- \frac{T^{n}}{n}) = 0$
305	301 303 304	3eqtrd	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to -1 (\frac{T^{n}}{n}) + (\frac{T^{n}}{n}) = 0$
306	195 299 305	3eqtrd	$⊢ (φ \land n \in (ℕ ∖ ran G)) \to F (n) = 0$
307	113 112	eqeltrd	$⊢ (φ \land n \in ℕ) \to F (n) \in ℂ$
308	3	a1i	$⊢ (φ \land k \in ℕ_{0}) \to F = (j \in ℕ ⟼ {(- 1)}^{j - 1} (\frac{T^{j}}{j}) + (\frac{T^{j}}{j}))$
309		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to j = 2 k + 1$
310	309	oveq1d	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to j - 1 = 2 k + 1 - 1$
311	310	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to {(- 1)}^{j - 1} = {(- 1)}^{2 k + 1 - 1}$
312	309	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to T^{j} = T^{2 k + 1}$
313	312 309	oveq12d	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to \frac{T^{j}}{j} = \frac{T^{2 k + 1}}{2 k + 1}$
314	311 313	oveq12d	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to {(- 1)}^{j - 1} (\frac{T^{j}}{j}) = {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1})$
315	314 313	oveq12d	$⊢ ((φ \land k \in ℕ_{0}) \land j = 2 k + 1) \to {(- 1)}^{j - 1} (\frac{T^{j}}{j}) + (\frac{T^{j}}{j}) = {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1})$
316	139	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 2 \in ℕ_{0}$
317		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
318	316 317	nn0mulcld	$⊢ (φ \land k \in ℕ_{0}) \to 2 k \in ℕ_{0}$
319		nn0p1nn	$⊢ 2 k \in ℕ_{0} \to 2 k + 1 \in ℕ$
320	318 319	syl	$⊢ (φ \land k \in ℕ_{0}) \to 2 k + 1 \in ℕ$
321	167	negcld	$⊢ k \in ℕ_{0} \to - 1 \in ℂ$
322	166 167	pncand	$⊢ k \in ℕ_{0} \to 2 k + 1 - 1 = 2 k$
323	139	a1i	$⊢ k \in ℕ_{0} \to 2 \in ℕ_{0}$
324	323 163	nn0mulcld	$⊢ k \in ℕ_{0} \to 2 k \in ℕ_{0}$
325	322 324	eqeltrd	$⊢ k \in ℕ_{0} \to 2 k + 1 - 1 \in ℕ_{0}$
326	321 325	expcld	$⊢ k \in ℕ_{0} \to {(- 1)}^{2 k + 1 - 1} \in ℂ$
327	326	adantl	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} \in ℂ$
328	19	adantr	$⊢ (φ \land k \in ℕ_{0}) \to T \in ℂ$
329	198	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 1 \in ℕ_{0}$
330	318 329	nn0addcld	$⊢ (φ \land k \in ℕ_{0}) \to 2 k + 1 \in ℕ_{0}$
331	328 330	expcld	$⊢ (φ \land k \in ℕ_{0}) \to T^{2 k + 1} \in ℂ$
332		2cnd	$⊢ (φ \land k \in ℕ_{0}) \to 2 \in ℂ$
333	165	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℂ$
334	332 333	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to 2 k \in ℂ$
335		1cnd	$⊢ (φ \land k \in ℕ_{0}) \to 1 \in ℂ$
336	334 335	addcld	$⊢ (φ \land k \in ℕ_{0}) \to 2 k + 1 \in ℂ$
337		0red	$⊢ (φ \land k \in ℕ_{0}) \to 0 \in ℝ$
338	147	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 2 \in ℝ$
339	149	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℝ$
340	338 339	remulcld	$⊢ (φ \land k \in ℕ_{0}) \to 2 k \in ℝ$
341		1red	$⊢ (φ \land k \in ℕ_{0}) \to 1 \in ℝ$
342		0le2	$⊢ 0 \leq 2$
343	342	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 0 \leq 2$
344	317	nn0ge0d	$⊢ (φ \land k \in ℕ_{0}) \to 0 \leq k$
345	338 339 343 344	mulge0d	$⊢ (φ \land k \in ℕ_{0}) \to 0 \leq 2 k$
346		0lt1	$⊢ 0 < 1$
347	346	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 0 < 1$
348	340 341 345 347	addgegt0d	$⊢ (φ \land k \in ℕ_{0}) \to 0 < 2 k + 1$
349	337 348	gtned	$⊢ (φ \land k \in ℕ_{0}) \to 2 k + 1 \neq 0$
350	331 336 349	divcld	$⊢ (φ \land k \in ℕ_{0}) \to \frac{T^{2 k + 1}}{2 k + 1} \in ℂ$
351	327 350	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) \in ℂ$
352	351 350	addcld	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1}) \in ℂ$
353	308 315 320 352	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to F (2 k + 1) = {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1})$
354	322	adantl	$⊢ (φ \land k \in ℕ_{0}) \to 2 k + 1 - 1 = 2 k$
355	354	oveq2d	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} = {(- 1)}^{2 k}$
356		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
357		m1expeven	$⊢ k \in ℤ \to {(- 1)}^{2 k} = 1$
358	356 357	syl	$⊢ k \in ℕ_{0} \to {(- 1)}^{2 k} = 1$
359	358	adantl	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k} = 1$
360	355 359	eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} = 1$
361	360	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) = 1 (\frac{T^{2 k + 1}}{2 k + 1})$
362	350	mullidd	$⊢ (φ \land k \in ℕ_{0}) \to 1 (\frac{T^{2 k + 1}}{2 k + 1}) = \frac{T^{2 k + 1}}{2 k + 1}$
363	361 362	eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) = \frac{T^{2 k + 1}}{2 k + 1}$
364	363	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1}) = (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1})$
365	350	2timesd	$⊢ (φ \land k \in ℕ_{0}) \to 2 (\frac{T^{2 k + 1}}{2 k + 1}) = (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1})$
366	331 336 349	divrec2d	$⊢ (φ \land k \in ℕ_{0}) \to \frac{T^{2 k + 1}}{2 k + 1} = (\frac{1}{2 k + 1}) T^{2 k + 1}$
367	366	oveq2d	$⊢ (φ \land k \in ℕ_{0}) \to 2 (\frac{T^{2 k + 1}}{2 k + 1}) = 2 (\frac{1}{2 k + 1}) T^{2 k + 1}$
368	364 365 367	3eqtr2d	$⊢ (φ \land k \in ℕ_{0}) \to {(- 1)}^{2 k + 1 - 1} (\frac{T^{2 k + 1}}{2 k + 1}) + (\frac{T^{2 k + 1}}{2 k + 1}) = 2 (\frac{1}{2 k + 1}) T^{2 k + 1}$
369	353 368	eqtr2d	$⊢ (φ \land k \in ℕ_{0}) \to 2 (\frac{1}{2 k + 1}) T^{2 k + 1} = F (2 k + 1)$
370	4	a1i	$⊢ (φ \land k \in ℕ_{0}) \to H = (j \in ℕ_{0} ⟼ 2 (\frac{1}{2 j + 1}) T^{2 j + 1})$
371		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to j = k$
372	371	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to 2 j = 2 k$
373	372	oveq1d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to 2 j + 1 = 2 k + 1$
374	373	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to \frac{1}{2 j + 1} = \frac{1}{2 k + 1}$
375	373	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to T^{2 j + 1} = T^{2 k + 1}$
376	374 375	oveq12d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to (\frac{1}{2 j + 1}) T^{2 j + 1} = (\frac{1}{2 k + 1}) T^{2 k + 1}$
377	376	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to 2 (\frac{1}{2 j + 1}) T^{2 j + 1} = 2 (\frac{1}{2 k + 1}) T^{2 k + 1}$
378	336 349	reccld	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2 k + 1} \in ℂ$
379	378 331	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to (\frac{1}{2 k + 1}) T^{2 k + 1} \in ℂ$
380	332 379	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to 2 (\frac{1}{2 k + 1}) T^{2 k + 1} \in ℂ$
381	370 377 317 380	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = 2 (\frac{1}{2 k + 1}) T^{2 k + 1}$
382	198	a1i	$⊢ k \in ℕ_{0} \to 1 \in ℕ_{0}$
383	324 382	nn0addcld	$⊢ k \in ℕ_{0} \to 2 k + 1 \in ℕ_{0}$
384	159 162 163 383	fvmptd	$⊢ k \in ℕ_{0} \to G (k) = 2 k + 1$
385	384	adantl	$⊢ (φ \land k \in ℕ_{0}) \to G (k) = 2 k + 1$
386	385	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to F (G (k)) = F (2 k + 1)$
387	369 381 386	3eqtr4d	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = F (G (k))$
388	137 8 138 9 146 179 306 307 387	isercoll2	$⊢ φ \to (seq 0 (+ H) ⇝ (\log (1 + T) - \log (1 - T)) \leftrightarrow seq 1 (+ F) ⇝ (\log (1 + T) - \log (1 - T)))$
389	136 388	mpbird	$⊢ φ \to seq 0 (+ H) ⇝ (\log (1 + T) - \log (1 - T))$
390	55 18	resubcld	$⊢ φ \to 1 - T \in ℝ$
391	19	subidd	$⊢ φ \to T - T = 0$
392	391	eqcomd	$⊢ φ \to 0 = T - T$
393	18 55 18 131	ltsub1dd	$⊢ φ \to T - T < 1 - T$
394	392 393	eqbrtrd	$⊢ φ \to 0 < 1 - T$
395	390 394	elrpd	$⊢ φ \to 1 - T \in ℝ^{+}$
396	125 395	relogdivd	$⊢ φ \to \log (\frac{1 + T}{1 - T}) = \log (1 + T) - \log (1 - T)$
397	389 396	breqtrrd	$⊢ φ \to seq 0 (+ H) ⇝ \log (\frac{1 + T}{1 - T})$

Metamath Proof Explorer

Theorem stirlinglem5

Proof