Metamath Proof Explorer

Theorem stirlinglem14

Description: The sequence A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem14.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem14.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
Assertion stirlinglem14 ∃ 𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐

Proof

Step Hyp Ref Expression
1 stirlinglem14.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 stirlinglem14.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3 1 2 stirlinglem13 ⊢ ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑
4 simpl ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → 𝑑 ∈ ℝ )
5 4 rpefcld ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → ( exp ‘ 𝑑 ) ∈ ℝ+ )
6 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
7 1zzd ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → 1 ∈ ℤ )
8 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
9 8 a1i ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → exp ∈ ( ℂ –cn→ ℂ ) )
10 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
11 faccl ⊢ ( 𝑛 ∈ ℕ0 → ( ! ‘ 𝑛 ) ∈ ℕ )
12 nncn ⊢ ( ( ! ‘ 𝑛 ) ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℂ )
13 10 11 12 3syl ⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℂ )
14 2cnd ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
15 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
16 14 15 mulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℂ )
17 16 sqrtcld ⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( 2 · 𝑛 ) ) ∈ ℂ )
18 epr ⊢ e ∈ ℝ+
19 rpcn ⊢ ( e ∈ ℝ+ → e ∈ ℂ )
20 18 19 ax-mp ⊢ e ∈ ℂ
21 20 a1i ⊢ ( 𝑛 ∈ ℕ → e ∈ ℂ )
22 0re ⊢ 0 ∈ ℝ
23 epos ⊢ 0 < e
24 22 23 gtneii ⊢ e ≠ 0
25 24 a1i ⊢ ( 𝑛 ∈ ℕ → e ≠ 0 )
26 15 21 25 divcld ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ∈ ℂ )
27 26 10 expcld ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ∈ ℂ )
28 17 27 mulcld ⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℂ )
29 2rp ⊢ 2 ∈ ℝ+
30 29 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ+ )
31 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
32 30 31 rpmulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ+ )
33 32 sqrtgt0d ⊢ ( 𝑛 ∈ ℕ → 0 < ( √ ‘ ( 2 · 𝑛 ) ) )
34 33 gt0ne0d ⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( 2 · 𝑛 ) ) ≠ 0 )
35 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
36 15 21 35 25 divne0d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ≠ 0 )
37 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
38 26 36 37 expne0d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ≠ 0 )
39 17 27 34 38 mulne0d ⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ≠ 0 )
40 13 28 39 divcld ⊢ ( 𝑛 ∈ ℕ → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ )
41 1 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ ) → ( 𝐴 ‘ 𝑛 ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
42 40 41 mpdan ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
43 42 40 eqeltrd ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
44 nnne0 ⊢ ( ( ! ‘ 𝑛 ) ∈ ℕ → ( ! ‘ 𝑛 ) ≠ 0 )
45 10 11 44 3syl ⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ≠ 0 )
46 13 28 45 39 divne0d ⊢ ( 𝑛 ∈ ℕ → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ≠ 0 )
47 42 46 eqnetrd ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) ≠ 0 )
48 43 47 logcld ⊢ ( 𝑛 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℂ )
49 2 48 fmpti ⊢ 𝐵 : ℕ ⟶ ℂ
50 49 a1i ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → 𝐵 : ℕ ⟶ ℂ )
51 simpr ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → 𝐵 ⇝ 𝑑 )
52 4 recnd ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → 𝑑 ∈ ℂ )
53 6 7 9 50 51 52 climcncf ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → ( exp ∘ 𝐵 ) ⇝ ( exp ‘ 𝑑 ) )
54 8 elexi ⊢ exp ∈ V
55 nnex ⊢ ℕ ∈ V
56 55 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ) ∈ V
57 2 56 eqeltri ⊢ 𝐵 ∈ V
58 54 57 coex ⊢ ( exp ∘ 𝐵 ) ∈ V
59 58 a1i ⊢ ( ⊤ → ( exp ∘ 𝐵 ) ∈ V )
60 55 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ∈ V
61 1 60 eqeltri ⊢ 𝐴 ∈ V
62 61 a1i ⊢ ( ⊤ → 𝐴 ∈ V )
63 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
64 2 funmpt2 ⊢ Fun 𝐵
65 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
66 rabid2 ⊢ ( ℕ = { 𝑛 ∈ ℕ ∣ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V } ↔ ∀ 𝑛 ∈ ℕ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V )
67 1 stirlinglem2 ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) ∈ ℝ+ )
68 relogcl ⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ ℝ+ → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ )
69 elex ⊢ ( ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V )
70 67 68 69 3syl ⊢ ( 𝑛 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V )
71 66 70 mprgbir ⊢ ℕ = { 𝑛 ∈ ℕ ∣ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V }
72 2 dmmpt ⊢ dom 𝐵 = { 𝑛 ∈ ℕ ∣ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V }
73 71 72 eqtr4i ⊢ ℕ = dom 𝐵
74 65 73 eleqtrdi ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ dom 𝐵 )
75 fvco ⊢ ( ( Fun 𝐵 ∧ 𝑘 ∈ dom 𝐵 ) → ( ( exp ∘ 𝐵 ) ‘ 𝑘 ) = ( exp ‘ ( 𝐵 ‘ 𝑘 ) ) )
76 64 74 75 sylancr ⊢ ( 𝑘 ∈ ℕ → ( ( exp ∘ 𝐵 ) ‘ 𝑘 ) = ( exp ‘ ( 𝐵 ‘ 𝑘 ) ) )
77 1 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) )
78 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → 𝑛 = 𝑘 )
79 78 fveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑘 ) )
80 78 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
81 80 fveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · 𝑘 ) ) )
82 78 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 𝑛 / e ) = ( 𝑘 / e ) )
83 82 78 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( 𝑛 / e ) ↑ 𝑛 ) = ( ( 𝑘 / e ) ↑ 𝑘 ) )
84 81 83 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) )
85 79 84 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
86 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
87 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
88 nncn ⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
89 86 87 88 3syl ⊢ ( 𝑘 ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
90 2cnd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
91 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
92 90 91 mulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℂ )
93 92 sqrtcld ⊢ ( 𝑘 ∈ ℕ → ( √ ‘ ( 2 · 𝑘 ) ) ∈ ℂ )
94 20 a1i ⊢ ( 𝑘 ∈ ℕ → e ∈ ℂ )
95 24 a1i ⊢ ( 𝑘 ∈ ℕ → e ≠ 0 )
96 91 94 95 divcld ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 / e ) ∈ ℂ )
97 96 86 expcld ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / e ) ↑ 𝑘 ) ∈ ℂ )
98 93 97 mulcld ⊢ ( 𝑘 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ∈ ℂ )
99 29 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ+ )
100 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
101 99 100 rpmulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ+ )
102 101 sqrtgt0d ⊢ ( 𝑘 ∈ ℕ → 0 < ( √ ‘ ( 2 · 𝑘 ) ) )
103 102 gt0ne0d ⊢ ( 𝑘 ∈ ℕ → ( √ ‘ ( 2 · 𝑘 ) ) ≠ 0 )
104 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
105 91 94 104 95 divne0d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 / e ) ≠ 0 )
106 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
107 96 105 106 expne0d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / e ) ↑ 𝑘 ) ≠ 0 )
108 93 97 103 107 mulne0d ⊢ ( 𝑘 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ≠ 0 )
109 89 98 108 divcld ⊢ ( 𝑘 ∈ ℕ → ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) ∈ ℂ )
110 77 85 65 109 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
111 110 109 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
112 nnne0 ⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ 𝑘 ) ≠ 0 )
113 86 87 112 3syl ⊢ ( 𝑘 ∈ ℕ → ( ! ‘ 𝑘 ) ≠ 0 )
114 89 98 113 108 divne0d ⊢ ( 𝑘 ∈ ℕ → ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) ≠ 0 )
115 110 114 eqnetrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) ≠ 0 )
116 111 115 logcld ⊢ ( 𝑘 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
117 nfcv ⊢ Ⅎ 𝑛 𝑘
118 nfcv ⊢ Ⅎ 𝑛 log
119 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
120 1 119 nfcxfr ⊢ Ⅎ 𝑛 𝐴
121 120 117 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
122 118 121 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑘 ) )
123 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
124 117 122 123 2 fvmptf ⊢ ( ( 𝑘 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ ) → ( 𝐵 ‘ 𝑘 ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
125 116 124 mpdan ⊢ ( 𝑘 ∈ ℕ → ( 𝐵 ‘ 𝑘 ) = ( log ‘ ( 𝐴 ‘ 𝑘 ) ) )
126 125 fveq2d ⊢ ( 𝑘 ∈ ℕ → ( exp ‘ ( 𝐵 ‘ 𝑘 ) ) = ( exp ‘ ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ) )
127 eflog ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ) = ( 𝐴 ‘ 𝑘 ) )
128 111 115 127 syl2anc ⊢ ( 𝑘 ∈ ℕ → ( exp ‘ ( log ‘ ( 𝐴 ‘ 𝑘 ) ) ) = ( 𝐴 ‘ 𝑘 ) )
129 76 126 128 3eqtrd ⊢ ( 𝑘 ∈ ℕ → ( ( exp ∘ 𝐵 ) ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
130 129 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( exp ∘ 𝐵 ) ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
131 6 59 62 63 130 climeq ⊢ ( ⊤ → ( ( exp ∘ 𝐵 ) ⇝ ( exp ‘ 𝑑 ) ↔ 𝐴 ⇝ ( exp ‘ 𝑑 ) ) )
132 131 mptru ⊢ ( ( exp ∘ 𝐵 ) ⇝ ( exp ‘ 𝑑 ) ↔ 𝐴 ⇝ ( exp ‘ 𝑑 ) )
133 53 132 sylib ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → 𝐴 ⇝ ( exp ‘ 𝑑 ) )
134 breq2 ⊢ ( 𝑐 = ( exp ‘ 𝑑 ) → ( 𝐴 ⇝ 𝑐 ↔ 𝐴 ⇝ ( exp ‘ 𝑑 ) ) )
135 134 rspcev ⊢ ( ( ( exp ‘ 𝑑 ) ∈ ℝ+ ∧ 𝐴 ⇝ ( exp ‘ 𝑑 ) ) → ∃ 𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐 )
136 5 133 135 syl2anc ⊢ ( ( 𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑 ) → ∃ 𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐 )
137 136 rexlimiva ⊢ ( ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑 → ∃ 𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐 )
138 3 137 ax-mp ⊢ ∃ 𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐