wallispi

Description: Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	wallispi.1	$⊢ F = (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))$
	wallispi.2	$⊢ W = (n \in ℕ ⟼ seq 1 (\times F) (n))$
Assertion	wallispi	$⊢ W ⇝ (\frac{π}{2})$

Proof

Step	Hyp	Ref	Expression
1		wallispi.1	$⊢ F = (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))$
2		wallispi.2	$⊢ W = (n \in ℕ ⟼ seq 1 (\times F) (n))$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4		1zzd	$⊢ ⊤ \to 1 \in ℤ$
5		eqid	$⊢ (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x) = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
6		eqid	$⊢ (n \in ℕ ⟼ \frac{(n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x) (2 n)}{(n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x) (2 n + 1)}) = (n \in ℕ ⟼ \frac{(n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x) (2 n)}{(n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x) (2 n + 1)})$
7		eqid	$⊢ (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) = (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}))$
8		eqid	$⊢ (n \in ℕ ⟼ \frac{2 n + 1}{2 n}) = (n \in ℕ ⟼ \frac{2 n + 1}{2 n})$
9	1 5 6 7 8	wallispilem5	$⊢ (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) ⇝ 1$
10	9	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) ⇝ 1$
11		2cnd	$⊢ ⊤ \to 2 \in ℂ$
12		picn	$⊢ π \in ℂ$
13	12	a1i	$⊢ ⊤ \to π \in ℂ$
14		pire	$⊢ π \in ℝ$
15		pipos	$⊢ 0 < π$
16	14 15	gt0ne0ii	$⊢ π \neq 0$
17	16	a1i	$⊢ ⊤ \to π \neq 0$
18	11 13 17	divcld	$⊢ ⊤ \to \frac{2}{π} \in ℂ$
19		nnex	$⊢ ℕ \in V$
20	19	mptex	$⊢ (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) \in V$
21	20	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) \in V$
22	12	a1i	$⊢ n \in ℕ \to π \in ℂ$
23	22	halfcld	$⊢ n \in ℕ \to \frac{π}{2} \in ℂ$
24		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
25	24	biimpi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
26		oveq2	$⊢ k = j \to 2 k = 2 j$
27	26	oveq1d	$⊢ k = j \to 2 k - 1 = 2 j - 1$
28	26 27	oveq12d	$⊢ k = j \to \frac{2 k}{2 k - 1} = \frac{2 j}{2 j - 1}$
29	26	oveq1d	$⊢ k = j \to 2 k + 1 = 2 j + 1$
30	26 29	oveq12d	$⊢ k = j \to \frac{2 k}{2 k + 1} = \frac{2 j}{2 j + 1}$
31	28 30	oveq12d	$⊢ k = j \to (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}) = (\frac{2 j}{2 j - 1}) (\frac{2 j}{2 j + 1})$
32		elfznn	$⊢ j \in (1 \dots n) \to j \in ℕ$
33		2cnd	$⊢ j \in ℕ \to 2 \in ℂ$
34		nncn	$⊢ j \in ℕ \to j \in ℂ$
35	33 34	mulcld	$⊢ j \in ℕ \to 2 j \in ℂ$
36		1cnd	$⊢ j \in ℕ \to 1 \in ℂ$
37	35 36	subcld	$⊢ j \in ℕ \to 2 j - 1 \in ℂ$
38		1red	$⊢ j \in ℕ \to 1 \in ℝ$
39		1t1e1	$⊢ 1 \cdot 1 = 1$
40	38 38	remulcld	$⊢ j \in ℕ \to 1 \cdot 1 \in ℝ$
41		2re	$⊢ 2 \in ℝ$
42	41	a1i	$⊢ j \in ℕ \to 2 \in ℝ$
43	42 38	remulcld	$⊢ j \in ℕ \to 2 \cdot 1 \in ℝ$
44		nnre	$⊢ j \in ℕ \to j \in ℝ$
45	42 44	remulcld	$⊢ j \in ℕ \to 2 j \in ℝ$
46		1rp	$⊢ 1 \in ℝ^{+}$
47	46	a1i	$⊢ j \in ℕ \to 1 \in ℝ^{+}$
48		1lt2	$⊢ 1 < 2$
49	48	a1i	$⊢ j \in ℕ \to 1 < 2$
50	38 42 47 49	ltmul1dd	$⊢ j \in ℕ \to 1 \cdot 1 < 2 \cdot 1$
51		0le2	$⊢ 0 \leq 2$
52	51	a1i	$⊢ j \in ℕ \to 0 \leq 2$
53		nnge1	$⊢ j \in ℕ \to 1 \leq j$
54	38 44 42 52 53	lemul2ad	$⊢ j \in ℕ \to 2 \cdot 1 \leq 2 j$
55	40 43 45 50 54	ltletrd	$⊢ j \in ℕ \to 1 \cdot 1 < 2 j$
56	39 55	eqbrtrrid	$⊢ j \in ℕ \to 1 < 2 j$
57	38 56	gtned	$⊢ j \in ℕ \to 2 j \neq 1$
58	35 36 57	subne0d	$⊢ j \in ℕ \to 2 j - 1 \neq 0$
59	35 37 58	divcld	$⊢ j \in ℕ \to \frac{2 j}{2 j - 1} \in ℂ$
60	35 36	addcld	$⊢ j \in ℕ \to 2 j + 1 \in ℂ$
61		0red	$⊢ j \in ℕ \to 0 \in ℝ$
62	45 38	readdcld	$⊢ j \in ℕ \to 2 j + 1 \in ℝ$
63	47	rpgt0d	$⊢ j \in ℕ \to 0 < 1$
64		2rp	$⊢ 2 \in ℝ^{+}$
65	64	a1i	$⊢ j \in ℕ \to 2 \in ℝ^{+}$
66		nnrp	$⊢ j \in ℕ \to j \in ℝ^{+}$
67	65 66	rpmulcld	$⊢ j \in ℕ \to 2 j \in ℝ^{+}$
68	38 67	ltaddrp2d	$⊢ j \in ℕ \to 1 < 2 j + 1$
69	61 38 62 63 68	lttrd	$⊢ j \in ℕ \to 0 < 2 j + 1$
70	61 69	gtned	$⊢ j \in ℕ \to 2 j + 1 \neq 0$
71	35 60 70	divcld	$⊢ j \in ℕ \to \frac{2 j}{2 j + 1} \in ℂ$
72	59 71	mulcld	$⊢ j \in ℕ \to (\frac{2 j}{2 j - 1}) (\frac{2 j}{2 j + 1}) \in ℂ$
73	32 72	syl	$⊢ j \in (1 \dots n) \to (\frac{2 j}{2 j - 1}) (\frac{2 j}{2 j + 1}) \in ℂ$
74	1 31 32 73	fvmptd3	$⊢ j \in (1 \dots n) \to F (j) = (\frac{2 j}{2 j - 1}) (\frac{2 j}{2 j + 1})$
75	64	a1i	$⊢ j \in (1 \dots n) \to 2 \in ℝ^{+}$
76	32	nnrpd	$⊢ j \in (1 \dots n) \to j \in ℝ^{+}$
77	75 76	rpmulcld	$⊢ j \in (1 \dots n) \to 2 j \in ℝ^{+}$
78	45 38	resubcld	$⊢ j \in ℕ \to 2 j - 1 \in ℝ$
79		1m1e0	$⊢ 1 - 1 = 0$
80	38 45 38 56	ltsub1dd	$⊢ j \in ℕ \to 1 - 1 < 2 j - 1$
81	79 80	eqbrtrrid	$⊢ j \in ℕ \to 0 < 2 j - 1$
82	78 81	elrpd	$⊢ j \in ℕ \to 2 j - 1 \in ℝ^{+}$
83	32 82	syl	$⊢ j \in (1 \dots n) \to 2 j - 1 \in ℝ^{+}$
84	77 83	rpdivcld	$⊢ j \in (1 \dots n) \to \frac{2 j}{2 j - 1} \in ℝ^{+}$
85	41	a1i	$⊢ j \in (1 \dots n) \to 2 \in ℝ$
86	32	nnred	$⊢ j \in (1 \dots n) \to j \in ℝ$
87	85 86	remulcld	$⊢ j \in (1 \dots n) \to 2 j \in ℝ$
88	75	rpge0d	$⊢ j \in (1 \dots n) \to 0 \leq 2$
89	76	rpge0d	$⊢ j \in (1 \dots n) \to 0 \leq j$
90	85 86 88 89	mulge0d	$⊢ j \in (1 \dots n) \to 0 \leq 2 j$
91	87 90	ge0p1rpd	$⊢ j \in (1 \dots n) \to 2 j + 1 \in ℝ^{+}$
92	77 91	rpdivcld	$⊢ j \in (1 \dots n) \to \frac{2 j}{2 j + 1} \in ℝ^{+}$
93	84 92	rpmulcld	$⊢ j \in (1 \dots n) \to (\frac{2 j}{2 j - 1}) (\frac{2 j}{2 j + 1}) \in ℝ^{+}$
94	74 93	eqeltrd	$⊢ j \in (1 \dots n) \to F (j) \in ℝ^{+}$
95	94	adantl	$⊢ (n \in ℕ \land j \in (1 \dots n)) \to F (j) \in ℝ^{+}$
96		rpmulcl	$⊢ (j \in ℝ^{+} \land w \in ℝ^{+}) \to j w \in ℝ^{+}$
97	96	adantl	$⊢ (n \in ℕ \land (j \in ℝ^{+} \land w \in ℝ^{+})) \to j w \in ℝ^{+}$
98	25 95 97	seqcl	$⊢ n \in ℕ \to seq 1 (\times F) (n) \in ℝ^{+}$
99	98	rpcnd	$⊢ n \in ℕ \to seq 1 (\times F) (n) \in ℂ$
100	98	rpne0d	$⊢ n \in ℕ \to seq 1 (\times F) (n) \neq 0$
101	99 100	reccld	$⊢ n \in ℕ \to \frac{1}{seq 1 (\times F) (n)} \in ℂ$
102	23 101	mulcld	$⊢ n \in ℕ \to (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}) \in ℂ$
103	7 102	fmpti	$⊢ (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) : ℕ ⟶ ℂ$
104	103	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) : ℕ ⟶ ℂ$
105	104	ffvelcdmda	$⊢ (⊤ \land j \in ℕ) \to (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) (j) \in ℂ$
106		fveq2	$⊢ n = j \to seq 1 (\times F) (n) = seq 1 (\times F) (j)$
107	106	eleq1d	$⊢ n = j \to (seq 1 (\times F) (n) \in ℝ^{+} \leftrightarrow seq 1 (\times F) (j) \in ℝ^{+})$
108	107 98	vtoclga	$⊢ j \in ℕ \to seq 1 (\times F) (j) \in ℝ^{+}$
109	108	rpcnd	$⊢ j \in ℕ \to seq 1 (\times F) (j) \in ℂ$
110	108	rpne0d	$⊢ j \in ℕ \to seq 1 (\times F) (j) \neq 0$
111	36 109 110	divrecd	$⊢ j \in ℕ \to \frac{1}{seq 1 (\times F) (j)} = 1 (\frac{1}{seq 1 (\times F) (j)})$
112	12	a1i	$⊢ j \in ℕ \to π \in ℂ$
113	65	rpne0d	$⊢ j \in ℕ \to 2 \neq 0$
114	16	a1i	$⊢ j \in ℕ \to π \neq 0$
115	33 112 113 114	divcan6d	$⊢ j \in ℕ \to (\frac{2}{π}) (\frac{π}{2}) = 1$
116	115	eqcomd	$⊢ j \in ℕ \to 1 = (\frac{2}{π}) (\frac{π}{2})$
117	116	oveq1d	$⊢ j \in ℕ \to 1 (\frac{1}{seq 1 (\times F) (j)}) = (\frac{2}{π}) (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)})$
118	33 112 114	divcld	$⊢ j \in ℕ \to \frac{2}{π} \in ℂ$
119	112	halfcld	$⊢ j \in ℕ \to \frac{π}{2} \in ℂ$
120	109 110	reccld	$⊢ j \in ℕ \to \frac{1}{seq 1 (\times F) (j)} \in ℂ$
121	118 119 120	mulassd	$⊢ j \in ℕ \to (\frac{2}{π}) (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)}) = (\frac{2}{π}) (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)})$
122	111 117 121	3eqtrd	$⊢ j \in ℕ \to \frac{1}{seq 1 (\times F) (j)} = (\frac{2}{π}) (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)})$
123		eqidd	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) = (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)})$
124	106	oveq2d	$⊢ n = j \to \frac{1}{seq 1 (\times F) (n)} = \frac{1}{seq 1 (\times F) (j)}$
125	124	adantl	$⊢ (j \in ℕ \land n = j) \to \frac{1}{seq 1 (\times F) (n)} = \frac{1}{seq 1 (\times F) (j)}$
126		id	$⊢ j \in ℕ \to j \in ℕ$
127	108	rpreccld	$⊢ j \in ℕ \to \frac{1}{seq 1 (\times F) (j)} \in ℝ^{+}$
128	123 125 126 127	fvmptd	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) = \frac{1}{seq 1 (\times F) (j)}$
129		eqidd	$⊢ j \in ℕ \to (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) = (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}))$
130	125	oveq2d	$⊢ (j \in ℕ \land n = j) \to (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}) = (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)})$
131	119 120	mulcld	$⊢ j \in ℕ \to (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)}) \in ℂ$
132	129 130 126 131	fvmptd	$⊢ j \in ℕ \to (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) (j) = (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)})$
133	132	oveq2d	$⊢ j \in ℕ \to (\frac{2}{π}) (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) (j) = (\frac{2}{π}) (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (j)})$
134	122 128 133	3eqtr4d	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) = (\frac{2}{π}) (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) (j)$
135	134	adantl	$⊢ (⊤ \land j \in ℕ) \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) = (\frac{2}{π}) (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)})) (j)$
136	3 4 10 18 21 105 135	climmulc2	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) ⇝ (\frac{2}{π}) \cdot 1$
137		2cn	$⊢ 2 \in ℂ$
138	137 12 16	divcli	$⊢ \frac{2}{π} \in ℂ$
139	138	mulridi	$⊢ (\frac{2}{π}) \cdot 1 = \frac{2}{π}$
140	136 139	breqtrdi	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) ⇝ (\frac{2}{π})$
141		2ne0	$⊢ 2 \neq 0$
142	137 12 141 16	divne0i	$⊢ \frac{2}{π} \neq 0$
143	142	a1i	$⊢ ⊤ \to \frac{2}{π} \neq 0$
144	128 120	eqeltrd	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \in ℂ$
145	109 110	recne0d	$⊢ j \in ℕ \to \frac{1}{seq 1 (\times F) (j)} \neq 0$
146	128 145	eqnetrd	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \neq 0$
147		nelsn	$⊢ (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \neq 0 \to \neg (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \in \{0\}$
148	146 147	syl	$⊢ j \in ℕ \to \neg (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \in \{0\}$
149	144 148	eldifd	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \in (ℂ ∖ \{0\})$
150	149	adantl	$⊢ (⊤ \land j \in ℕ) \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) \in (ℂ ∖ \{0\})$
151	109 110	recrecd	$⊢ j \in ℕ \to \frac{1}{\frac{1}{seq 1 (\times F) (j)}} = seq 1 (\times F) (j)$
152	123 125 126 120	fvmptd	$⊢ j \in ℕ \to (n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j) = \frac{1}{seq 1 (\times F) (j)}$
153	152	oveq2d	$⊢ j \in ℕ \to \frac{1}{(n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j)} = \frac{1}{\frac{1}{seq 1 (\times F) (j)}}$
154	106 2 98	fvmpt3	$⊢ j \in ℕ \to W (j) = seq 1 (\times F) (j)$
155	151 153 154	3eqtr4rd	$⊢ j \in ℕ \to W (j) = \frac{1}{(n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j)}$
156	155	adantl	$⊢ (⊤ \land j \in ℕ) \to W (j) = \frac{1}{(n \in ℕ ⟼ \frac{1}{seq 1 (\times F) (n)}) (j)}$
157	19	mptex	$⊢ (n \in ℕ ⟼ seq 1 (\times F) (n)) \in V$
158	2 157	eqeltri	$⊢ W \in V$
159	158	a1i	$⊢ ⊤ \to W \in V$
160	3 4 140 143 150 156 159	climrec	$⊢ ⊤ \to W ⇝ (\frac{1}{\frac{2}{π}})$
161	160	mptru	$⊢ W ⇝ (\frac{1}{\frac{2}{π}})$
162		recdiv	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (π \in ℂ \land π \neq 0)) \to \frac{1}{\frac{2}{π}} = \frac{π}{2}$
163	137 141 12 16 162	mp4an	$⊢ \frac{1}{\frac{2}{π}} = \frac{π}{2}$
164	161 163	breqtri	$⊢ W ⇝ (\frac{π}{2})$

Metamath Proof Explorer

Theorem wallispi

Proof