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 )