Theorem 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	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) )
Assertion	leibpi	⊢ seq 0 ( + , 𝐹 ) ⇝ ( π / 4 )

Proof

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