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	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
	stirlinglem14.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
Assertion	stirlinglem14	$⊢ \exists c \in ℝ^{+} A ⇝ c$

Proof

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

Metamath Proof Explorer

Theorem stirlinglem14

Proof