Metamath Proof Explorer

Theorem 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∈ℕ0⟼2⁢π⁢n⁢nen
stirlingr.2 ⊢R=⇝t⁡topGen⁡ran⁡.
Assertion stirlingr ⊢n∈ℕ⟼n!S⁡nR1

Proof

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