This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )