Metamath Proof Explorer


Theorem leibpisum

Description: The Leibniz formula for _pi . This version of leibpi looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Assertion leibpisum Σ 𝑛 ∈ ℕ0 ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) = ( π / 4 )

Proof

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 )