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	$$⊢\sum _{n\in {\mathbb{N}}_0}\left(\frac{{\left(-1\right)}^n}{2n+1}\right)=\frac{\mathrm{\pi }}{4}$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		0zd	$$⊢\top \to 0\in \mathbb{Z}$$
3		oveq2	$$⊢k=n\to {\left(-1\right)}^k={\left(-1\right)}^n$$
4		oveq2	$$⊢k=n\to 2k=2n$$
5	4	oveq1d	$$⊢k=n\to 2k+1=2n+1$$
6	3 5	oveq12d	$$⊢k=n\to \frac{{\left(-1\right)}^k}{2k+1}=\frac{{\left(-1\right)}^n}{2n+1}$$
7		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^k}{2k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^k}{2k+1}\right)$$
8		ovex	$$⊢\frac{{\left(-1\right)}^n}{2n+1}\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢n\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^k}{2k+1}\right)\left(n\right)=\frac{{\left(-1\right)}^n}{2n+1}$$
10	9	adantl	$$⊢\left(\top \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^k}{2k+1}\right)\left(n\right)=\frac{{\left(-1\right)}^n}{2n+1}$$
11		neg1rr	$$⊢-1\in ℝ$$
12		reexpcl	$$⊢\left(-1\in ℝ\wedge n\in {\mathbb{N}}_0\right)\to {\left(-1\right)}^n\in ℝ$$
13	11 12	mpan	$$⊢n\in {\mathbb{N}}_0\to {\left(-1\right)}^n\in ℝ$$
14		2nn0	$$⊢2\in {\mathbb{N}}_0$$
15		nn0mulcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to 2n\in {\mathbb{N}}_0$$
16	14 15	mpan	$$⊢n\in {\mathbb{N}}_0\to 2n\in {\mathbb{N}}_0$$
17		nn0p1nn	$$⊢2n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
18	16 17	syl	$$⊢n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
19	13 18	nndivred	$$⊢n\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^n}{2n+1}\in ℝ$$
20	19	recnd	$$⊢n\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^n}{2n+1}\in ℂ$$
21	20	adantl	$$⊢\left(\top \wedge n\in {\mathbb{N}}_0\right)\to \frac{{\left(-1\right)}^n}{2n+1}\in ℂ$$
22	7	leibpi	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^k}{2k+1}\right)\right)⇝\left(\frac{\mathrm{\pi }}{4}\right)$$
23	22	a1i	$$⊢\top \to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^k}{2k+1}\right)\right)⇝\left(\frac{\mathrm{\pi }}{4}\right)$$
24	1 2 10 21 23	isumclim	$$⊢\top \to \sum _{n\in {\mathbb{N}}_0}\left(\frac{{\left(-1\right)}^n}{2n+1}\right)=\frac{\mathrm{\pi }}{4}$$
25	24	mptru	$$⊢\sum _{n\in {\mathbb{N}}_0}\left(\frac{{\left(-1\right)}^n}{2n+1}\right)=\frac{\mathrm{\pi }}{4}$$