Step |
Hyp |
Ref |
Expression |
1 |
|
stirling.1 |
⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) |
2 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) |
3 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ) ) |
4 |
2 3
|
stirlinglem14 |
⊢ ∃ 𝑐 ∈ ℝ+ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 |
5 |
|
nfv |
⊢ Ⅎ 𝑛 𝑐 ∈ ℝ+ |
6 |
|
nfmpt1 |
⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑛 ⇝ |
8 |
|
nfcv |
⊢ Ⅎ 𝑛 𝑐 |
9 |
6 7 8
|
nfbr |
⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 |
10 |
5 9
|
nfan |
⊢ Ⅎ 𝑛 ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) |
11 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) |
12 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) |
13 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) |
14 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ↑ 4 ) / ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) ‘ 𝑛 ) ↑ 2 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ↑ 4 ) / ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) ‘ 𝑛 ) ↑ 2 ) ) ) |
15 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) |
16 |
|
simpl |
⊢ ( ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) → 𝑐 ∈ ℝ+ ) |
17 |
|
simpr |
⊢ ( ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) |
18 |
10 1 2 11 12 13 14 15 16 17
|
stirlinglem15 |
⊢ ( ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 ) |
19 |
18
|
rexlimiva |
⊢ ( ∃ 𝑐 ∈ ℝ+ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 ) |
20 |
4 19
|
ax-mp |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 |