wallispi2

Description: An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to prove Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

		Ref	Expression
	Hypothesis	wallispi2.1	$⊢ V = (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1})$
	Assertion	wallispi2	$⊢ V ⇝ (\frac{π}{2})$

Proof

Step	Hyp	Ref	Expression
1		wallispi2.1	$⊢ V = (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1})$
2		eqid	$⊢ (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1})) = (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))$
3		1cnd	$⊢ n \in ℕ \to 1 \in ℂ$
4		2cnd	$⊢ n \in ℕ \to 2 \in ℂ$
5		nncn	$⊢ n \in ℕ \to n \in ℂ$
6	4 5	mulcld	$⊢ n \in ℕ \to 2 n \in ℂ$
7	6 3	addcld	$⊢ n \in ℕ \to 2 n + 1 \in ℂ$
8		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
9	8	biimpi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
10		eqidd	$⊢ m \in (1 \dots n) \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) = (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})$
11		simpr	$⊢ (m \in (1 \dots n) \land k = m) \to k = m$
12	11	oveq2d	$⊢ (m \in (1 \dots n) \land k = m) \to 2 k = 2 m$
13	12	oveq1d	$⊢ (m \in (1 \dots n) \land k = m) \to {2 k}^{4} = {2 m}^{4}$
14	12	oveq1d	$⊢ (m \in (1 \dots n) \land k = m) \to 2 k - 1 = 2 m - 1$
15	12 14	oveq12d	$⊢ (m \in (1 \dots n) \land k = m) \to 2 k (2 k - 1) = 2 m (2 m - 1)$
16	15	oveq1d	$⊢ (m \in (1 \dots n) \land k = m) \to {2 k (2 k - 1)}^{2} = {2 m (2 m - 1)}^{2}$
17	13 16	oveq12d	$⊢ (m \in (1 \dots n) \land k = m) \to \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}} = \frac{{2 m}^{4}}{{2 m (2 m - 1)}^{2}}$
18		elfznn	$⊢ m \in (1 \dots n) \to m \in ℕ$
19		2cnd	$⊢ m \in (1 \dots n) \to 2 \in ℂ$
20	18	nncnd	$⊢ m \in (1 \dots n) \to m \in ℂ$
21	19 20	mulcld	$⊢ m \in (1 \dots n) \to 2 m \in ℂ$
22		4nn0	$⊢ 4 \in ℕ_{0}$
23	22	a1i	$⊢ m \in (1 \dots n) \to 4 \in ℕ_{0}$
24	21 23	expcld	$⊢ m \in (1 \dots n) \to {2 m}^{4} \in ℂ$
25		1cnd	$⊢ m \in (1 \dots n) \to 1 \in ℂ$
26	21 25	subcld	$⊢ m \in (1 \dots n) \to 2 m - 1 \in ℂ$
27	21 26	mulcld	$⊢ m \in (1 \dots n) \to 2 m (2 m - 1) \in ℂ$
28	27	sqcld	$⊢ m \in (1 \dots n) \to {2 m (2 m - 1)}^{2} \in ℂ$
29		2ne0	$⊢ 2 \neq 0$
30	29	a1i	$⊢ m \in (1 \dots n) \to 2 \neq 0$
31	18	nnne0d	$⊢ m \in (1 \dots n) \to m \neq 0$
32	19 20 30 31	mulne0d	$⊢ m \in (1 \dots n) \to 2 m \neq 0$
33		1red	$⊢ m \in (1 \dots n) \to 1 \in ℝ$
34		2re	$⊢ 2 \in ℝ$
35	34	a1i	$⊢ m \in (1 \dots n) \to 2 \in ℝ$
36	35 33	remulcld	$⊢ m \in (1 \dots n) \to 2 \cdot 1 \in ℝ$
37	18	nnred	$⊢ m \in (1 \dots n) \to m \in ℝ$
38	35 37	remulcld	$⊢ m \in (1 \dots n) \to 2 m \in ℝ$
39		1lt2	$⊢ 1 < 2$
40	39	a1i	$⊢ m \in (1 \dots n) \to 1 < 2$
41		2t1e2	$⊢ 2 \cdot 1 = 2$
42	40 41	breqtrrdi	$⊢ m \in (1 \dots n) \to 1 < 2 \cdot 1$
43		0le2	$⊢ 0 \leq 2$
44	43	a1i	$⊢ m \in (1 \dots n) \to 0 \leq 2$
45		elfzle1	$⊢ m \in (1 \dots n) \to 1 \leq m$
46	33 37 35 44 45	lemul2ad	$⊢ m \in (1 \dots n) \to 2 \cdot 1 \leq 2 m$
47	33 36 38 42 46	ltletrd	$⊢ m \in (1 \dots n) \to 1 < 2 m$
48	33 47	gtned	$⊢ m \in (1 \dots n) \to 2 m \neq 1$
49	21 25 48	subne0d	$⊢ m \in (1 \dots n) \to 2 m - 1 \neq 0$
50	21 26 32 49	mulne0d	$⊢ m \in (1 \dots n) \to 2 m (2 m - 1) \neq 0$
51		2z	$⊢ 2 \in ℤ$
52	51	a1i	$⊢ m \in (1 \dots n) \to 2 \in ℤ$
53	27 50 52	expne0d	$⊢ m \in (1 \dots n) \to {2 m (2 m - 1)}^{2} \neq 0$
54	24 28 53	divcld	$⊢ m \in (1 \dots n) \to \frac{{2 m}^{4}}{{2 m (2 m - 1)}^{2}} \in ℂ$
55	10 17 18 54	fvmptd	$⊢ m \in (1 \dots n) \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (m) = \frac{{2 m}^{4}}{{2 m (2 m - 1)}^{2}}$
56	55 54	eqeltrd	$⊢ m \in (1 \dots n) \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (m) \in ℂ$
57	56	adantl	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (m) \in ℂ$
58		mulcl	$⊢ (m \in ℂ \land w \in ℂ) \to m w \in ℂ$
59	58	adantl	$⊢ (n \in ℕ \land (m \in ℂ \land w \in ℂ)) \to m w \in ℂ$
60	9 57 59	seqcl	$⊢ n \in ℕ \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n) \in ℂ$
61		2nn	$⊢ 2 \in ℕ$
62	61	a1i	$⊢ n \in ℕ \to 2 \in ℕ$
63		id	$⊢ n \in ℕ \to n \in ℕ$
64	62 63	nnmulcld	$⊢ n \in ℕ \to 2 n \in ℕ$
65	64	peano2nnd	$⊢ n \in ℕ \to 2 n + 1 \in ℕ$
66	65	nnne0d	$⊢ n \in ℕ \to 2 n + 1 \neq 0$
67	3 7 60 66	div32d	$⊢ n \in ℕ \to (\frac{1}{2 n + 1}) seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n) = 1 (\frac{seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)}{2 n + 1})$
68	60 7 66	divcld	$⊢ n \in ℕ \to \frac{seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)}{2 n + 1} \in ℂ$
69	68	mullidd	$⊢ n \in ℕ \to 1 (\frac{seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)}{2 n + 1}) = \frac{seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)}{2 n + 1}$
70		wallispi2lem2	$⊢ n \in ℕ \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n) = \frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}$
71	70	oveq1d	$⊢ n \in ℕ \to \frac{seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)}{2 n + 1} = \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1}$
72	67 69 71	3eqtrd	$⊢ n \in ℕ \to (\frac{1}{2 n + 1}) seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n) = \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1}$
73	72	mpteq2ia	$⊢ (n \in ℕ ⟼ (\frac{1}{2 n + 1}) seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)) = (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1})$
74		wallispi2lem1	$⊢ n \in ℕ \to seq 1 (\times (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))) (n) = (\frac{1}{2 n + 1}) seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n)$
75	74	mpteq2ia	$⊢ (n \in ℕ ⟼ seq 1 (\times (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))) (n)) = (n \in ℕ ⟼ (\frac{1}{2 n + 1}) seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (n))$
76	73 75 1	3eqtr4ri	$⊢ V = (n \in ℕ ⟼ seq 1 (\times (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))) (n))$
77	2 76	wallispi	$⊢ V ⇝ (\frac{π}{2})$

Metamath Proof Explorer

Theorem wallispi2

Proof