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 simpr ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → 𝑦 ∈ ran 𝐵 )
54 8 rgen ⊢ ∀ 𝑛 ∈ ℕ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ
55 2 fnmpt ⊢ ( ∀ 𝑛 ∈ ℕ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ → 𝐵 Fn ℕ )
56 fvelrnb ⊢ ( 𝐵 Fn ℕ → ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) )
57 54 55 56 mp2b ⊢ ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 )
58 53 57 sylib ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 )
59 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 )
60 nfv ⊢ Ⅎ 𝑗 𝑦 ∈ ran 𝐵
61 59 60 nfan ⊢ Ⅎ 𝑗 ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 )
62 nfv ⊢ Ⅎ 𝑗 𝑥 ≤ 𝑦
63 simp1l ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
64 simp2 ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → 𝑗 ∈ ℕ )
65 rsp ⊢ ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) → ( 𝑗 ∈ ℕ → 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ) )
66 63 64 65 sylc ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
67 simp3 ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → ( 𝐵 ‘ 𝑗 ) = 𝑦 )
68 66 67 breqtrd ⊢ ( ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ ( 𝐵 ‘ 𝑗 ) = 𝑦 ) → 𝑥 ≤ 𝑦 )
69 68 3exp ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → ( 𝑗 ∈ ℕ → ( ( 𝐵 ‘ 𝑗 ) = 𝑦 → 𝑥 ≤ 𝑦 ) ) )
70 61 62 69 rexlimd ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → ( ∃ 𝑗 ∈ ℕ ( 𝐵 ‘ 𝑗 ) = 𝑦 → 𝑥 ≤ 𝑦 ) )
71 58 70 mpd ⊢ ( ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) ∧ 𝑦 ∈ ran 𝐵 ) → 𝑥 ≤ 𝑦 )
72 71 ralrimiva ⊢ ( ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) → ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦 )
73 72 reximi ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦 )
74 52 73 ax-mp ⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦
75 infrecl ⊢ ( ( ran 𝐵 ⊆ ℝ ∧ ran 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦 ) → inf ( ran 𝐵 , ℝ , < ) ∈ ℝ )
76 13 41 74 75 mp3an ⊢ inf ( ran 𝐵 , ℝ , < ) ∈ ℝ
77 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
78 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
79 2 8 fmpti ⊢ 𝐵 : ℕ ⟶ ℝ
80 79 a1i ⊢ ( ⊤ → 𝐵 : ℕ ⟶ ℝ )
81 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
82 1 a1i ⊢ ( 𝑗 ∈ ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) )
83 simpr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → 𝑛 = ( 𝑗 + 1 ) )
84 83 fveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ! ‘ 𝑛 ) = ( ! ‘ ( 𝑗 + 1 ) ) )
85 83 oveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( 2 · 𝑛 ) = ( 2 · ( 𝑗 + 1 ) ) )
86 85 fveq2d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) )
87 83 oveq1d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( 𝑛 / e ) = ( ( 𝑗 + 1 ) / e ) )
88 87 83 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ( 𝑛 / e ) ↑ 𝑛 ) = ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) )
89 86 88 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) )
90 84 89 oveq12d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑛 = ( 𝑗 + 1 ) ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) )
91 81 nnnn0d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ0 )
92 faccl ⊢ ( ( 𝑗 + 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ )
93 nncn ⊢ ( ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
94 91 92 93 3syl ⊢ ( 𝑗 ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
95 2cnd ⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℂ )
96 nncn ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
97 1cnd ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℂ )
98 96 97 addcld ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℂ )
99 95 98 mulcld ⊢ ( 𝑗 ∈ ℕ → ( 2 · ( 𝑗 + 1 ) ) ∈ ℂ )
100 99 sqrtcld ⊢ ( 𝑗 ∈ ℕ → ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
101 ere ⊢ e ∈ ℝ
102 101 recni ⊢ e ∈ ℂ
103 102 a1i ⊢ ( 𝑗 ∈ ℕ → e ∈ ℂ )
104 0re ⊢ 0 ∈ ℝ
105 epos ⊢ 0 < e
106 104 105 gtneii ⊢ e ≠ 0
107 106 a1i ⊢ ( 𝑗 ∈ ℕ → e ≠ 0 )
108 98 103 107 divcld ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑗 + 1 ) / e ) ∈ ℂ )
109 108 91 expcld ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
110 100 109 mulcld ⊢ ( 𝑗 ∈ ℕ → ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ∈ ℂ )
111 2rp ⊢ 2 ∈ ℝ+
112 111 a1i ⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℝ+ )
113 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
114 104 a1i ⊢ ( 𝑗 ∈ ℕ → 0 ∈ ℝ )
115 1red ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℝ )
116 0le1 ⊢ 0 ≤ 1
117 116 a1i ⊢ ( 𝑗 ∈ ℕ → 0 ≤ 1 )
118 nnge1 ⊢ ( 𝑗 ∈ ℕ → 1 ≤ 𝑗 )
119 114 115 113 117 118 letrd ⊢ ( 𝑗 ∈ ℕ → 0 ≤ 𝑗 )
120 113 119 ge0p1rpd ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℝ+ )
121 112 120 rpmulcld ⊢ ( 𝑗 ∈ ℕ → ( 2 · ( 𝑗 + 1 ) ) ∈ ℝ+ )
122 121 sqrtgt0d ⊢ ( 𝑗 ∈ ℕ → 0 < ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) )
123 122 gt0ne0d ⊢ ( 𝑗 ∈ ℕ → ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) ≠ 0 )
124 81 nnne0d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ≠ 0 )
125 98 103 124 107 divne0d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑗 + 1 ) / e ) ≠ 0 )
126 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
127 126 peano2zd ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℤ )
128 108 125 127 expne0d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ≠ 0 )
129 100 109 123 128 mulne0d ⊢ ( 𝑗 ∈ ℕ → ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ≠ 0 )
130 94 110 129 divcld ⊢ ( 𝑗 ∈ ℕ → ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
131 82 90 81 130 fvmptd ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) = ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) )
132 nnrp ⊢ ( ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
133 91 92 132 3syl ⊢ ( 𝑗 ∈ ℕ → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
134 121 rpsqrtcld ⊢ ( 𝑗 ∈ ℕ → ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) ∈ ℝ+ )
135 epr ⊢ e ∈ ℝ+
136 135 a1i ⊢ ( 𝑗 ∈ ℕ → e ∈ ℝ+ )
137 120 136 rpdivcld ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑗 + 1 ) / e ) ∈ ℝ+ )
138 137 127 rpexpcld ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ∈ ℝ+ )
139 134 138 rpmulcld ⊢ ( 𝑗 ∈ ℕ → ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ+ )
140 133 139 rpdivcld ⊢ ( 𝑗 ∈ ℕ → ( ( ! ‘ ( 𝑗 + 1 ) ) / ( ( √ ‘ ( 2 · ( 𝑗 + 1 ) ) ) · ( ( ( 𝑗 + 1 ) / e ) ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℝ+ )
141 131 140 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∈ ℝ+ )
142 141 relogcld ⊢ ( 𝑗 ∈ ℕ → ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
143 nfcv ⊢ Ⅎ 𝑛 ( 𝑗 + 1 )
144 21 143 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ ( 𝑗 + 1 ) )
145 19 144 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
146 2fveq3 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
147 143 145 146 2 fvmptf ⊢ ( ( ( 𝑗 + 1 ) ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
148 81 142 147 syl2anc ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
149 148 142 eqeltrd ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
150 79 ffvelcdmi ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
151 eqid ⊢ ( 𝑧 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑧 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ↑ ( 2 · 𝑧 ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑧 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ↑ ( 2 · 𝑧 ) ) ) )
152 1 2 151 stirlinglem11 ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) < ( 𝐵 ‘ 𝑗 ) )
153 149 150 152 ltled ⊢ ( 𝑗 ∈ ℕ → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐵 ‘ 𝑗 ) )
154 153 adantl ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℕ ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐵 ‘ 𝑗 ) )
155 52 a1i ⊢ ( ⊤ → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ 𝑥 ≤ ( 𝐵 ‘ 𝑗 ) )
156 77 78 80 154 155 climinf ⊢ ( ⊤ → 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < ) )
157 156 mptru ⊢ 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < )
158 breq2 ⊢ ( 𝑑 = inf ( ran 𝐵 , ℝ , < ) → ( 𝐵 ⇝ 𝑑 ↔ 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < ) ) )
159 158 rspcev ⊢ ( ( inf ( ran 𝐵 , ℝ , < ) ∈ ℝ ∧ 𝐵 ⇝ inf ( ran 𝐵 , ℝ , < ) ) → ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑 )
160 76 157 159 mp2an ⊢ ∃ 𝑑 ∈ ℝ 𝐵 ⇝ 𝑑