leibpi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > leibpi		Structured version Visualization version GIF version

Theorem leibpi 24469

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

**Hypothesis**
Ref	Expression
leibpi.1	⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))

**Assertion**
Ref	Expression
leibpi	⊢ seq0( + , 𝐹) ⇝ (π / 4)

Proof of Theorem leibpi Dummy variables 𝑗 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 11598	. . . . 5 ⊢ ℕ₀ = (ℤ_≥‘0)
2		0zd 11266	. . . . 5 ⊢ (⊤ → 0 ∈ ℤ)
3		eqidd 2611	. . . . 5 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
4		0cnd 9912	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → 0 ∈ ℂ)
5		ioran 510	. . . . . . . . . 10 ⊢ (¬ (𝑘 = 0 ∨ 2 ∥ 𝑘) ↔ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘))
6		neg1rr 11002	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℝ
7		leibpilem1 24467	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ₀ ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (𝑘 ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀))
8	7	simprd 478	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((𝑘 − 1) / 2) ∈ ℕ₀)
9		reexpcl 12739	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℝ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀) → (-1↑((𝑘 − 1) / 2)) ∈ ℝ)
10	6, 8, 9	sylancr 694	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℝ)
11	7	simpld 474	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℕ)
12	10, 11	nndivred 10946	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℝ)
13	12	recnd 9947	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℂ)
14	5, 13	sylan2b 491	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ ¬ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℂ)
15	4, 14	ifclda 4070	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ₀ → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ ℂ)
16	15	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ ℂ)
17		eqid 2610	. . . . . . 7 ⊢ (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))) = (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
18	16, 17	fmptd 6292	. . . . . 6 ⊢ (⊤ → (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))):ℕ₀⟶ℂ)
19	18	ffvelrnda 6267	. . . . 5 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∈ ℂ)
20		2nn0 11186	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
21	20	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 2 ∈ ℕ₀)
22		nn0mulcl 11206	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀) → (2 · 𝑛) ∈ ℕ₀)
23	21, 22	sylan 487	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ₀) → (2 · 𝑛) ∈ ℕ₀)
24		nn0p1nn 11209	. . . . . . . . . . . 12 ⊢ ((2 · 𝑛) ∈ ℕ₀ → ((2 · 𝑛) + 1) ∈ ℕ)
25	23, 24	syl 17	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ₀) → ((2 · 𝑛) + 1) ∈ ℕ)
26	25	nnrecred 10943	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ₀) → (1 / ((2 · 𝑛) + 1)) ∈ ℝ)
27		eqid 2610	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))
28	26, 27	fmptd 6292	. . . . . . . . 9 ⊢ (⊤ → (𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1))):ℕ₀⟶ℝ)
29		nn0mulcl 11206	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℕ₀)
30	21, 29	sylan 487	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℕ₀)
31	30	nn0red 11229	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℝ)
32		peano2nn0 11210	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
33	32	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℕ₀)
34		nn0mulcl 11206	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ₀ ∧ (𝑘 + 1) ∈ ℕ₀) → (2 · (𝑘 + 1)) ∈ ℕ₀)
35	20, 33, 34	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (2 · (𝑘 + 1)) ∈ ℕ₀)
36	35	nn0red 11229	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (2 · (𝑘 + 1)) ∈ ℝ)
37		1red 9934	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 1 ∈ ℝ)
38		nn0re 11178	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
39	38	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℝ)
40	39	lep1d 10834	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 𝑘 ≤ (𝑘 + 1))
41		peano2re 10088	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
42	39, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 1) ∈ ℝ)
43		2re 10967	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
44	43	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 2 ∈ ℝ)
45		2pos 10989	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
46	45	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 0 < 2)
47		lemul2 10755	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘 ≤ (𝑘 + 1) ↔ (2 · 𝑘) ≤ (2 · (𝑘 + 1))))
48	39, 42, 44, 46, 47	syl112anc 1322	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (𝑘 ≤ (𝑘 + 1) ↔ (2 · 𝑘) ≤ (2 · (𝑘 + 1))))
49	40, 48	mpbid 221	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ≤ (2 · (𝑘 + 1)))
50	31, 36, 37, 49	leadd1dd 10520	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · 𝑘) + 1) ≤ ((2 · (𝑘 + 1)) + 1))
51		nn0p1nn 11209	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑘) ∈ ℕ₀ → ((2 · 𝑘) + 1) ∈ ℕ)
52	30, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · 𝑘) + 1) ∈ ℕ)
53	52	nnred 10912	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · 𝑘) + 1) ∈ ℝ)
54	52	nngt0d 10941	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 0 < ((2 · 𝑘) + 1))
55		nn0p1nn 11209	. . . . . . . . . . . . . 14 ⊢ ((2 · (𝑘 + 1)) ∈ ℕ₀ → ((2 · (𝑘 + 1)) + 1) ∈ ℕ)
56	35, 55	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · (𝑘 + 1)) + 1) ∈ ℕ)
57	56	nnred 10912	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · (𝑘 + 1)) + 1) ∈ ℝ)
58	56	nngt0d 10941	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → 0 < ((2 · (𝑘 + 1)) + 1))
59		lerec 10785	. . . . . . . . . . . 12 ⊢ (((((2 · 𝑘) + 1) ∈ ℝ ∧ 0 < ((2 · 𝑘) + 1)) ∧ (((2 · (𝑘 + 1)) + 1) ∈ ℝ ∧ 0 < ((2 · (𝑘 + 1)) + 1))) → (((2 · 𝑘) + 1) ≤ ((2 · (𝑘 + 1)) + 1) ↔ (1 / ((2 · (𝑘 + 1)) + 1)) ≤ (1 / ((2 · 𝑘) + 1))))
60	53, 54, 57, 58, 59	syl22anc 1319	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (((2 · 𝑘) + 1) ≤ ((2 · (𝑘 + 1)) + 1) ↔ (1 / ((2 · (𝑘 + 1)) + 1)) ≤ (1 / ((2 · 𝑘) + 1))))
61	50, 60	mpbid 221	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (1 / ((2 · (𝑘 + 1)) + 1)) ≤ (1 / ((2 · 𝑘) + 1)))
62		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑘 + 1) → (2 · 𝑛) = (2 · (𝑘 + 1)))
63	62	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → ((2 · 𝑛) + 1) = ((2 · (𝑘 + 1)) + 1))
64	63	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑘 + 1) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · (𝑘 + 1)) + 1)))
65		ovex 6577	. . . . . . . . . . . 12 ⊢ (1 / ((2 · (𝑘 + 1)) + 1)) ∈ V
66	64, 27, 65	fvmpt 6191	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘(𝑘 + 1)) = (1 / ((2 · (𝑘 + 1)) + 1)))
67	33, 66	syl 17	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘(𝑘 + 1)) = (1 / ((2 · (𝑘 + 1)) + 1)))
68		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
69	68	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
70	69	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
71		ovex 6577	. . . . . . . . . . . 12 ⊢ (1 / ((2 · 𝑘) + 1)) ∈ V
72	70, 27, 71	fvmpt 6191	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) = (1 / ((2 · 𝑘) + 1)))
73	72	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) = (1 / ((2 · 𝑘) + 1)))
74	61, 67, 73	3brtr4d 4615	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘(𝑘 + 1)) ≤ ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘))
75		nnuz 11599	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
76		1zzd 11285	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ ℤ)
77		ax-1cn 9873	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
78		divcnv 14424	. . . . . . . . . . 11 ⊢ (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
79	77, 78	mp1i 13	. . . . . . . . . 10 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
80		nn0ex 11175	. . . . . . . . . . . 12 ⊢ ℕ₀ ∈ V
81	80	mptex 6390	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
82	81	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V)
83		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
84		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
85		ovex 6577	. . . . . . . . . . . . 13 ⊢ (1 / 𝑘) ∈ V
86	83, 84, 85	fvmpt 6191	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
87	86	adantl 481	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
88		nnrecre 10934	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
89	88	adantl 481	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℝ)
90	87, 89	eqeltrd 2688	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℝ)
91		nnnn0 11176	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
92	91	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
93	92, 72	syl 17	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) = (1 / ((2 · 𝑘) + 1)))
94	91, 52	sylan2 490	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
95	94	nnrecred 10943	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
96	93, 95	eqeltrd 2688	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) ∈ ℝ)
97		nnre 10904	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
98	97	adantl 481	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
99	20, 92, 29	sylancr 694	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ₀)
100	99	nn0red 11229	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℝ)
101		peano2re 10088	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑘) ∈ ℝ → ((2 · 𝑘) + 1) ∈ ℝ)
102	100, 101	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℝ)
103		nn0addge1 11216	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → 𝑘 ≤ (𝑘 + 𝑘))
104	98, 92, 103	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (𝑘 + 𝑘))
105	98	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
106	105	2timesd 11152	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
107	104, 106	breqtrrd 4611	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · 𝑘))
108	100	lep1d 10834	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
109	98, 100, 102, 107, 108	letrd 10073	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ ((2 · 𝑘) + 1))
110		nngt0 10926	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 0 < 𝑘)
111	110	adantl 481	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 < 𝑘)
112	94	nnred 10912	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℝ)
113	94	nngt0d 10941	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 < ((2 · 𝑘) + 1))
114		lerec 10785	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℝ ∧ 0 < 𝑘) ∧ (((2 · 𝑘) + 1) ∈ ℝ ∧ 0 < ((2 · 𝑘) + 1))) → (𝑘 ≤ ((2 · 𝑘) + 1) ↔ (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘)))
115	98, 111, 112, 113, 114	syl22anc 1319	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ ((2 · 𝑘) + 1) ↔ (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘)))
116	109, 115	mpbid 221	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
117	116, 93, 87	3brtr4d 4615	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘))
118	94	nnrpd 11746	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℝ⁺)
119	118	rpreccld 11758	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / ((2 · 𝑘) + 1)) ∈ ℝ⁺)
120	119	rpge0d 11752	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / ((2 · 𝑘) + 1)))
121	120, 93	breqtrrd 4611	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘))
122	75, 76, 79, 82, 90, 96, 117, 121	climsqz2 14220	. . . . . . . . 9 ⊢ (⊤ → (𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1))) ⇝ 0)
123		neg1cn 11001	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → -1 ∈ ℂ)
125		expcl 12740	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℂ)
126	124, 125	sylan 487	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℂ)
127	52	nncnd 10913	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · 𝑘) + 1) ∈ ℂ)
128	52	nnne0d 10942	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((2 · 𝑘) + 1) ≠ 0)
129	126, 127, 128	divrecd 10683	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((-1↑𝑘) / ((2 · 𝑘) + 1)) = ((-1↑𝑘) · (1 / ((2 · 𝑘) + 1))))
130		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (-1↑𝑛) = (-1↑𝑘))
131	130, 69	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → ((-1↑𝑛) / ((2 · 𝑛) + 1)) = ((-1↑𝑘) / ((2 · 𝑘) + 1)))
132		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))
133		ovex 6577	. . . . . . . . . . . 12 ⊢ ((-1↑𝑘) / ((2 · 𝑘) + 1)) ∈ V
134	131, 132, 133	fvmpt 6191	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))‘𝑘) = ((-1↑𝑘) / ((2 · 𝑘) + 1)))
135	134	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))‘𝑘) = ((-1↑𝑘) / ((2 · 𝑘) + 1)))
136	73	oveq2d 6565	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((-1↑𝑘) · ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘)) = ((-1↑𝑘) · (1 / ((2 · 𝑘) + 1))))
137	129, 135, 136	3eqtr4d 2654	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))‘𝑘) = ((-1↑𝑘) · ((𝑛 ∈ ℕ₀ ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘)))
138	1, 2, 28, 74, 122, 137	iseralt 14263	. . . . . . . 8 ⊢ (⊤ → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ∈ dom ⇝ )
139		climdm 14133	. . . . . . . 8 ⊢ (seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ∈ dom ⇝ ↔ seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
140	138, 139	sylib 207	. . . . . . 7 ⊢ (⊤ → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
141		fvex 6113	. . . . . . . 8 ⊢ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))) ∈ V
142	132, 17, 141	leibpilem2 24468	. . . . . . 7 ⊢ (seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))) ↔ seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
143	140, 142	sylib 207	. . . . . 6 ⊢ (⊤ → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
144		seqex 12665	. . . . . . 7 ⊢ seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ∈ V
145	144, 141	breldm 5251	. . . . . 6 ⊢ (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))) → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ∈ dom ⇝ )
146	143, 145	syl 17	. . . . 5 ⊢ (⊤ → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ∈ dom ⇝ )
147	1, 2, 3, 19, 146	isumclim2 14331	. . . 4 ⊢ (⊤ → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
148		eqid 2610	. . . . . . . 8 ⊢ (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))) = (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)))
149	18, 146, 148	abelth2 24000	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))) ∈ ((0[,]1)–cn→ℂ))
150		nnrp 11718	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ⁺)
151	150	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ⁺)
152	151	rpreccld 11758	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ⁺)
153	152	rpred 11748	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
154	152	rpge0d 11752	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 0 ≤ (1 / 𝑛))
155		nnge1 10923	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 1 ≤ 𝑛)
156	155	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ≤ 𝑛)
157		nnre 10904	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
158	157	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
159	158	recnd 9947	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
160	159	mulid1d 9936	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (𝑛 · 1) = 𝑛)
161	156, 160	breqtrrd 4611	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ≤ (𝑛 · 1))
162		1red 9934	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℝ)
163		nngt0 10926	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
164	163	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
165		ledivmul 10778	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / 𝑛) ≤ 1 ↔ 1 ≤ (𝑛 · 1)))
166	162, 162, 158, 164, 165	syl112anc 1322	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) ≤ 1 ↔ 1 ≤ (𝑛 · 1)))
167	161, 166	mpbird 246	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ≤ 1)
168		0re 9919	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
169		1re 9918	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
170	168, 169	elicc2i 12110	. . . . . . . . . 10 ⊢ ((1 / 𝑛) ∈ (0[,]1) ↔ ((1 / 𝑛) ∈ ℝ ∧ 0 ≤ (1 / 𝑛) ∧ (1 / 𝑛) ≤ 1))
171	153, 154, 167, 170	syl3anbrc 1239	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ (0[,]1))
172		iirev 22536	. . . . . . . . 9 ⊢ ((1 / 𝑛) ∈ (0[,]1) → (1 − (1 / 𝑛)) ∈ (0[,]1))
173	171, 172	syl 17	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ (0[,]1))
174		eqid 2610	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))
175	173, 174	fmptd 6292	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶(0[,]1))
176		1cnd 9935	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℂ)
177		nnex 10903	. . . . . . . . . . 11 ⊢ ℕ ∈ V
178	177	mptex 6390	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ∈ V
179	178	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ∈ V)
180	90	recnd 9947	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
181	83	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (1 − (1 / 𝑛)) = (1 − (1 / 𝑘)))
182		ovex 6577	. . . . . . . . . . . 12 ⊢ (1 − (1 / 𝑘)) ∈ V
183	181, 174, 182	fvmpt 6191	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))‘𝑘) = (1 − (1 / 𝑘)))
184	86	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (1 − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (1 − (1 / 𝑘)))
185	183, 184	eqtr4d 2647	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))‘𝑘) = (1 − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
186	185	adantl 481	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))‘𝑘) = (1 − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
187	75, 76, 79, 176, 179, 180, 186	climsubc2 14217	. . . . . . . 8 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ⇝ (1 − 0))
188		1m0e1 11008	. . . . . . . 8 ⊢ (1 − 0) = 1
189	187, 188	syl6breq 4624	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ⇝ 1)
190		1elunit 12162	. . . . . . . 8 ⊢ 1 ∈ (0[,]1)
191	190	a1i 11	. . . . . . 7 ⊢ (⊤ → 1 ∈ (0[,]1))
192	75, 76, 149, 175, 189, 191	climcncf 22511	. . . . . 6 ⊢ (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) ⇝ ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)))‘1))
193		eqidd 2611	. . . . . . . 8 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))))
194		eqidd 2611	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))) = (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))))
195		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑥 = (1 − (1 / 𝑛)) → (𝑥↑𝑗) = ((1 − (1 / 𝑛))↑𝑗))
196	195	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑥 = (1 − (1 / 𝑛)) → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
197	196	sumeq2sdv 14282	. . . . . . . 8 ⊢ (𝑥 = (1 − (1 / 𝑛)) → Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)) = Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
198	173, 193, 194, 197	fmptco 6303	. . . . . . 7 ⊢ (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) = (𝑛 ∈ ℕ ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))))
199		0zd 11266	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 0 ∈ ℤ)
200	8	adantll 746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((𝑘 − 1) / 2) ∈ ℕ₀)
201	6, 200, 9	sylancr 694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℝ)
202	201	recnd 9947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℂ)
203	202	adantllr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℂ)
204		resubcl 10224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (1 − (1 / 𝑛)) ∈ ℝ)
205	169, 153, 204	sylancr 694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ ℝ)
206	205	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (1 − (1 / 𝑛)) ∈ ℝ)
207		simplr 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℕ₀)
208	206, 207	reexpcld 12887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℝ)
209	208	recnd 9947	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℂ)
210		nn0cn 11179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℂ)
211	210	ad2antlr 759	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℂ)
212	11	adantll 746	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℕ)
213	212	nnne0d 10942	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ≠ 0)
214	203, 209, 211, 213	div12d 10716	. . . . . . . . . . . . . . . . . 18 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) = (((1 − (1 / 𝑛))↑𝑘) · ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
215	13	adantll 746	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℂ)
216	209, 215	mulcomd 9940	. . . . . . . . . . . . . . . . . 18 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (((1 − (1 / 𝑛))↑𝑘) · ((-1↑((𝑘 − 1) / 2)) / 𝑘)) = (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
217	214, 216	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) = (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
218	5, 217	sylan2b 491	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ ¬ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) = (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
219	218	ifeq2da 4067	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))))
220	205	recnd 9947	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ ℂ)
221		expcl 12740	. . . . . . . . . . . . . . . . . 18 ⊢ (((1 − (1 / 𝑛)) ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℂ)
222	220, 221	sylan 487	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℂ)
223	222	mul02d 10113	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → (0 · ((1 − (1 / 𝑛))↑𝑘)) = 0)
224	223	ifeq1d 4054	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), (0 · ((1 − (1 / 𝑛))↑𝑘)), (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))))
225	219, 224	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), (0 · ((1 − (1 / 𝑛))↑𝑘)), (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))))
226		ovif 6635	. . . . . . . . . . . . . 14 ⊢ (if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) · ((1 − (1 / 𝑛))↑𝑘)) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), (0 · ((1 − (1 / 𝑛))↑𝑘)), (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
227	225, 226	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = (if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) · ((1 − (1 / 𝑛))↑𝑘)))
228		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
229		c0ex 9913	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
230		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) ∈ V
231	229, 230	ifex 4106	. . . . . . . . . . . . . 14 ⊢ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V
232		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))) = (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
233	232	fvmpt2 6200	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ₀ ∧ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
234	228, 231, 233	sylancl 693	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
235		ovex 6577	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ V
236	229, 235	ifex 4106	. . . . . . . . . . . . . . 15 ⊢ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ V
237	17	fvmpt2 6200	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ₀ ∧ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ V) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
238	228, 236, 237	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
239	238	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) = (if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) · ((1 − (1 / 𝑛))↑𝑘)))
240	227, 234, 239	3eqtr4d 2654	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
241	240	ralrimiva 2949	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
242		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘))
243		nffvmpt1 6111	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)
244		nffvmpt1 6111	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗)
245		nfcv 2751	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 ·
246		nfcv 2751	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((1 − (1 / 𝑛))↑𝑗)
247	244, 245, 246	nfov 6575	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))
248	243, 247	nfeq 2762	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))
249		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
250		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
251		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → ((1 − (1 / 𝑛))↑𝑘) = ((1 − (1 / 𝑛))↑𝑗))
252	250, 251	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
253	249, 252	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) ↔ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))))
254	242, 248, 253	cbvral 3143	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) ↔ ∀𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
255	241, 254	sylib 207	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
256	255	r19.21bi 2916	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
257		0cnd 9912	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → 0 ∈ ℂ)
258	208, 212	nndivred 10946	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (((1 − (1 / 𝑛))↑𝑘) / 𝑘) ∈ ℝ)
259	258	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (((1 − (1 / 𝑛))↑𝑘) / 𝑘) ∈ ℂ)
260	203, 259	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) ∈ ℂ)
261	5, 260	sylan2b 491	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) ∧ ¬ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) ∈ ℂ)
262	257, 261	ifclda 4070	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ₀) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ ℂ)
263	262, 232	fmptd 6292	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))):ℕ₀⟶ℂ)
264	263	ffvelrnda 6267	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) ∈ ℂ)
265	256, 264	eqeltrrd 2689	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ₀) → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)) ∈ ℂ)
266		0nn0 11184	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
267	266	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 0 ∈ ℕ₀)
268		0p1e1 11009	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
269		seqeq1 12666	. . . . . . . . . . . . 13 ⊢ ((0 + 1) = 1 → seq(0 + 1)( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) = seq1( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))))
270	268, 269	ax-mp 5	. . . . . . . . . . . 12 ⊢ seq(0 + 1)( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) = seq1( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))
271		1zzd 11285	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
272		elnnuz 11600	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ_≥‘1))
273		nnne0 10930	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
274	273	neneqd 2787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℕ → ¬ 𝑘 = 0)
275		biorf 419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 0 → (2 ∥ 𝑘 ↔ (𝑘 = 0 ∨ 2 ∥ 𝑘)))
276	274, 275	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → (2 ∥ 𝑘 ↔ (𝑘 = 0 ∨ 2 ∥ 𝑘)))
277	276	bicomd 212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ → ((𝑘 = 0 ∨ 2 ∥ 𝑘) ↔ 2 ∥ 𝑘))
278	277	ifbid 4058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
279	91, 231, 233	sylancl 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
280	229, 230	ifex 4106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V
281		eqid 2610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))) = (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
282	281	fvmpt2 6200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V) → ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
283	280, 282	mpan2 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
284	278, 279, 283	3eqtr4d 2654	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘))
285	284	rgen 2906	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑘 ∈ ℕ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘)
286	285	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘))
287		nfv 1830	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘)
288		nffvmpt1 6111	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)
289	243, 288	nfeq 2762	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)
290		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
291	249, 290	eqeq12d 2625	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) ↔ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)))
292	287, 289, 291	cbvral 3143	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ ℕ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) ↔ ∀𝑗 ∈ ℕ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
293	286, 292	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
294	293	r19.21bi 2916	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
295	272, 294	sylan2br 492	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘1)) → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
296	271, 295	seqfeq 12688	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) = seq1( + , (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))))
297	153, 162, 167	abssubge0d 14018	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (abs‘(1 − (1 / 𝑛))) = (1 − (1 / 𝑛)))
298		ltsubrp 11742	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ⁺) → (1 − (1 / 𝑛)) < 1)
299	169, 152, 298	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) < 1)
300	297, 299	eqbrtrd 4605	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (abs‘(1 − (1 / 𝑛))) < 1)
301	281	atantayl2 24465	. . . . . . . . . . . . . 14 ⊢ (((1 − (1 / 𝑛)) ∈ ℂ ∧ (abs‘(1 − (1 / 𝑛))) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
302	220, 300, 301	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
303	296, 302	eqbrtrd 4605	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
304	270, 303	syl5eqbr 4618	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → seq(0 + 1)( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
305	1, 267, 264, 304	clim2ser2 14234	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ ((arctan‘(1 − (1 / 𝑛))) + (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0)))
306		0z 11265	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
307		seq1 12676	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0))
308	306, 307	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0)
309		iftrue 4042	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 0 ∨ 2 ∥ 𝑘) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = 0)
310	309	orcs 408	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = 0)
311	310, 232, 229	fvmpt 6191	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0) = 0)
312	266, 311	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0) = 0
313	308, 312	eqtri 2632	. . . . . . . . . . . 12 ⊢ (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0) = 0
314	313	oveq2i 6560	. . . . . . . . . . 11 ⊢ ((arctan‘(1 − (1 / 𝑛))) + (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0)) = ((arctan‘(1 − (1 / 𝑛))) + 0)
315		atanrecl 24438	. . . . . . . . . . . . . 14 ⊢ ((1 − (1 / 𝑛)) ∈ ℝ → (arctan‘(1 − (1 / 𝑛))) ∈ ℝ)
316	205, 315	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (arctan‘(1 − (1 / 𝑛))) ∈ ℝ)
317	316	recnd 9947	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (arctan‘(1 − (1 / 𝑛))) ∈ ℂ)
318	317	addid1d 10115	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((arctan‘(1 − (1 / 𝑛))) + 0) = (arctan‘(1 − (1 / 𝑛))))
319	314, 318	syl5eq 2656	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((arctan‘(1 − (1 / 𝑛))) + (seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0)) = (arctan‘(1 − (1 / 𝑛))))
320	305, 319	breqtrd 4609	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
321	1, 199, 256, 265, 320	isumclim 14330	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)) = (arctan‘(1 − (1 / 𝑛))))
322	321	mpteq2dva 4672	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))) = (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))))
323	198, 322	eqtrd 2644	. . . . . 6 ⊢ (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗))) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))))
324		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑥↑𝑗) = (1↑𝑗))
325		nn0z 11277	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ₀ → 𝑗 ∈ ℤ)
326		1exp 12751	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℤ → (1↑𝑗) = 1)
327	325, 326	syl 17	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ₀ → (1↑𝑗) = 1)
328	324, 327	sylan9eq 2664	. . . . . . . . . . 11 ⊢ ((𝑥 = 1 ∧ 𝑗 ∈ ℕ₀) → (𝑥↑𝑗) = 1)
329	328	oveq2d 6565	. . . . . . . . . 10 ⊢ ((𝑥 = 1 ∧ 𝑗 ∈ ℕ₀) → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)) = (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · 1))
330	18	trud 1484	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))):ℕ₀⟶ℂ
331	330	ffvelrni 6266	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∈ ℂ)
332	331	mulid1d 9936	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ₀ → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · 1) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
333	332	adantl 481	. . . . . . . . . 10 ⊢ ((𝑥 = 1 ∧ 𝑗 ∈ ℕ₀) → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · 1) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
334	329, 333	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝑥 = 1 ∧ 𝑗 ∈ ℕ₀) → (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)) = ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
335	334	sumeq2dv 14281	. . . . . . . 8 ⊢ (𝑥 = 1 → Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)) = Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
336		sumex 14266	. . . . . . . 8 ⊢ Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∈ V
337	335, 148, 336	fvmpt 6191	. . . . . . 7 ⊢ (1 ∈ (0[,]1) → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)))‘1) = Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
338	190, 337	mp1i 13	. . . . . 6 ⊢ (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ₀ (((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥↑𝑗)))‘1) = Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
339	192, 323, 338	3brtr3d 4614	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
340		eqid 2610	. . . . . . . . 9 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
341		eqid 2610	. . . . . . . . 9 ⊢ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} = {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
342	340, 341	atancn 24463	. . . . . . . 8 ⊢ (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∈ ({𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}–cn→ℂ)
343	342	a1i 11	. . . . . . 7 ⊢ (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∈ ({𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}–cn→ℂ))
344		unitssre 12190	. . . . . . . . 9 ⊢ (0[,]1) ⊆ ℝ
345	340, 341	ressatans 24461	. . . . . . . . 9 ⊢ ℝ ⊆ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
346	344, 345	sstri 3577	. . . . . . . 8 ⊢ (0[,]1) ⊆ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
347		fss 5969	. . . . . . . 8 ⊢ (((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶(0[,]1) ∧ (0[,]1) ⊆ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
348	175, 346, 347	sylancl 693	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
349	345, 169	sselii 3565	. . . . . . . 8 ⊢ 1 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
350	349	a1i 11	. . . . . . 7 ⊢ (⊤ → 1 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
351	75, 76, 343, 348, 189, 350	climcncf 22511	. . . . . 6 ⊢ (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) ⇝ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1))
352	346, 173	sseldi 3566	. . . . . . 7 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
353		cncff 22504	. . . . . . . . . 10 ⊢ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∈ ({𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}–cn→ℂ) → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}):{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}⟶ℂ)
354	342, 353	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}):{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}⟶ℂ)
355	354	feqmptd 6159	. . . . . . . 8 ⊢ (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) = (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘𝑘)))
356		fvres 6117	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘𝑘) = (arctan‘𝑘))
357	356	mpteq2ia 4668	. . . . . . . 8 ⊢ (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘𝑘)) = (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ (arctan‘𝑘))
358	355, 357	syl6eq 2660	. . . . . . 7 ⊢ (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) = (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ (arctan‘𝑘)))
359		fveq2 6103	. . . . . . 7 ⊢ (𝑘 = (1 − (1 / 𝑛)) → (arctan‘𝑘) = (arctan‘(1 − (1 / 𝑛))))
360	352, 193, 358, 359	fmptco 6303	. . . . . 6 ⊢ (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))))
361		fvres 6117	. . . . . . . 8 ⊢ (1 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1) = (arctan‘1))
362	349, 361	mp1i 13	. . . . . . 7 ⊢ (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1) = (arctan‘1))
363		atan1 24455	. . . . . . 7 ⊢ (arctan‘1) = (π / 4)
364	362, 363	syl6eq 2660	. . . . . 6 ⊢ (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1) = (π / 4))
365	351, 360, 364	3brtr3d 4614	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ (π / 4))
366		climuni 14131	. . . . 5 ⊢ (((𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∧ (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ (π / 4)) → Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) = (π / 4))
367	339, 365, 366	syl2anc 691	. . . 4 ⊢ (⊤ → Σ𝑗 ∈ ℕ₀ ((𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) = (π / 4))
368	147, 367	breqtrd 4609	. . 3 ⊢ (⊤ → seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ (π / 4))
369	368	trud 1484	. 2 ⊢ seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ (π / 4)
370		leibpi.1	. . 3 ⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))
371		ovex 6577	. . 3 ⊢ (π / 4) ∈ V
372	370, 17, 371	leibpilem2 24468	. 2 ⊢ (seq0( + , 𝐹) ⇝ (π / 4) ↔ seq0( + , (𝑘 ∈ ℕ₀ ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ (π / 4))
373	369, 372	mpbir 220	1 ⊢ seq0( + , 𝐹) ⇝ (π / 4)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ⊤wtru 1476 ∈ wcel 1977 ∀wral 2896 {crab 2900 Vcvv 3173 ∖ cdif 3537 ⊆ wss 3540 ifcif 4036 class class class wbr 4583 ↦ cmpt 4643 dom cdm 5038 ↾ cres 5040 ∘ ccom 5042 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 -∞cmnf 9951 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 ℕcn 10897 2c2 10947 4c4 10949 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ℝ⁺crp 11708 (,]cioc 12047 [,]cicc 12049 seqcseq 12663 ↑cexp 12722 abscabs 13822 ⇝ cli 14063 Σcsu 14264 πcpi 14636 ∥ cdvds 14821 –cn→ccncf 22487 arctancatan 24391

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-xnn0 11241 df-z 11255 df-dec 11370 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ioc 12051 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-fl 12455 df-mod 12531 df-seq 12664 df-exp 12723 df-fac 12923 df-bc 12952 df-hash 12980 df-shft 13655 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-limsup 14050 df-clim 14067 df-rlim 14068 df-sum 14265 df-ef 14637 df-sin 14639 df-cos 14640 df-tan 14641 df-pi 14642 df-dvds 14822 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-rest 15906 df-topn 15907 df-0g 15925 df-gsum 15926 df-topgen 15927 df-pt 15928 df-prds 15931 df-xrs 15985 df-qtop 15990 df-imas 15991 df-xps 15993 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-mulg 17364 df-cntz 17573 df-cmn 18018 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-fbas 19564 df-fg 19565 df-cnfld 19568 df-top 20521 df-bases 20522 df-topon 20523 df-topsp 20524 df-cld 20633 df-ntr 20634 df-cls 20635 df-nei 20712 df-lp 20750 df-perf 20751 df-cn 20841 df-cnp 20842 df-t1 20928 df-haus 20929 df-cmp 21000 df-tx 21175 df-hmeo 21368 df-fil 21460 df-fm 21552 df-flim 21553 df-flf 21554 df-xms 21935 df-ms 21936 df-tms 21937 df-cncf 22489 df-limc 23436 df-dv 23437 df-ulm 23935 df-log 24107 df-atan 24394

This theorem is referenced by: leibpisum 24470

W3C validator