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 ffvelrnda ( ( ⊤ ∧ 𝑗 ∈ ℕ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 mulid1d ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · 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 ffvelrnda ( ( ( ⊤ ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ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 addid1d ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( ( arctan ‘ ( 1 − ( 1 / 𝑛 ) ) ) + 0 ) = ( arctan ‘ ( 1 − ( 1 / 𝑛 ) ) ) )
319 314 318 syl5eq ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( ( 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 ffvelrni ( 𝑗 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ‘ 𝑗 ) ∈ ℂ )
332 331 mulid1d ( 𝑗 ∈ ℕ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 )