leibpi

Description: The Leibniz formula for _pi . This proof depends on three main facts: (1) the series F is convergent, because it is an alternating series ( iseralt ). (2) Using leibpilem2 to rewrite the series as a power series, it is the x = 1 special case of the Taylor series for arctan ( atantayl2 ). (3) Although we cannot directly plug x = 1 into atantayl2 , Abel's theorem ( abelth2 ) says that the limit along any sequence converging to 1 , such as 1 - 1 / n , of the power series converges to the power series extended to 1 , and then since arctan is continuous at 1 ( atancn ) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015)

		Ref	Expression
	Hypothesis	leibpi.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})$
	Assertion	leibpi	$⊢ seq 0 (+ F) ⇝ (\frac{π}{4})$

Proof

Step	Hyp	Ref	Expression
1		leibpi.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})$
2		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
3		0zd	$⊢ ⊤ \to 0 \in ℤ$
4		eqidd	$⊢ (⊤ \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
5		0cnd	$⊢ (k \in ℕ_{0} \land (k = 0 \lor 2 ∥ k)) \to 0 \in ℂ$
6		ioran	$⊢ \neg (k = 0 \lor 2 ∥ k) \leftrightarrow (\neg k = 0 \land \neg 2 ∥ k)$
7		neg1rr	$⊢ - 1 \in ℝ$
8		leibpilem1	$⊢ (k \in ℕ_{0} \land (\neg k = 0 \land \neg 2 ∥ k)) \to (k \in ℕ \land \frac{k - 1}{2} \in ℕ_{0})$
9	8	simprd	$⊢ (k \in ℕ_{0} \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{k - 1}{2} \in ℕ_{0}$
10		reexpcl	$⊢ (- 1 \in ℝ \land \frac{k - 1}{2} \in ℕ_{0}) \to {(- 1)}^{\frac{k - 1}{2}} \in ℝ$
11	7 9 10	sylancr	$⊢ (k \in ℕ_{0} \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} \in ℝ$
12	8	simpld	$⊢ (k \in ℕ_{0} \land (\neg k = 0 \land \neg 2 ∥ k)) \to k \in ℕ$
13	11 12	nndivred	$⊢ (k \in ℕ_{0} \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{{(- 1)}^{\frac{k - 1}{2}}}{k} \in ℝ$
14	13	recnd	$⊢ (k \in ℕ_{0} \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{{(- 1)}^{\frac{k - 1}{2}}}{k} \in ℂ$
15	6 14	sylan2b	$⊢ (k \in ℕ_{0} \land \neg (k = 0 \lor 2 ∥ k)) \to \frac{{(- 1)}^{\frac{k - 1}{2}}}{k} \in ℂ$
16	5 15	ifclda	$⊢ k \in ℕ_{0} \to if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) \in ℂ$
17	16	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) \in ℂ$
18	17	fmpttd	$⊢ ⊤ \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) : ℕ_{0} ⟶ ℂ$
19	18	ffvelrnda	$⊢ (⊤ \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \in ℂ$
20		2nn0	$⊢ 2 \in ℕ_{0}$
21	20	a1i	$⊢ ⊤ \to 2 \in ℕ_{0}$
22		nn0mulcl	$⊢ (2 \in ℕ_{0} \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
23	21 22	sylan	$⊢ (⊤ \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
24		nn0p1nn	$⊢ 2 n \in ℕ_{0} \to 2 n + 1 \in ℕ$
25	23 24	syl	$⊢ (⊤ \land n \in ℕ_{0}) \to 2 n + 1 \in ℕ$
26	25	nnrecred	$⊢ (⊤ \land n \in ℕ_{0}) \to \frac{1}{2 n + 1} \in ℝ$
27	26	fmpttd	$⊢ ⊤ \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) : ℕ_{0} ⟶ ℝ$
28		nn0mulcl	$⊢ (2 \in ℕ_{0} \land k \in ℕ_{0}) \to 2 k \in ℕ_{0}$
29	21 28	sylan	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k \in ℕ_{0}$
30	29	nn0red	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k \in ℝ$
31		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
32	31	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
33		nn0mulcl	$⊢ (2 \in ℕ_{0} \land k + 1 \in ℕ_{0}) \to 2 (k + 1) \in ℕ_{0}$
34	20 32 33	sylancr	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 (k + 1) \in ℕ_{0}$
35	34	nn0red	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 (k + 1) \in ℝ$
36		1red	$⊢ (⊤ \land k \in ℕ_{0}) \to 1 \in ℝ$
37		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
38	37	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to k \in ℝ$
39	38	lep1d	$⊢ (⊤ \land k \in ℕ_{0}) \to k \leq k + 1$
40		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
41	38 40	syl	$⊢ (⊤ \land k \in ℕ_{0}) \to k + 1 \in ℝ$
42		2re	$⊢ 2 \in ℝ$
43	42	a1i	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 \in ℝ$
44		2pos	$⊢ 0 < 2$
45	44	a1i	$⊢ (⊤ \land k \in ℕ_{0}) \to 0 < 2$
46		lemul2	$⊢ (k \in ℝ \land k + 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (k \leq k + 1 \leftrightarrow 2 k \leq 2 (k + 1))$
47	38 41 43 45 46	syl112anc	$⊢ (⊤ \land k \in ℕ_{0}) \to (k \leq k + 1 \leftrightarrow 2 k \leq 2 (k + 1))$
48	39 47	mpbid	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k \leq 2 (k + 1)$
49	30 35 36 48	leadd1dd	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k + 1 \leq 2 (k + 1) + 1$
50		nn0p1nn	$⊢ 2 k \in ℕ_{0} \to 2 k + 1 \in ℕ$
51	29 50	syl	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k + 1 \in ℕ$
52	51	nnred	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k + 1 \in ℝ$
53	51	nngt0d	$⊢ (⊤ \land k \in ℕ_{0}) \to 0 < 2 k + 1$
54		nn0p1nn	$⊢ 2 (k + 1) \in ℕ_{0} \to 2 (k + 1) + 1 \in ℕ$
55	34 54	syl	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 (k + 1) + 1 \in ℕ$
56	55	nnred	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 (k + 1) + 1 \in ℝ$
57	55	nngt0d	$⊢ (⊤ \land k \in ℕ_{0}) \to 0 < 2 (k + 1) + 1$
58		lerec	$⊢ ((2 k + 1 \in ℝ \land 0 < 2 k + 1) \land (2 (k + 1) + 1 \in ℝ \land 0 < 2 (k + 1) + 1)) \to (2 k + 1 \leq 2 (k + 1) + 1 \leftrightarrow \frac{1}{2 (k + 1) + 1} \leq \frac{1}{2 k + 1})$
59	52 53 56 57 58	syl22anc	$⊢ (⊤ \land k \in ℕ_{0}) \to (2 k + 1 \leq 2 (k + 1) + 1 \leftrightarrow \frac{1}{2 (k + 1) + 1} \leq \frac{1}{2 k + 1})$
60	49 59	mpbid	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{1}{2 (k + 1) + 1} \leq \frac{1}{2 k + 1}$
61		oveq2	$⊢ n = k + 1 \to 2 n = 2 (k + 1)$
62	61	oveq1d	$⊢ n = k + 1 \to 2 n + 1 = 2 (k + 1) + 1$
63	62	oveq2d	$⊢ n = k + 1 \to \frac{1}{2 n + 1} = \frac{1}{2 (k + 1) + 1}$
64		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) = (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1})$
65		ovex	$⊢ \frac{1}{2 (k + 1) + 1} \in V$
66	63 64 65	fvmpt	$⊢ k + 1 \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k + 1) = \frac{1}{2 (k + 1) + 1}$
67	32 66	syl	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k + 1) = \frac{1}{2 (k + 1) + 1}$
68		oveq2	$⊢ n = k \to 2 n = 2 k$
69	68	oveq1d	$⊢ n = k \to 2 n + 1 = 2 k + 1$
70	69	oveq2d	$⊢ n = k \to \frac{1}{2 n + 1} = \frac{1}{2 k + 1}$
71		ovex	$⊢ \frac{1}{2 k + 1} \in V$
72	70 64 71	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k) = \frac{1}{2 k + 1}$
73	72	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k) = \frac{1}{2 k + 1}$
74	60 67 73	3brtr4d	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k + 1) \leq (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k)$
75		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
76		1zzd	$⊢ ⊤ \to 1 \in ℤ$
77		ax-1cn	$⊢ 1 \in ℂ$
78		divcnv	$⊢ 1 \in ℂ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
79	77 78	mp1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
80		nn0ex	$⊢ ℕ_{0} \in V$
81	80	mptex	$⊢ (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) \in V$
82	81	a1i	$⊢ ⊤ \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) \in V$
83		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
84		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n}) = (n \in ℕ ⟼ \frac{1}{n})$
85		ovex	$⊢ \frac{1}{k} \in V$
86	83 84 85	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{1}{n}) (k) = \frac{1}{k}$
87	86	adantl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) = \frac{1}{k}$
88		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
89	88	adantl	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{k} \in ℝ$
90	87 89	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) \in ℝ$
91		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
92	91	adantl	$⊢ (⊤ \land k \in ℕ) \to k \in ℕ_{0}$
93	92 72	syl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k) = \frac{1}{2 k + 1}$
94	91 51	sylan2	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℕ$
95	94	nnrecred	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{2 k + 1} \in ℝ$
96	93 95	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k) \in ℝ$
97		nnre	$⊢ k \in ℕ \to k \in ℝ$
98	97	adantl	$⊢ (⊤ \land k \in ℕ) \to k \in ℝ$
99	20 92 28	sylancr	$⊢ (⊤ \land k \in ℕ) \to 2 k \in ℕ_{0}$
100	99	nn0red	$⊢ (⊤ \land k \in ℕ) \to 2 k \in ℝ$
101		peano2re	$⊢ 2 k \in ℝ \to 2 k + 1 \in ℝ$
102	100 101	syl	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℝ$
103		nn0addge1	$⊢ (k \in ℝ \land k \in ℕ_{0}) \to k \leq k + k$
104	98 92 103	syl2anc	$⊢ (⊤ \land k \in ℕ) \to k \leq k + k$
105	98	recnd	$⊢ (⊤ \land k \in ℕ) \to k \in ℂ$
106	105	2timesd	$⊢ (⊤ \land k \in ℕ) \to 2 k = k + k$
107	104 106	breqtrrd	$⊢ (⊤ \land k \in ℕ) \to k \leq 2 k$
108	100	lep1d	$⊢ (⊤ \land k \in ℕ) \to 2 k \leq 2 k + 1$
109	98 100 102 107 108	letrd	$⊢ (⊤ \land k \in ℕ) \to k \leq 2 k + 1$
110		nngt0	$⊢ k \in ℕ \to 0 < k$
111	110	adantl	$⊢ (⊤ \land k \in ℕ) \to 0 < k$
112	94	nnred	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℝ$
113	94	nngt0d	$⊢ (⊤ \land k \in ℕ) \to 0 < 2 k + 1$
114		lerec	$⊢ ((k \in ℝ \land 0 < k) \land (2 k + 1 \in ℝ \land 0 < 2 k + 1)) \to (k \leq 2 k + 1 \leftrightarrow \frac{1}{2 k + 1} \leq \frac{1}{k})$
115	98 111 112 113 114	syl22anc	$⊢ (⊤ \land k \in ℕ) \to (k \leq 2 k + 1 \leftrightarrow \frac{1}{2 k + 1} \leq \frac{1}{k})$
116	109 115	mpbid	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{2 k + 1} \leq \frac{1}{k}$
117	116 93 87	3brtr4d	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k) \leq (n \in ℕ ⟼ \frac{1}{n}) (k)$
118	94	nnrpd	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℝ^{+}$
119	118	rpreccld	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{2 k + 1} \in ℝ^{+}$
120	119	rpge0d	$⊢ (⊤ \land k \in ℕ) \to 0 \leq \frac{1}{2 k + 1}$
121	120 93	breqtrrd	$⊢ (⊤ \land k \in ℕ) \to 0 \leq (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k)$
122	75 76 79 82 90 96 117 121	climsqz2	$⊢ ⊤ \to (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) ⇝ 0$
123		neg1cn	$⊢ - 1 \in ℂ$
124	123	a1i	$⊢ ⊤ \to - 1 \in ℂ$
125		expcl	$⊢ (- 1 \in ℂ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℂ$
126	124 125	sylan	$⊢ (⊤ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℂ$
127	51	nncnd	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k + 1 \in ℂ$
128	51	nnne0d	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 k + 1 \neq 0$
129	126 127 128	divrecd	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{{(- 1)}^{k}}{2 k + 1} = {(- 1)}^{k} (\frac{1}{2 k + 1})$
130		oveq2	$⊢ n = k \to {(- 1)}^{n} = {(- 1)}^{k}$
131	130 69	oveq12d	$⊢ n = k \to \frac{{(- 1)}^{n}}{2 n + 1} = \frac{{(- 1)}^{k}}{2 k + 1}$
132		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}) = (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})$
133		ovex	$⊢ \frac{{(- 1)}^{k}}{2 k + 1} \in V$
134	131 132 133	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}) (k) = \frac{{(- 1)}^{k}}{2 k + 1}$
135	134	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}) (k) = \frac{{(- 1)}^{k}}{2 k + 1}$
136	73	oveq2d	$⊢ (⊤ \land k \in ℕ_{0}) \to {(- 1)}^{k} (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k) = {(- 1)}^{k} (\frac{1}{2 k + 1})$
137	129 135 136	3eqtr4d	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}) (k) = {(- 1)}^{k} (n \in ℕ_{0} ⟼ \frac{1}{2 n + 1}) (k)$
138	2 3 27 74 122 137	iseralt	$⊢ ⊤ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})) \in dom ⇝$
139		climdm	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})) \in dom ⇝ \leftrightarrow seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})) ⇝ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})))$
140	138 139	sylib	$⊢ ⊤ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})) ⇝ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})))$
141		eqid	$⊢ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))$
142		fvex	$⊢ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}))) \in V$
143	132 141 142	leibpilem2	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})) ⇝ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}))) \leftrightarrow seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})))$
144	140 143	sylib	$⊢ ⊤ \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1})))$
145		seqex	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) \in V$
146	145 142	breldm	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ ⇝ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{(- 1)}^{n}}{2 n + 1}))) \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) \in dom ⇝$
147	144 146	syl	$⊢ ⊤ \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) \in dom ⇝$
148	2 3 4 19 147	isumclim2	$⊢ ⊤ \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
149		eqid	$⊢ (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) = (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j})$
150	18 147 149	abelth2	$⊢ ⊤ \to (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) : [0, 1] \underset{cn}{⟶} ℂ$
151		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
152	151	adantl	$⊢ (⊤ \land n \in ℕ) \to n \in ℝ^{+}$
153	152	rpreccld	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
154	153	rpred	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
155	153	rpge0d	$⊢ (⊤ \land n \in ℕ) \to 0 \leq \frac{1}{n}$
156		nnge1	$⊢ n \in ℕ \to 1 \leq n$
157	156	adantl	$⊢ (⊤ \land n \in ℕ) \to 1 \leq n$
158		nnre	$⊢ n \in ℕ \to n \in ℝ$
159	158	adantl	$⊢ (⊤ \land n \in ℕ) \to n \in ℝ$
160	159	recnd	$⊢ (⊤ \land n \in ℕ) \to n \in ℂ$
161	160	mulid1d	$⊢ (⊤ \land n \in ℕ) \to n \cdot 1 = n$
162	157 161	breqtrrd	$⊢ (⊤ \land n \in ℕ) \to 1 \leq n \cdot 1$
163		1red	$⊢ (⊤ \land n \in ℕ) \to 1 \in ℝ$
164		nngt0	$⊢ n \in ℕ \to 0 < n$
165	164	adantl	$⊢ (⊤ \land n \in ℕ) \to 0 < n$
166		ledivmul	$⊢ (1 \in ℝ \land 1 \in ℝ \land (n \in ℝ \land 0 < n)) \to (\frac{1}{n} \leq 1 \leftrightarrow 1 \leq n \cdot 1)$
167	163 163 159 165 166	syl112anc	$⊢ (⊤ \land n \in ℕ) \to (\frac{1}{n} \leq 1 \leftrightarrow 1 \leq n \cdot 1)$
168	162 167	mpbird	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{n} \leq 1$
169		elicc01	$⊢ \frac{1}{n} \in [0, 1] \leftrightarrow (\frac{1}{n} \in ℝ \land 0 \leq \frac{1}{n} \land \frac{1}{n} \leq 1)$
170	154 155 168 169	syl3anbrc	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{n} \in [0, 1]$
171		iirev	$⊢ \frac{1}{n} \in [0, 1] \to 1 - (\frac{1}{n}) \in [0, 1]$
172	170 171	syl	$⊢ (⊤ \land n \in ℕ) \to 1 - (\frac{1}{n}) \in [0, 1]$
173	172	fmpttd	$⊢ ⊤ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) : ℕ ⟶ [0, 1]$
174		1cnd	$⊢ ⊤ \to 1 \in ℂ$
175		nnex	$⊢ ℕ \in V$
176	175	mptex	$⊢ (n \in ℕ ⟼ 1 - (\frac{1}{n})) \in V$
177	176	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) \in V$
178	90	recnd	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) \in ℂ$
179	83	oveq2d	$⊢ n = k \to 1 - (\frac{1}{n}) = 1 - (\frac{1}{k})$
180		eqid	$⊢ (n \in ℕ ⟼ 1 - (\frac{1}{n})) = (n \in ℕ ⟼ 1 - (\frac{1}{n}))$
181		ovex	$⊢ 1 - (\frac{1}{k}) \in V$
182	179 180 181	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) (k) = 1 - (\frac{1}{k})$
183	86	oveq2d	$⊢ k \in ℕ \to 1 - (n \in ℕ ⟼ \frac{1}{n}) (k) = 1 - (\frac{1}{k})$
184	182 183	eqtr4d	$⊢ k \in ℕ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) (k) = 1 - (n \in ℕ ⟼ \frac{1}{n}) (k)$
185	184	adantl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) (k) = 1 - (n \in ℕ ⟼ \frac{1}{n}) (k)$
186	75 76 79 174 177 178 185	climsubc2	$⊢ ⊤ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) ⇝ (1 - 0)$
187		1m0e1	$⊢ 1 - 0 = 1$
188	186 187	breqtrdi	$⊢ ⊤ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) ⇝ 1$
189		1elunit	$⊢ 1 \in [0, 1]$
190	189	a1i	$⊢ ⊤ \to 1 \in [0, 1]$
191	75 76 150 173 188 190	climcncf	$⊢ ⊤ \to ((x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) \circ (n \in ℕ ⟼ 1 - (\frac{1}{n}))) ⇝ (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) (1)$
192		eqidd	$⊢ ⊤ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) = (n \in ℕ ⟼ 1 - (\frac{1}{n}))$
193		eqidd	$⊢ ⊤ \to (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) = (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j})$
194		oveq1	$⊢ x = 1 - (\frac{1}{n}) \to x^{j} = {(1 - (\frac{1}{n}))}^{j}$
195	194	oveq2d	$⊢ x = 1 - (\frac{1}{n}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j} = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
196	195	sumeq2sdv	$⊢ x = 1 - (\frac{1}{n}) \to \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j} = \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
197	172 192 193 196	fmptco	$⊢ ⊤ \to (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) \circ (n \in ℕ ⟼ 1 - (\frac{1}{n})) = (n \in ℕ ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j})$
198		0zd	$⊢ (⊤ \land n \in ℕ) \to 0 \in ℤ$
199	9	adantll	$⊢ ((⊤ \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{k - 1}{2} \in ℕ_{0}$
200	7 199 10	sylancr	$⊢ ((⊤ \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} \in ℝ$
201	200	recnd	$⊢ ((⊤ \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} \in ℂ$
202	201	adantllr	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} \in ℂ$
203		1re	$⊢ 1 \in ℝ$
204		resubcl	$⊢ (1 \in ℝ \land \frac{1}{n} \in ℝ) \to 1 - (\frac{1}{n}) \in ℝ$
205	203 154 204	sylancr	$⊢ (⊤ \land n \in ℕ) \to 1 - (\frac{1}{n}) \in ℝ$
206	205	ad2antrr	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to 1 - (\frac{1}{n}) \in ℝ$
207		simplr	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to k \in ℕ_{0}$
208	206 207	reexpcld	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(1 - (\frac{1}{n}))}^{k} \in ℝ$
209	208	recnd	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(1 - (\frac{1}{n}))}^{k} \in ℂ$
210		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
211	210	ad2antlr	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to k \in ℂ$
212	12	adantll	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to k \in ℕ$
213	212	nnne0d	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to k \neq 0$
214	202 209 211 213	div12d	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}) = {(1 - (\frac{1}{n}))}^{k} (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k})$
215	14	adantll	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{{(- 1)}^{\frac{k - 1}{2}}}{k} \in ℂ$
216	209 215	mulcomd	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(1 - (\frac{1}{n}))}^{k} (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) = (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k}$
217	214 216	eqtrd	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}) = (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k}$
218	6 217	sylan2b	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land \neg (k = 0 \lor 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}) = (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k}$
219	218	ifeq2da	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) = if ((k = 0 \lor 2 ∥ k), 0, (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k})$
220	205	recnd	$⊢ (⊤ \land n \in ℕ) \to 1 - (\frac{1}{n}) \in ℂ$
221		expcl	$⊢ (1 - (\frac{1}{n}) \in ℂ \land k \in ℕ_{0}) \to {(1 - (\frac{1}{n}))}^{k} \in ℂ$
222	220 221	sylan	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to {(1 - (\frac{1}{n}))}^{k} \in ℂ$
223	222	mul02d	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to 0 \cdot {(1 - (\frac{1}{n}))}^{k} = 0$
224	223	ifeq1d	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to if ((k = 0 \lor 2 ∥ k), 0 \cdot {(1 - (\frac{1}{n}))}^{k}, (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k}) = if ((k = 0 \lor 2 ∥ k), 0, (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k})$
225	219 224	eqtr4d	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) = if ((k = 0 \lor 2 ∥ k), 0 \cdot {(1 - (\frac{1}{n}))}^{k}, (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k})$
226		ovif	$⊢ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k} = if ((k = 0 \lor 2 ∥ k), 0 \cdot {(1 - (\frac{1}{n}))}^{k}, (\frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k})$
227	225 226	eqtr4di	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) = if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k}$
228		simpr	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
229		c0ex	$⊢ 0 \in V$
230		ovex	$⊢ {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}) \in V$
231	229 230	ifex	$⊢ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) \in V$
232		eqid	$⊢ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))$
233	232	fvmpt2	$⊢ (k \in ℕ_{0} \land if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) \in V) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))$
234	228 231 233	sylancl	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))$
235		ovex	$⊢ \frac{{(- 1)}^{\frac{k - 1}{2}}}{k} \in V$
236	229 235	ifex	$⊢ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) \in V$
237	141	fvmpt2	$⊢ (k \in ℕ_{0} \land if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) \in V) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) = if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})$
238	228 236 237	sylancl	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) = if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})$
239	238	oveq1d	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k} = if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}) {(1 - (\frac{1}{n}))}^{k}$
240	227 234 239	3eqtr4d	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k}$
241	240	ralrimiva	$⊢ (⊤ \land n \in ℕ) \to \forall k \in ℕ_{0} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k}$
242		nfv	$⊢ Ⅎ j (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k}$
243		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
244		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
245		nfcv	$⊢ \underline{Ⅎ} k \times$
246		nfcv	$⊢ \underline{Ⅎ} k {(1 - (\frac{1}{n}))}^{j}$
247	244 245 246	nfov	$⊢ \underline{Ⅎ} k (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
248	243 247	nfeq	$⊢ Ⅎ k (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
249		fveq2	$⊢ k = j \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
250		fveq2	$⊢ k = j \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
251		oveq2	$⊢ k = j \to {(1 - (\frac{1}{n}))}^{k} = {(1 - (\frac{1}{n}))}^{j}$
252	250 251	oveq12d	$⊢ k = j \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k} = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
253	249 252	eqeq12d	$⊢ k = j \to ((k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k} \leftrightarrow (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j})$
254	242 248 253	cbvralw	$⊢ \forall k \in ℕ_{0} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (k) {(1 - (\frac{1}{n}))}^{k} \leftrightarrow \forall j \in ℕ_{0} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
255	241 254	sylib	$⊢ (⊤ \land n \in ℕ) \to \forall j \in ℕ_{0} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
256	255	r19.21bi	$⊢ ((⊤ \land n \in ℕ) \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}$
257		0cnd	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (k = 0 \lor 2 ∥ k)) \to 0 \in ℂ$
258	208 212	nndivred	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{{(1 - (\frac{1}{n}))}^{k}}{k} \in ℝ$
259	258	recnd	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to \frac{{(1 - (\frac{1}{n}))}^{k}}{k} \in ℂ$
260	202 259	mulcld	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land (\neg k = 0 \land \neg 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}) \in ℂ$
261	6 260	sylan2b	$⊢ (((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \land \neg (k = 0 \lor 2 ∥ k)) \to {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}) \in ℂ$
262	257 261	ifclda	$⊢ ((⊤ \land n \in ℕ) \land k \in ℕ_{0}) \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) \in ℂ$
263	262	fmpttd	$⊢ (⊤ \land n \in ℕ) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) : ℕ_{0} ⟶ ℂ$
264	263	ffvelrnda	$⊢ ((⊤ \land n \in ℕ) \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) \in ℂ$
265	256 264	eqeltrrd	$⊢ ((⊤ \land n \in ℕ) \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j} \in ℂ$
266		0nn0	$⊢ 0 \in ℕ_{0}$
267	266	a1i	$⊢ (⊤ \land n \in ℕ) \to 0 \in ℕ_{0}$
268		0p1e1	$⊢ 0 + 1 = 1$
269		seqeq1	$⊢ 0 + 1 = 1 \to seq (0 + 1) (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) = seq 1 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))))$
270	268 269	ax-mp	$⊢ seq (0 + 1) (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) = seq 1 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))))$
271		1zzd	$⊢ (⊤ \land n \in ℕ) \to 1 \in ℤ$
272		elnnuz	$⊢ j \in ℕ \leftrightarrow j \in ℤ_{\geq 1}$
273		nnne0	$⊢ k \in ℕ \to k \neq 0$
274	273	neneqd	$⊢ k \in ℕ \to \neg k = 0$
275		biorf	$⊢ \neg k = 0 \to (2 ∥ k \leftrightarrow (k = 0 \lor 2 ∥ k))$
276	274 275	syl	$⊢ k \in ℕ \to (2 ∥ k \leftrightarrow (k = 0 \lor 2 ∥ k))$
277	276	bicomd	$⊢ k \in ℕ \to ((k = 0 \lor 2 ∥ k) \leftrightarrow 2 ∥ k)$
278	277	ifbid	$⊢ k \in ℕ \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) = if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))$
279	91 231 233	sylancl	$⊢ k \in ℕ \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))$
280	229 230	ifex	$⊢ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) \in V$
281		eqid	$⊢ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))$
282	281	fvmpt2	$⊢ (k \in ℕ \land if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) \in V) \to (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))$
283	280 282	mpan2	$⊢ k \in ℕ \to (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))$
284	278 279 283	3eqtr4d	$⊢ k \in ℕ \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k)$
285	284	rgen	$⊢ \forall k \in ℕ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k)$
286	285	a1i	$⊢ (⊤ \land n \in ℕ) \to \forall k \in ℕ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k)$
287		nfv	$⊢ Ⅎ j (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k)$
288		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
289	243 288	nfeq	$⊢ Ⅎ k (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
290		fveq2	$⊢ k = j \to (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
291	249 290	eqeq12d	$⊢ k = j \to ((k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) \leftrightarrow (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j))$
292	287 289 291	cbvralw	$⊢ \forall k \in ℕ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (k) \leftrightarrow \forall j \in ℕ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
293	286 292	sylib	$⊢ (⊤ \land n \in ℕ) \to \forall j \in ℕ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
294	293	r19.21bi	$⊢ ((⊤ \land n \in ℕ) \land j \in ℕ) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
295	272 294	sylan2br	$⊢ ((⊤ \land n \in ℕ) \land j \in ℤ_{\geq 1}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (j)$
296	271 295	seqfeq	$⊢ (⊤ \land n \in ℕ) \to seq 1 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) = seq 1 (+ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))))$
297	154 163 168	abssubge0d	$⊢ (⊤ \land n \in ℕ) \to \|1 - (\frac{1}{n})\| = 1 - (\frac{1}{n})$
298		ltsubrp	$⊢ (1 \in ℝ \land \frac{1}{n} \in ℝ^{+}) \to 1 - (\frac{1}{n}) < 1$
299	203 153 298	sylancr	$⊢ (⊤ \land n \in ℕ) \to 1 - (\frac{1}{n}) < 1$
300	297 299	eqbrtrd	$⊢ (⊤ \land n \in ℕ) \to \|1 - (\frac{1}{n})\| < 1$
301	281	atantayl2	$⊢ (1 - (\frac{1}{n}) \in ℂ \land \|1 - (\frac{1}{n})\| < 1) \to seq 1 (+ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) ⇝ arctan (1 - (\frac{1}{n}))$
302	220 300 301	syl2anc	$⊢ (⊤ \land n \in ℕ) \to seq 1 (+ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) ⇝ arctan (1 - (\frac{1}{n}))$
303	296 302	eqbrtrd	$⊢ (⊤ \land n \in ℕ) \to seq 1 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) ⇝ arctan (1 - (\frac{1}{n}))$
304	270 303	eqbrtrid	$⊢ (⊤ \land n \in ℕ) \to seq (0 + 1) (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) ⇝ arctan (1 - (\frac{1}{n}))$
305	2 267 264 304	clim2ser2	$⊢ (⊤ \land n \in ℕ) \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) ⇝ (arctan (1 - (\frac{1}{n})) + seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) (0))$
306		0z	$⊢ 0 \in ℤ$
307		seq1	$⊢ 0 \in ℤ \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) (0) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (0)$
308	306 307	ax-mp	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) (0) = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (0)$
309		iftrue	$⊢ (k = 0 \lor 2 ∥ k) \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) = 0$
310	309	orcs	$⊢ k = 0 \to if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})) = 0$
311	310 232 229	fvmpt	$⊢ 0 \in ℕ_{0} \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (0) = 0$
312	266 311	ax-mp	$⊢ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k}))) (0) = 0$
313	308 312	eqtri	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) (0) = 0$
314	313	oveq2i	$⊢ arctan (1 - (\frac{1}{n})) + seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) (0) = arctan (1 - (\frac{1}{n})) + 0$
315		atanrecl	$⊢ 1 - (\frac{1}{n}) \in ℝ \to arctan (1 - (\frac{1}{n})) \in ℝ$
316	205 315	syl	$⊢ (⊤ \land n \in ℕ) \to arctan (1 - (\frac{1}{n})) \in ℝ$
317	316	recnd	$⊢ (⊤ \land n \in ℕ) \to arctan (1 - (\frac{1}{n})) \in ℂ$
318	317	addid1d	$⊢ (⊤ \land n \in ℕ) \to arctan (1 - (\frac{1}{n})) + 0 = arctan (1 - (\frac{1}{n}))$
319	314 318	syl5eq	$⊢ (⊤ \land n \in ℕ) \to arctan (1 - (\frac{1}{n})) + seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) (0) = arctan (1 - (\frac{1}{n}))$
320	305 319	breqtrd	$⊢ (⊤ \land n \in ℕ) \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{{(1 - (\frac{1}{n}))}^{k}}{k})))) ⇝ arctan (1 - (\frac{1}{n}))$
321	2 198 256 265 320	isumclim	$⊢ (⊤ \land n \in ℕ) \to \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j} = arctan (1 - (\frac{1}{n}))$
322	321	mpteq2dva	$⊢ ⊤ \to (n \in ℕ ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) {(1 - (\frac{1}{n}))}^{j}) = (n \in ℕ ⟼ arctan (1 - (\frac{1}{n})))$
323	197 322	eqtrd	$⊢ ⊤ \to (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) \circ (n \in ℕ ⟼ 1 - (\frac{1}{n})) = (n \in ℕ ⟼ arctan (1 - (\frac{1}{n})))$
324		oveq1	$⊢ x = 1 \to x^{j} = 1^{j}$
325		nn0z	$⊢ j \in ℕ_{0} \to j \in ℤ$
326		1exp	$⊢ j \in ℤ \to 1^{j} = 1$
327	325 326	syl	$⊢ j \in ℕ_{0} \to 1^{j} = 1$
328	324 327	sylan9eq	$⊢ (x = 1 \land j \in ℕ_{0}) \to x^{j} = 1$
329	328	oveq2d	$⊢ (x = 1 \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j} = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \cdot 1$
330	18	mptru	$⊢ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) : ℕ_{0} ⟶ ℂ$
331	330	ffvelrni	$⊢ j \in ℕ_{0} \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \in ℂ$
332	331	mulid1d	$⊢ j \in ℕ_{0} \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \cdot 1 = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
333	332	adantl	$⊢ (x = 1 \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \cdot 1 = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
334	329 333	eqtrd	$⊢ (x = 1 \land j \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j} = (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
335	334	sumeq2dv	$⊢ x = 1 \to \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j} = \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
336		sumex	$⊢ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \in V$
337	335 149 336	fvmpt	$⊢ 1 \in [0, 1] \to (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) (1) = \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
338	189 337	mp1i	$⊢ ⊤ \to (x \in [0, 1] ⟼ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) x^{j}) (1) = \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
339	191 323 338	3brtr3d	$⊢ ⊤ \to (n \in ℕ ⟼ arctan (1 - (\frac{1}{n}))) ⇝ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j)$
340		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
341		eqid	$⊢ \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} = \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
342	340 341	atancn	$⊢ ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) : \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} \underset{cn}{⟶} ℂ$
343	342	a1i	$⊢ ⊤ \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) : \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} \underset{cn}{⟶} ℂ$
344		unitssre	$⊢ [0, 1] \subseteq ℝ$
345	340 341	ressatans	$⊢ ℝ \subseteq \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
346	344 345	sstri	$⊢ [0, 1] \subseteq \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
347		fss	$⊢ ((n \in ℕ ⟼ 1 - (\frac{1}{n})) : ℕ ⟶ [0, 1] \land [0, 1] \subseteq \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}) \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) : ℕ ⟶ \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
348	173 346 347	sylancl	$⊢ ⊤ \to (n \in ℕ ⟼ 1 - (\frac{1}{n})) : ℕ ⟶ \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
349	345 203	sselii	$⊢ 1 \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
350	349	a1i	$⊢ ⊤ \to 1 \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
351	75 76 343 348 188 350	climcncf	$⊢ ⊤ \to (({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) \circ (n \in ℕ ⟼ 1 - (\frac{1}{n}))) ⇝ ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (1)$
352	346 172	sselid	$⊢ (⊤ \land n \in ℕ) \to 1 - (\frac{1}{n}) \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}$
353		cncff	$⊢ ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) : \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} \underset{cn}{⟶} ℂ \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) : \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} ⟶ ℂ$
354	342 353	mp1i	$⊢ ⊤ \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) : \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} ⟶ ℂ$
355	354	feqmptd	$⊢ ⊤ \to {arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}} = (k \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} ⟼ ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (k))$
356		fvres	$⊢ k \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (k) = arctan (k)$
357	356	mpteq2ia	$⊢ (k \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} ⟼ ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (k)) = (k \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} ⟼ arctan (k))$
358	355 357	eqtrdi	$⊢ ⊤ \to {arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}} = (k \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} ⟼ arctan (k))$
359		fveq2	$⊢ k = 1 - (\frac{1}{n}) \to arctan (k) = arctan (1 - (\frac{1}{n}))$
360	352 192 358 359	fmptco	$⊢ ⊤ \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) \circ (n \in ℕ ⟼ 1 - (\frac{1}{n})) = (n \in ℕ ⟼ arctan (1 - (\frac{1}{n})))$
361		fvres	$⊢ 1 \in \{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\} \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (1) = arctan (1)$
362	349 361	mp1i	$⊢ ⊤ \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (1) = arctan (1)$
363		atan1	$⊢ arctan (1) = \frac{π}{4}$
364	362 363	eqtrdi	$⊢ ⊤ \to ({arctan ↾}_{\{x \in ℂ \| 1 + x^{2} \in (ℂ ∖ (−∞, 0])\}}) (1) = \frac{π}{4}$
365	351 360 364	3brtr3d	$⊢ ⊤ \to (n \in ℕ ⟼ arctan (1 - (\frac{1}{n}))) ⇝ (\frac{π}{4})$
366		climuni	$⊢ ((n \in ℕ ⟼ arctan (1 - (\frac{1}{n}))) ⇝ \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) \land (n \in ℕ ⟼ arctan (1 - (\frac{1}{n}))) ⇝ (\frac{π}{4})) \to \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) = \frac{π}{4}$
367	339 365 366	syl2anc	$⊢ ⊤ \to \sum_{j \in ℕ_{0}} (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k})) (j) = \frac{π}{4}$
368	148 367	breqtrd	$⊢ ⊤ \to seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ (\frac{π}{4})$
369	368	mptru	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ (\frac{π}{4})$
370		ovex	$⊢ \frac{π}{4} \in V$
371	1 141 370	leibpilem2	$⊢ seq 0 (+ F) ⇝ (\frac{π}{4}) \leftrightarrow seq 0 (+ (k \in ℕ_{0} ⟼ if ((k = 0 \lor 2 ∥ k), 0, \frac{{(- 1)}^{\frac{k - 1}{2}}}{k}))) ⇝ (\frac{π}{4})$
372	369 371	mpbir	$⊢ seq 0 (+ F) ⇝ (\frac{π}{4})$

Metamath Proof Explorer

Theorem leibpi

Proof