Theorem 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	⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
Assertion	wallispi2	⊢ 𝑉 ⇝ ( π / 2 )

Proof

Step	Hyp	Ref	Expression
1		wallispi2.1	⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
2		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
3		1cnd	⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℂ )
4		2cnd	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
5		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
6	4 5	mulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℂ )
7	6 3	addcld	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
8		elnnuz	⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
9	8	biimpi	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
10		eqidd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) )
11		simpr	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → 𝑘 = 𝑚 )
12	11	oveq2d	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → ( 2 · 𝑘 ) = ( 2 · 𝑚 ) )
13	12	oveq1d	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → ( ( 2 · 𝑘 ) ↑ 4 ) = ( ( 2 · 𝑚 ) ↑ 4 ) )
14	12	oveq1d	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 𝑚 ) − 1 ) )
15	12 14	oveq12d	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) = ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) )
16	15	oveq1d	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) = ( ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ↑ 2 ) )
17	13 16	oveq12d	⊢ ( ( 𝑚 ∈ ( 1 ... 𝑛 ) ∧ 𝑘 = 𝑚 ) → ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 · 𝑚 ) ↑ 4 ) / ( ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ↑ 2 ) ) )
18		elfznn	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 𝑚 ∈ ℕ )
19		2cnd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 2 ∈ ℂ )
20	18	nncnd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 𝑚 ∈ ℂ )
21	19 20	mulcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 2 · 𝑚 ) ∈ ℂ )
22		4nn0	⊢ 4 ∈ ℕ0
23	22	a1i	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 4 ∈ ℕ0 )
24	21 23	expcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 2 · 𝑚 ) ↑ 4 ) ∈ ℂ )
25		1cnd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 1 ∈ ℂ )
26	21 25	subcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 2 · 𝑚 ) − 1 ) ∈ ℂ )
27	21 26	mulcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ∈ ℂ )
28	27	sqcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ↑ 2 ) ∈ ℂ )
29		2ne0	⊢ 2 ≠ 0
30	29	a1i	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 2 ≠ 0 )
31	18	nnne0d	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 𝑚 ≠ 0 )
32	19 20 30 31	mulne0d	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 2 · 𝑚 ) ≠ 0 )
33		1red	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 1 ∈ ℝ )
34		2re	⊢ 2 ∈ ℝ
35	34	a1i	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 2 ∈ ℝ )
36	35 33	remulcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 2 · 1 ) ∈ ℝ )
37	18	nnred	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 𝑚 ∈ ℝ )
38	35 37	remulcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 2 · 𝑚 ) ∈ ℝ )
39		1lt2	⊢ 1 < 2
40	39	a1i	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 1 < 2 )
41		2t1e2	⊢ ( 2 · 1 ) = 2
42	40 41	breqtrrdi	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 1 < ( 2 · 1 ) )
43		0le2	⊢ 0 ≤ 2
44	43	a1i	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 0 ≤ 2 )
45		elfzle1	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 1 ≤ 𝑚 )
46	33 37 35 44 45	lemul2ad	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 2 · 1 ) ≤ ( 2 · 𝑚 ) )
47	33 36 38 42 46	ltletrd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 1 < ( 2 · 𝑚 ) )
48	33 47	gtned	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 2 · 𝑚 ) ≠ 1 )
49	21 25 48	subne0d	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 2 · 𝑚 ) − 1 ) ≠ 0 )
50	21 26 32 49	mulne0d	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ≠ 0 )
51		2z	⊢ 2 ∈ ℤ
52	51	a1i	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → 2 ∈ ℤ )
53	27 50 52	expne0d	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ↑ 2 ) ≠ 0 )
54	24 28 53	divcld	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( ( 2 · 𝑚 ) ↑ 4 ) / ( ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ↑ 2 ) ) ∈ ℂ )
55	10 17 18 54	fvmptd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 𝑚 ) = ( ( ( 2 · 𝑚 ) ↑ 4 ) / ( ( ( 2 · 𝑚 ) · ( ( 2 · 𝑚 ) − 1 ) ) ↑ 2 ) ) )
56	55 54	eqeltrd	⊢ ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 𝑚 ) ∈ ℂ )
57	56	adantl	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 𝑚 ) ∈ ℂ )
58		mulcl	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑚 · 𝑤 ) ∈ ℂ )
59	58	adantl	⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑚 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑚 · 𝑤 ) ∈ ℂ )
60	9 57 59	seqcl	⊢ ( 𝑛 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
61		2nn	⊢ 2 ∈ ℕ
62	61	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ )
63		id	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
64	62 63	nnmulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℕ )
65	64	peano2nnd	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
66	65	nnne0d	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
67	3 7 60 66	div32d	⊢ ( 𝑛 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) ) = ( 1 · ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ) )
68	60 7 66	divcld	⊢ ( 𝑛 ∈ ℕ → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
69	68	mullidd	⊢ ( 𝑛 ∈ ℕ → ( 1 · ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) )
70		wallispi2lem2	⊢ ( 𝑛 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) = ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) )
71	70	oveq1d	⊢ ( 𝑛 ∈ ℕ → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) = ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
72	67 69 71	3eqtrd	⊢ ( 𝑛 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) ) = ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
73	72	mpteq2ia	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
74		wallispi2lem1	⊢ ( 𝑛 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) ‘ 𝑛 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) ) )
75	74	mpteq2ia	⊢ ( 𝑛 ∈ ℕ ↦ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑛 ) ) )
76	73 75 1	3eqtr4ri	⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) ‘ 𝑛 ) )
77	2 76	wallispi	⊢ 𝑉 ⇝ ( π / 2 )