stirlingr

Description: Stirling's approximation formula for n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling is proven for convergence in the topology of complex numbers. The variable R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlingr.1	$⊢ S = (n \in ℕ_{0} ⟼ \sqrt{2 π n} {(\frac{n}{e})}^{n})$
	stirlingr.2	$⊢ R = \underset{t}{⇝} (topGen (ran (.)))$
Assertion	stirlingr	$⊢ (n \in ℕ ⟼ \frac{n!}{S (n)}) R 1$

Proof

Step	Hyp	Ref	Expression
1		stirlingr.1	$⊢ S = (n \in ℕ_{0} ⟼ \sqrt{2 π n} {(\frac{n}{e})}^{n})$
2		stirlingr.2	$⊢ R = \underset{t}{⇝} (topGen (ran (.)))$
3	1	stirling	$⊢ (n \in ℕ ⟼ \frac{n!}{S (n)}) ⇝ 1$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ ⊤ \to 1 \in ℤ$
6		eqid	$⊢ (n \in ℕ ⟼ \frac{n!}{S (n)}) = (n \in ℕ ⟼ \frac{n!}{S (n)})$
7		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
8		faccl	$⊢ n \in ℕ_{0} \to n! \in ℕ$
9		nnre	$⊢ n! \in ℕ \to n! \in ℝ$
10	7 8 9	3syl	$⊢ n \in ℕ \to n! \in ℝ$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
13		pire	$⊢ π \in ℝ$
14	13	a1i	$⊢ n \in ℕ \to π \in ℝ$
15	12 14	remulcld	$⊢ n \in ℕ \to 2 π \in ℝ$
16		nnre	$⊢ n \in ℕ \to n \in ℝ$
17	15 16	remulcld	$⊢ n \in ℕ \to 2 π n \in ℝ$
18		0re	$⊢ 0 \in ℝ$
19	18	a1i	$⊢ n \in ℕ \to 0 \in ℝ$
20		2pos	$⊢ 0 < 2$
21	20	a1i	$⊢ n \in ℕ \to 0 < 2$
22	19 12 21	ltled	$⊢ n \in ℕ \to 0 \leq 2$
23		pipos	$⊢ 0 < π$
24	18 13 23	ltleii	$⊢ 0 \leq π$
25	24	a1i	$⊢ n \in ℕ \to 0 \leq π$
26	12 14 22 25	mulge0d	$⊢ n \in ℕ \to 0 \leq 2 π$
27	7	nn0ge0d	$⊢ n \in ℕ \to 0 \leq n$
28	15 16 26 27	mulge0d	$⊢ n \in ℕ \to 0 \leq 2 π n$
29	17 28	resqrtcld	$⊢ n \in ℕ \to \sqrt{2 π n} \in ℝ$
30		ere	$⊢ e \in ℝ$
31	30	a1i	$⊢ n \in ℕ \to e \in ℝ$
32		epos	$⊢ 0 < e$
33	18 32	gtneii	$⊢ e \neq 0$
34	33	a1i	$⊢ n \in ℕ \to e \neq 0$
35	16 31 34	redivcld	$⊢ n \in ℕ \to \frac{n}{e} \in ℝ$
36	35 7	reexpcld	$⊢ n \in ℕ \to {(\frac{n}{e})}^{n} \in ℝ$
37	29 36	remulcld	$⊢ n \in ℕ \to \sqrt{2 π n} {(\frac{n}{e})}^{n} \in ℝ$
38	1	fvmpt2	$⊢ (n \in ℕ_{0} \land \sqrt{2 π n} {(\frac{n}{e})}^{n} \in ℝ) \to S (n) = \sqrt{2 π n} {(\frac{n}{e})}^{n}$
39	7 37 38	syl2anc	$⊢ n \in ℕ \to S (n) = \sqrt{2 π n} {(\frac{n}{e})}^{n}$
40		2rp	$⊢ 2 \in ℝ^{+}$
41	40	a1i	$⊢ n \in ℕ \to 2 \in ℝ^{+}$
42		pirp	$⊢ π \in ℝ^{+}$
43	42	a1i	$⊢ n \in ℕ \to π \in ℝ^{+}$
44	41 43	rpmulcld	$⊢ n \in ℕ \to 2 π \in ℝ^{+}$
45		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
46	44 45	rpmulcld	$⊢ n \in ℕ \to 2 π n \in ℝ^{+}$
47	46	rpsqrtcld	$⊢ n \in ℕ \to \sqrt{2 π n} \in ℝ^{+}$
48		epr	$⊢ e \in ℝ^{+}$
49	48	a1i	$⊢ n \in ℕ \to e \in ℝ^{+}$
50	45 49	rpdivcld	$⊢ n \in ℕ \to \frac{n}{e} \in ℝ^{+}$
51		nnz	$⊢ n \in ℕ \to n \in ℤ$
52	50 51	rpexpcld	$⊢ n \in ℕ \to {(\frac{n}{e})}^{n} \in ℝ^{+}$
53	47 52	rpmulcld	$⊢ n \in ℕ \to \sqrt{2 π n} {(\frac{n}{e})}^{n} \in ℝ^{+}$
54	39 53	eqeltrd	$⊢ n \in ℕ \to S (n) \in ℝ^{+}$
55	10 54	rerpdivcld	$⊢ n \in ℕ \to \frac{n!}{S (n)} \in ℝ$
56	6 55	fmpti	$⊢ (n \in ℕ ⟼ \frac{n!}{S (n)}) : ℕ ⟶ ℝ$
57	56	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{n!}{S (n)}) : ℕ ⟶ ℝ$
58	2 4 5 57	climreeq	$⊢ ⊤ \to ((n \in ℕ ⟼ \frac{n!}{S (n)}) R 1 \leftrightarrow (n \in ℕ ⟼ \frac{n!}{S (n)}) ⇝ 1)$
59	58	mptru	$⊢ (n \in ℕ ⟼ \frac{n!}{S (n)}) R 1 \leftrightarrow (n \in ℕ ⟼ \frac{n!}{S (n)}) ⇝ 1$
60	3 59	mpbir	$⊢ (n \in ℕ ⟼ \frac{n!}{S (n)}) R 1$

Metamath Proof Explorer

Theorem stirlingr

Proof