This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
stirlingr.2 ⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
Assertion stirlingr ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) 𝑅 1

Proof

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