Step |
Hyp |
Ref |
Expression |
1 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
2 |
|
0zd |
⊢ ( ⊤ → 0 ∈ ℤ ) |
3 |
|
oveq2 |
⊢ ( 𝑘 = 𝑛 → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ 𝑛 ) ) |
4 |
|
oveq2 |
⊢ ( 𝑘 = 𝑛 → ( 2 · 𝑘 ) = ( 2 · 𝑛 ) ) |
5 |
4
|
oveq1d |
⊢ ( 𝑘 = 𝑛 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) ) |
6 |
3 5
|
oveq12d |
⊢ ( 𝑘 = 𝑛 → ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) = ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ) |
7 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) |
8 |
|
ovex |
⊢ ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ V |
9 |
6 7 8
|
fvmpt |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ‘ 𝑛 ) = ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ) |
10 |
9
|
adantl |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ‘ 𝑛 ) = ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ) |
11 |
|
neg1rr |
⊢ - 1 ∈ ℝ |
12 |
|
reexpcl |
⊢ ( ( - 1 ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑛 ) ∈ ℝ ) |
13 |
11 12
|
mpan |
⊢ ( 𝑛 ∈ ℕ0 → ( - 1 ↑ 𝑛 ) ∈ ℝ ) |
14 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
15 |
|
nn0mulcl |
⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 ) |
16 |
14 15
|
mpan |
⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℕ0 ) |
17 |
|
nn0p1nn |
⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) |
18 |
16 17
|
syl |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) |
19 |
13 18
|
nndivred |
⊢ ( 𝑛 ∈ ℕ0 → ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ ) |
20 |
19
|
recnd |
⊢ ( 𝑛 ∈ ℕ0 → ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ ) |
21 |
20
|
adantl |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ ) |
22 |
7
|
leibpi |
⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ⇝ ( π / 4 ) |
23 |
22
|
a1i |
⊢ ( ⊤ → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ⇝ ( π / 4 ) ) |
24 |
1 2 10 21 23
|
isumclim |
⊢ ( ⊤ → Σ 𝑛 ∈ ℕ0 ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) = ( π / 4 ) ) |
25 |
24
|
mptru |
⊢ Σ 𝑛 ∈ ℕ0 ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) = ( π / 4 ) |