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

Metamath Proof Explorer

Theorem stirlinglem13

Description: B is decreasing and has a lower bound, then it converges. Since B is log A , in another theorem it is proven that A converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem13.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem13.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
Assertion stirlinglem13 ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑

Proof

Step Hyp Ref Expression
1 stirlinglem13.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 stirlinglem13.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3 vex ⊢ 𝑦 ∈ V
4 2 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑛 ∈ ℕ 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ) )
5 3 4 ax-mp ⊢ ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑛 ∈ ℕ 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
6 simpr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ) → 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
7 1 stirlinglem2 ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) ∈ ℝ+ )
8 7 relogcld ⊢ ( 𝑛 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ )
9 8 adantr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ )
10 6 9 eqeltrd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ) → 𝑦 ∈ ℝ )
11 10 rexlimiva ⊢ ( ∃ 𝑛 ∈ ℕ 𝑦 = ( log ‘ ( 𝐴 ‘ 𝑛 ) ) → 𝑦 ∈ ℝ )
12 5 11 sylbi ⊢ ( 𝑦 ∈ ran 𝐵 → 𝑦 ∈ ℝ )
13 12 ssriv ⊢ ran 𝐵 ⊆ ℝ
14 1nn ⊢ 1 ∈ ℕ
15 1 stirlinglem2 ⊢ ( 1 ∈ ℕ → ( 𝐴 ‘ 1 ) ∈ ℝ+ )
16 relogcl ⊢ ( ( 𝐴 ‘ 1 ) ∈ ℝ+ → ( log ‘ ( 𝐴 ‘ 1 ) ) ∈ ℝ )
17 14 15 16 mp2b ⊢ ( log ‘ ( 𝐴 ‘ 1 ) ) ∈ ℝ
18 nfcv ⊢ Ⅎ 𝑛 1
19 nfcv ⊢ Ⅎ 𝑛 log
20 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
21 1 20 nfcxfr ⊢ Ⅎ 𝑛 𝐴
22 21 18 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 1 )
23 19 22 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 1 ) )
24 2fveq3 ⊢ ( 𝑛 = 1 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 1 ) ) )
25 18 23 24 2 fvmptf ⊢ ( ( 1 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 1 ) ) ∈ ℝ ) → ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 1 ) ) )
26 14 17 25 mp2an ⊢ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 1 ) )
27 2fveq3 ⊢ ( 𝑗 = 1 → ( log ‘ ( 𝐴 ‘ 𝑗 ) ) = ( log ‘ ( 𝐴 ‘ 1 ) ) )
28 27 rspceeqv ⊢ ( ( 1 ∈ ℕ ∧ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 1 ) ) ) → ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
29 14 26 28 mp2an ⊢ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) )
30 26 17 eqeltri ⊢ ( 𝐵 ‘ 1 ) ∈ ℝ
31 nfcv ⊢ Ⅎ 𝑗 ( log ‘ ( 𝐴 ‘ 𝑛 ) )
32 nfcv ⊢ Ⅎ 𝑛 𝑗
33 21 32 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑗 )
34 19 33 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑗 ) )
35 2fveq3 ⊢ ( 𝑛 = 𝑗 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
36 31 34 35 cbvmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
37 2 36 eqtri ⊢ 𝐵 = ( 𝑗 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
38 37 elrnmpt ⊢ ( ( 𝐵 ‘ 1 ) ∈ ℝ → ( ( 𝐵 ‘ 1 ) ∈ ran 𝐵 ↔ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) ) )
39 30 38 ax-mp ⊢ ( ( 𝐵 ‘ 1 ) ∈ ran 𝐵 ↔ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 1 ) = ( log ‘ ( 𝐴 ‘ 𝑗 ) ) )
40 29 39 mpbir ⊢ ( 𝐵 ‘ 1 ) ∈ ran 𝐵
41 40 ne0ii ⊢ ran 𝐵 ≠ ∅
42 4re ⊢ 4 ∈ ℝ
43 4ne0 ⊢ 4 ≠ 0
44 42 43 rereccli ⊢ ( 1 / 4 ) ∈ ℝ
45 30 44 resubcli ⊢ ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ∈ ℝ
46 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
47 1 2 46 stirlinglem12 ⊢ ( 𝑗 ∈ ℕ → ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑗 ) )
48 47 rgen ⊢ ∀ 𝑗 ∈ ℕ ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑗 )
49 breq1 ⊢ ( 𝑥 = ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) → ( 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ↔ ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑗 ) ) )
50 49 ralbidv ⊢ ( 𝑥 = ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) → ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ ℕ ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑗 ) ) )
51 50 rspcev ⊢ ( ( ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝐵 ‘ 1 ) − ( 1 / 4 ) ) ≤ ( 𝐵 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
52 45 48 51 mp2an ⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 )
53 8 rgen ⊢ ∀ 𝑛 ∈ ℕ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ
54 2 fnmpt ⊢ ( ∀ 𝑛 ∈ ℕ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ → 𝐵 Fn ℕ )
55 fvelrnb ⊢ ( 𝐵 Fn ℕ → ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) )
56 53 54 55 mp2b ⊢ ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 )
57 56 bilani ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 )
58 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 )
59 nfv ⊢ Ⅎ 𝑗 𝑦 ∈ ran 𝐵
60 58 59 nfan ⊢ Ⅎ 𝑗 ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 )
61 nfv ⊢ Ⅎ 𝑗 𝑥 ≤ 𝑦
62 simp1l ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
63 simp2 ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → 𝑗 ∈ ℕ )
64 rsp ⊢ ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) → ( 𝑗 ∈ ℕ → 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ) )
65 62 63 64 sylc ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
66 simp3 ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → ( 𝐵 ‘ 𝑗 ) = 𝑦 )
67 65 66 breqtrd ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → 𝑥 ≤ 𝑦 )
68 67 3exp ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → ( 𝑗 ∈ ℕ → ( ( 𝐵 ‘ 𝑗 ) = 𝑦 → 𝑥 ≤ 𝑦 ) ) )
69 60 61 68 rexlimd ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → ( ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 → 𝑥 ≤ 𝑦 ) )
70 57 69 mpd ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → 𝑥 ≤ 𝑦 )
71 70 ralrimiva ⊢ ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) → ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦 )
72 71 reximi ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦 )
73 52 72 ax-mp ⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦
74 infrecl ⊢ ( ( ran 𝐵 ⊆ ℝ ∧ ran 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦 ) → inf ( ran 𝐵 , ℝ , < ) ∈ ℝ )
75 13 41 73 74 mp3an ⊢ inf ( ran 𝐵 , ℝ , < ) ∈ ℝ
76 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
77 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
78 2 8 fmpti ⊢ 𝐵 : ℕ ⟶ ℝ
79 78 a1i ⊢ ( ⊤ → 𝐵 : ℕ ⟶ ℝ )
80 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
81 1 a1i ⊢ ( 𝑗 ∈ ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) )
82 simpr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → 𝑛 = ( 𝑗 + 1 ) )
83 82 fveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ! ‘ 𝑛 ) = ( ! ‘ ( 𝑗 + 1 ) ) )
84 82 oveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( 2 · 𝑛 ) = ( 2 · ( 𝑗 + 1 ) ) )
85 84 fveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) )
86 82 oveq1d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( 𝑛 / e ) = ( ( 𝑗 + 1 ) / e ) )
87 86 82 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ( 𝑛 / e ) ↑ 𝑛 ) = ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) )
88 85 87 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) )
89 83 88 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) )
90 80 nnnn0d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ0 )
91 faccl ⊢ ( ( 𝑗 + 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ )
92 nncn ⊢ ( ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
93 90 91 92 3syl ⊢ ( 𝑗 ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
94 2cnd ⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℂ )
95 nncn ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
96 1cnd ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℂ )
97 95 96 addcld ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℂ )
98 94 97 mulcld ⊢ ( 𝑗 ∈ ℕ → ( 2 · ( 𝑗 + 1 ) ) ∈ ℂ )
99 98 sqrtcld ⊢ ( 𝑗 ∈ ℕ → ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
100 ere ⊢ e ∈ ℝ
101 100 recni ⊢ e ∈ ℂ
102 101 a1i ⊢ ( 𝑗 ∈ ℕ → e ∈ ℂ )
103 0re ⊢ 0 ∈ ℝ
104 epos ⊢ 0 < e
105 103 104 gtneii ⊢ e ≠ 0
106 105 a1i ⊢ ( 𝑗 ∈ ℕ → e ≠ 0 )
107 97 102 106 divcld ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑗 + 1 ) / e ) ∈ ℂ )
108 107 90 expcld ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
109 99 108 mulcld ⊢ ( 𝑗 ∈ ℕ → ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ∈ ℂ )
110 2rp ⊢ 2 ∈ ℝ+
111 110 a1i ⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℝ+ )
112 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
113 103 a1i ⊢ ( 𝑗 ∈ ℕ → 0 ∈ ℝ )
114 1red ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℝ )
115 0le1 ⊢ 0 ≤ 1
116 115 a1i ⊢ ( 𝑗 ∈ ℕ → 0 ≤ 1 )
117 nnge1 ⊢ ( 𝑗 ∈ ℕ → 1 ≤ 𝑗 )
118 113 114 112 116 117 letrd ⊢ ( 𝑗 ∈ ℕ → 0 ≤ 𝑗 )
119 112 118 ge0p1rpd ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℝ+ )
120 111 119 rpmulcld ⊢ ( 𝑗 ∈ ℕ → ( 2 · ( 𝑗 + 1 ) ) ∈ ℝ+ )
121 120 sqrtgt0d ⊢ ( 𝑗 ∈ ℕ → 0 < ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) )
122 121 gt0ne0d ⊢ ( 𝑗 ∈ ℕ → ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) ≠ 0 )
123 80 nnne0d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ≠ 0 )
124 97 102 123 106 divne0d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑗 + 1 ) / e ) ≠ 0 )
125 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
126 125 peano2zd ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℤ )
127 107 124 126 expne0d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ≠ 0 )
128 99 108 122 127 mulne0d ⊢ ( 𝑗 ∈ ℕ → ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ≠ 0 )
129 93 109 128 divcld ⊢ ( 𝑗 ∈ ℕ → ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
130 81 89 80 129 fvmptd ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) = ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) )
131 nnrp ⊢ ( ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
132 90 91 131 3syl ⊢ ( 𝑗 ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
133 120 rpsqrtcld ⊢ ( 𝑗 ∈ ℕ → ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) ∈ ℝ+ )
134 epr ⊢ e ∈ ℝ+
135 134 a1i ⊢ ( 𝑗 ∈ ℕ → e ∈ ℝ+ )
136 119 135 rpdivcld ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑗 + 1 ) / e ) ∈ ℝ+ )
137 136 126 rpexpcld ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ∈ ℝ+ )
138 133 137 rpmulcld ⊢ ( 𝑗 ∈ ℕ → ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ+ )
139 132 138 rpdivcld ⊢ ( 𝑗 ∈ ℕ → ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℝ+ )
140 130 139 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
141 140 relogcld ⊢ ( 𝑗 ∈ ℕ → ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
142 nfcv ⊢ Ⅎ 𝑛 ( 𝑗 + 1 )
143 21 142 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ ( 𝑗 + 1 ) )
144 19 143 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
145 2fveq3 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
146 142 144 145 2 fvmptf ⊢ ( ( ( 𝑗 + 1 ) ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
147 80 141 146 syl2anc ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
148 147 141 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
149 78 ffvelcdmi ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
150 eqid ⊢ ( 𝑧 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑧 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ↑ ( 2 · 𝑧 ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑧 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ↑ ( 2 · 𝑧 ) ) ) )
151 1 2 150 stirlinglem11 ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) < ( 𝐵 ‘ 𝑗 ) )
152 148 149 151 ltled ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐵 ‘ 𝑗 ) )
153 152 adantl ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℕ ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐵 ‘ 𝑗 ) )
154 52 a1i ⊢ ( ⊤ → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
155 76 77 79 153 154 climinf ⊢ ( ⊤ → 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < ) )
156 155 mptru ⊢ 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < )
157 breq2 ⊢ ( 𝑑 = inf ( ran 𝐵 , ℝ , < ) → ( 𝐵 ⇝ 𝑑 ↔ 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < ) ) )
158 157 rspcev ⊢ ( ( inf ( ran 𝐵 , ℝ , < ) ∈ ℝ ∧ 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < ) ) → ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑 )
159 75 156 158 mp2an ⊢ ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑