Theorem leibpilem2

Description: The Leibniz formula for _pi . (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	leibpi.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^n}{2n+1}\right)$$
	leibpilem2.2	$$⊢G=\left(k\in {\mathbb{N}}_0⟼if\left(\left(k=0\vee 2\parallel k\right),0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)$$
	leibpilem2.3	$$⊢A\in \mathrm{V}$$
Assertion	leibpilem2	$$⊢seq0\left(+,F\right)⇝A\leftrightarrow seq0\left(+,G\right)⇝A$$

Proof

Step	Hyp	Ref	Expression
1		leibpi.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^n}{2n+1}\right)$$
2		leibpilem2.2	$$⊢G=\left(k\in {\mathbb{N}}_0⟼if\left(\left(k=0\vee 2\parallel k\right),0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)$$
3		leibpilem2.3	$$⊢A\in \mathrm{V}$$
4		2cn	$$⊢2\in ℂ$$
5		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
6		mulcl	$$⊢\left(2\in ℂ\wedge n\in ℂ\right)\to 2n\in ℂ$$
7	4 5 6	sylancr	$$⊢n\in {\mathbb{N}}_0\to 2n\in ℂ$$
8		ax-1cn	$$⊢1\in ℂ$$
9		pncan	$$⊢\left(2n\in ℂ\wedge 1\in ℂ\right)\to 2n+1-1=2n$$
10	7 8 9	sylancl	$$⊢n\in {\mathbb{N}}_0\to 2n+1-1=2n$$
11	10	oveq1d	$$⊢n\in {\mathbb{N}}_0\to \frac{2n+1-1}{2}=\frac{2n}{2}$$
12		2ne0	$$⊢2\ne 0$$
13		divcan3	$$⊢\left(n\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{2n}{2}=n$$
14	4 12 13	mp3an23	$$⊢n\in ℂ\to \frac{2n}{2}=n$$
15	5 14	syl	$$⊢n\in {\mathbb{N}}_0\to \frac{2n}{2}=n$$
16	11 15	eqtrd	$$⊢n\in {\mathbb{N}}_0\to \frac{2n+1-1}{2}=n$$
17	16	oveq2d	$$⊢n\in {\mathbb{N}}_0\to {\left(-1\right)}^{\frac{2n+1-1}{2}}={\left(-1\right)}^n$$
18	17	oveq1d	$$⊢n\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}=\frac{{\left(-1\right)}^n}{2n+1}$$
19	18	mpteq2ia	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^n}{2n+1}\right)$$
20	1 19	eqtr4i	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)$$
21		seqeq3	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)\to seq0\left(+,F\right)=seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)\right)$$
22	20 21	ax-mp	$$⊢seq0\left(+,F\right)=seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)\right)$$
23	22	breq1i	$$⊢seq0\left(+,F\right)⇝A\leftrightarrow seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)\right)⇝A$$
24		neg1rr	$$⊢-1\in ℝ$$
25		reexpcl	$$⊢\left(-1\in ℝ\wedge n\in {\mathbb{N}}_0\right)\to {\left(-1\right)}^n\in ℝ$$
26	24 25	mpan	$$⊢n\in {\mathbb{N}}_0\to {\left(-1\right)}^n\in ℝ$$
27		2nn0	$$⊢2\in {\mathbb{N}}_0$$
28		nn0mulcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to 2n\in {\mathbb{N}}_0$$
29	27 28	mpan	$$⊢n\in {\mathbb{N}}_0\to 2n\in {\mathbb{N}}_0$$
30		nn0p1nn	$$⊢2n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
31	29 30	syl	$$⊢n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
32	26 31	nndivred	$$⊢n\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^n}{2n+1}\in ℝ$$
33	32	recnd	$$⊢n\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^n}{2n+1}\in ℂ$$
34	18 33	eqeltrd	$$⊢n\in {\mathbb{N}}_0\to \frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\in ℂ$$
35	34	adantl	$$⊢\left(\top \wedge n\in {\mathbb{N}}_0\right)\to \frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\in ℂ$$
36		oveq1	$$⊢k=2n+1\to k-1=2n+1-1$$
37	36	oveq1d	$$⊢k=2n+1\to \frac{k-1}{2}=\frac{2n+1-1}{2}$$
38	37	oveq2d	$$⊢k=2n+1\to {\left(-1\right)}^{\frac{k-1}{2}}={\left(-1\right)}^{\frac{2n+1-1}{2}}$$
39		id	$$⊢k=2n+1\to k=2n+1$$
40	38 39	oveq12d	$$⊢k=2n+1\to \frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}=\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}$$
41	35 40	iserodd	$$⊢\top \to \left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)\right)⇝A\leftrightarrow seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)⇝A\right)$$
42	41	mptru	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{{\left(-1\right)}^{\frac{2n+1-1}{2}}}{2n+1}\right)\right)⇝A\leftrightarrow seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)⇝A$$
43		addlid	$$⊢n\in ℂ\to 0+n=n$$
44	43	adantl	$$⊢\left(\top \wedge n\in ℂ\right)\to 0+n=n$$
45		0cnd	$$⊢\top \to 0\in ℂ$$
46		1eluzge0	$$⊢1\in {\mathbb{Z}}_{\ge 0}$$
47	46	a1i	$$⊢\top \to 1\in {\mathbb{Z}}_{\ge 0}$$
48		1nn0	$$⊢1\in {\mathbb{N}}_0$$
49		0cnd	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(k=0\vee 2\parallel k\right)\right)\to 0\in ℂ$$
50		ioran	$$⊢\neg \left(k=0\vee 2\parallel k\right)\leftrightarrow \left(\neg k=0\wedge \neg 2\parallel k\right)$$
51		leibpilem1	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(\neg k=0\wedge \neg 2\parallel k\right)\right)\to \left(k\in \mathbb{N}\wedge \frac{k-1}{2}\in {\mathbb{N}}_0\right)$$
52	51	simprd	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(\neg k=0\wedge \neg 2\parallel k\right)\right)\to \frac{k-1}{2}\in {\mathbb{N}}_0$$
53		reexpcl	$$⊢\left(-1\in ℝ\wedge \frac{k-1}{2}\in {\mathbb{N}}_0\right)\to {\left(-1\right)}^{\frac{k-1}{2}}\in ℝ$$
54	24 52 53	sylancr	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(\neg k=0\wedge \neg 2\parallel k\right)\right)\to {\left(-1\right)}^{\frac{k-1}{2}}\in ℝ$$
55	51	simpld	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(\neg k=0\wedge \neg 2\parallel k\right)\right)\to k\in \mathbb{N}$$
56	54 55	nndivred	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(\neg k=0\wedge \neg 2\parallel k\right)\right)\to \frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\in ℝ$$
57	56	recnd	$$⊢\left(k\in {\mathbb{N}}_0\wedge \left(\neg k=0\wedge \neg 2\parallel k\right)\right)\to \frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\in ℂ$$
58	50 57	sylan2b	$$⊢\left(k\in {\mathbb{N}}_0\wedge \neg \left(k=0\vee 2\parallel k\right)\right)\to \frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\in ℂ$$
59	49 58	ifclda	$$⊢k\in {\mathbb{N}}_0\to if\left(\left(k=0\vee 2\parallel k\right),0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\in ℂ$$
60	2 59	fmpti	$$⊢G:{\mathbb{N}}_0⟶ℂ$$
61	60	ffvelcdmi	$$⊢1\in {\mathbb{N}}_0\to G\left(1\right)\in ℂ$$
62	48 61	mp1i	$$⊢\top \to G\left(1\right)\in ℂ$$
63		simpr	$$⊢\left(\top \wedge n\in \left(0\dots 1-1\right)\right)\to n\in \left(0\dots 1-1\right)$$
64		1m1e0	$$⊢1-1=0$$
65	64	oveq2i	$$⊢\left(0\dots 1-1\right)=\left(0\dots 0\right)$$
66	63 65	eleqtrdi	$$⊢\left(\top \wedge n\in \left(0\dots 1-1\right)\right)\to n\in \left(0\dots 0\right)$$
67		elfz1eq	$$⊢n\in \left(0\dots 0\right)\to n=0$$
68	66 67	syl	$$⊢\left(\top \wedge n\in \left(0\dots 1-1\right)\right)\to n=0$$
69	68	fveq2d	$$⊢\left(\top \wedge n\in \left(0\dots 1-1\right)\right)\to G\left(n\right)=G\left(0\right)$$
70		0nn0	$$⊢0\in {\mathbb{N}}_0$$
71		iftrue	$$⊢\left(k=0\vee 2\parallel k\right)\to if\left(\left(k=0\vee 2\parallel k\right),0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)=0$$
72	71	orcs	$$⊢k=0\to if\left(\left(k=0\vee 2\parallel k\right),0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)=0$$
73		c0ex	$$⊢0\in \mathrm{V}$$
74	72 2 73	fvmpt	$$⊢0\in {\mathbb{N}}_0\to G\left(0\right)=0$$
75	70 74	ax-mp	$$⊢G\left(0\right)=0$$
76	69 75	eqtrdi	$$⊢\left(\top \wedge n\in \left(0\dots 1-1\right)\right)\to G\left(n\right)=0$$
77	44 45 47 62 76	seqid	$$⊢\top \to {seq0\left(+,G\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}=seq1\left(+,G\right)$$
78		1zzd	$$⊢\top \to 1\in \mathbb{Z}$$
79		simpr	$$⊢\left(\top \wedge n\in {\mathbb{Z}}_{\ge 1}\right)\to n\in {\mathbb{Z}}_{\ge 1}$$
80		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
81	79 80	eleqtrrdi	$$⊢\left(\top \wedge n\in {\mathbb{Z}}_{\ge 1}\right)\to n\in \mathbb{N}$$
82		nnne0	$$⊢n\in \mathbb{N}\to n\ne 0$$
83	82	neneqd	$$⊢n\in \mathbb{N}\to \neg n=0$$
84		biorf	$$⊢\neg n=0\to \left(2\parallel n\leftrightarrow \left(n=0\vee 2\parallel n\right)\right)$$
85	83 84	syl	$$⊢n\in \mathbb{N}\to \left(2\parallel n\leftrightarrow \left(n=0\vee 2\parallel n\right)\right)$$
86	85	ifbid	$$⊢n\in \mathbb{N}\to if\left(2\parallel n,0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)=if\left(\left(n=0\vee 2\parallel n\right),0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)$$
87		breq2	$$⊢k=n\to \left(2\parallel k\leftrightarrow 2\parallel n\right)$$
88		oveq1	$$⊢k=n\to k-1=n-1$$
89	88	oveq1d	$$⊢k=n\to \frac{k-1}{2}=\frac{n-1}{2}$$
90	89	oveq2d	$$⊢k=n\to {\left(-1\right)}^{\frac{k-1}{2}}={\left(-1\right)}^{\frac{n-1}{2}}$$
91		id	$$⊢k=n\to k=n$$
92	90 91	oveq12d	$$⊢k=n\to \frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}=\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}$$
93	87 92	ifbieq2d	$$⊢k=n\to if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)=if\left(2\parallel n,0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)$$
94		eqid	$$⊢\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)=\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)$$
95		ovex	$$⊢\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\in \mathrm{V}$$
96	73 95	ifex	$$⊢if\left(2\parallel n,0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)\in \mathrm{V}$$
97	93 94 96	fvmpt	$$⊢n\in \mathbb{N}\to \left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\left(n\right)=if\left(2\parallel n,0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)$$
98		nnnn0	$$⊢n\in \mathbb{N}\to n\in {\mathbb{N}}_0$$
99		eqeq1	$$⊢k=n\to \left(k=0\leftrightarrow n=0\right)$$
100	99 87	orbi12d	$$⊢k=n\to \left(\left(k=0\vee 2\parallel k\right)\leftrightarrow \left(n=0\vee 2\parallel n\right)\right)$$
101	100 92	ifbieq2d	$$⊢k=n\to if\left(\left(k=0\vee 2\parallel k\right),0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)=if\left(\left(n=0\vee 2\parallel n\right),0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)$$
102	73 95	ifex	$$⊢if\left(\left(n=0\vee 2\parallel n\right),0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)\in \mathrm{V}$$
103	101 2 102	fvmpt	$$⊢n\in {\mathbb{N}}_0\to G\left(n\right)=if\left(\left(n=0\vee 2\parallel n\right),0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)$$
104	98 103	syl	$$⊢n\in \mathbb{N}\to G\left(n\right)=if\left(\left(n=0\vee 2\parallel n\right),0,\frac{{\left(-1\right)}^{\frac{n-1}{2}}}{n}\right)$$
105	86 97 104	3eqtr4d	$$⊢n\in \mathbb{N}\to \left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\left(n\right)=G\left(n\right)$$
106	81 105	syl	$$⊢\left(\top \wedge n\in {\mathbb{Z}}_{\ge 1}\right)\to \left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\left(n\right)=G\left(n\right)$$
107	78 106	seqfeq	$$⊢\top \to seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)=seq1\left(+,G\right)$$
108	77 107	eqtr4d	$$⊢\top \to {seq0\left(+,G\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}=seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)$$
109	108	mptru	$$⊢{seq0\left(+,G\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}=seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)$$
110	109	breq1i	$$⊢\left({seq0\left(+,G\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}\right)⇝A\leftrightarrow seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)⇝A$$
111		1z	$$⊢1\in \mathbb{Z}$$
112		seqex	$$⊢seq0\left(+,G\right)\in \mathrm{V}$$
113		climres	$$⊢\left(1\in \mathbb{Z}\wedge seq0\left(+,G\right)\in \mathrm{V}\right)\to \left(\left({seq0\left(+,G\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}\right)⇝A\leftrightarrow seq0\left(+,G\right)⇝A\right)$$
114	111 112 113	mp2an	$$⊢\left({seq0\left(+,G\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}\right)⇝A\leftrightarrow seq0\left(+,G\right)⇝A$$
115	110 114	bitr3i	$$⊢seq1\left(+,\left(k\in \mathbb{N}⟼if\left(2\parallel k,0,\frac{{\left(-1\right)}^{\frac{k-1}{2}}}{k}\right)\right)\right)⇝A\leftrightarrow seq0\left(+,G\right)⇝A$$
116	23 42 115	3bitri	$$⊢seq0\left(+,F\right)⇝A\leftrightarrow seq0\left(+,G\right)⇝A$$