Metamath Proof Explorer

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 )