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 ⊢ ∑ n ∈ ℕ 0 − 1 n 2 ⁢ n + 1 = π 4

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
2 0zd ⊢ ⊤ → 0 ∈ ℤ
3 oveq2 ⊢ k = n → − 1 k = − 1 n
4 oveq2 ⊢ k = n → 2 ⁢ k = 2 ⁢ n
5 4 oveq1d ⊢ k = n → 2 ⁢ k + 1 = 2 ⁢ n + 1
6 3 5 oveq12d ⊢ k = n → − 1 k 2 ⁢ k + 1 = − 1 n 2 ⁢ n + 1
7 eqid ⊢ k ∈ ℕ 0 ⟼ − 1 k 2 ⁢ k + 1 = k ∈ ℕ 0 ⟼ − 1 k 2 ⁢ k + 1
8 ovex ⊢ − 1 n 2 ⁢ n + 1 ∈ V
9 6 7 8 fvmpt ⊢ n ∈ ℕ 0 → k ∈ ℕ 0 ⟼ − 1 k 2 ⁢ k + 1 ⁡ n = − 1 n 2 ⁢ n + 1
10 9 adantl ⊢ ⊤ ∧ n ∈ ℕ 0 → k ∈ ℕ 0 ⟼ − 1 k 2 ⁢ k + 1 ⁡ n = − 1 n 2 ⁢ n + 1
11 neg1rr ⊢ − 1 ∈ ℝ
12 reexpcl ⊢ − 1 ∈ ℝ ∧ n ∈ ℕ 0 → − 1 n ∈ ℝ
13 11 12 mpan ⊢ n ∈ ℕ 0 → − 1 n ∈ ℝ
14 2nn0 ⊢ 2 ∈ ℕ 0
15 nn0mulcl ⊢ 2 ∈ ℕ 0 ∧ n ∈ ℕ 0 → 2 ⁢ n ∈ ℕ 0
16 14 15 mpan ⊢ n ∈ ℕ 0 → 2 ⁢ n ∈ ℕ 0
17 nn0p1nn ⊢ 2 ⁢ n ∈ ℕ 0 → 2 ⁢ n + 1 ∈ ℕ
18 16 17 syl ⊢ n ∈ ℕ 0 → 2 ⁢ n + 1 ∈ ℕ
19 13 18 nndivred ⊢ n ∈ ℕ 0 → − 1 n 2 ⁢ n + 1 ∈ ℝ
20 19 recnd ⊢ n ∈ ℕ 0 → − 1 n 2 ⁢ n + 1 ∈ ℂ
21 20 adantl ⊢ ⊤ ∧ n ∈ ℕ 0 → − 1 n 2 ⁢ n + 1 ∈ ℂ
22 7 leibpi ⊢ seq 0 + k ∈ ℕ 0 ⟼ − 1 k 2 ⁢ k + 1 ⇝ π 4
23 22 a1i ⊢ ⊤ → seq 0 + k ∈ ℕ 0 ⟼ − 1 k 2 ⁢ k + 1 ⇝ π 4
24 1 2 10 21 23 isumclim ⊢ ⊤ → ∑ n ∈ ℕ 0 − 1 n 2 ⁢ n + 1 = π 4
25 24 mptru ⊢ ∑ n ∈ ℕ 0 − 1 n 2 ⁢ n + 1 = π 4