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 ) |