Metamath Proof Explorer

Theorem stirlinglem11

Description: B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem11.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem11.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
stirlinglem11.3 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
Assertion stirlinglem11 ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) < ( 𝐵 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 stirlinglem11.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 stirlinglem11.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3 stirlinglem11.3 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
4 0red ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
5 3 a1i ⊢ ( 𝑁 ∈ ℕ → 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) ) )
6 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → 𝑘 = 1 )
7 6 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( 2 · 𝑘 ) = ( 2 · 1 ) )
8 7 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 1 ) + 1 ) )
9 8 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 1 ) + 1 ) ) )
10 7 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) )
11 9 10 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 1 ) → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) )
12 1nn ⊢ 1 ∈ ℕ
13 12 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ )
14 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
15 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
16 14 15 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℂ )
17 16 15 addcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) + 1 ) ∈ ℂ )
18 2t1e2 ⊢ ( 2 · 1 ) = 2
19 18 oveq1i ⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
20 2p1e3 ⊢ ( 2 + 1 ) = 3
21 19 20 eqtri ⊢ ( ( 2 · 1 ) + 1 ) = 3
22 3ne0 ⊢ 3 ≠ 0
23 21 22 eqnetri ⊢ ( ( 2 · 1 ) + 1 ) ≠ 0
24 23 a1i ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) + 1 ) ≠ 0 )
25 17 24 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℂ )
26 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
27 14 26 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℂ )
28 27 15 addcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
29 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
30 2re ⊢ 2 ∈ ℝ
31 30 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
32 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
33 31 32 remulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
34 33 29 readdcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
35 0lt1 ⊢ 0 < 1
36 35 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
37 2rp ⊢ 2 ∈ ℝ+
38 37 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
39 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
40 38 39 rpmulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ+ )
41 29 40 ltaddrp2d ⊢ ( 𝑁 ∈ ℕ → 1 < ( ( 2 · 𝑁 ) + 1 ) )
42 4 29 34 36 41 lttrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 · 𝑁 ) + 1 ) )
43 42 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
44 28 43 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
45 2nn0 ⊢ 2 ∈ ℕ0
46 45 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ0 )
47 1nn0 ⊢ 1 ∈ ℕ0
48 47 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ0 )
49 46 48 nn0mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℕ0 )
50 44 49 expcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ∈ ℂ )
51 25 50 mulcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) ∈ ℂ )
52 5 11 13 51 fvmptd ⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) = ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) )
53 1re ⊢ 1 ∈ ℝ
54 30 53 remulcli ⊢ ( 2 · 1 ) ∈ ℝ
55 54 53 readdcli ⊢ ( ( 2 · 1 ) + 1 ) ∈ ℝ
56 55 23 rereccli ⊢ ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℝ
57 56 a1i ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℝ )
58 34 43 rereccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
59 58 49 reexpcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ∈ ℝ )
60 57 59 remulcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) ∈ ℝ )
61 52 60 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ∈ ℝ )
62 1 stirlinglem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ‘ 𝑁 ) ∈ ℝ+ )
63 62 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ )
64 nfcv ⊢ Ⅎ 𝑛 𝑁
65 nfcv ⊢ Ⅎ 𝑛 log
66 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
67 1 66 nfcxfr ⊢ Ⅎ 𝑛 𝐴
68 67 64 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑁 )
69 65 68 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ 𝑁 ) )
70 2fveq3 ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
71 64 69 70 2 fvmptf ⊢ ( ( 𝑁 ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ ) → ( 𝐵 ‘ 𝑁 ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
72 63 71 mpdan ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) = ( log ‘ ( 𝐴 ‘ 𝑁 ) ) )
73 72 63 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) ∈ ℝ )
74 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
75 1 stirlinglem2 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( 𝐴 ‘ ( 𝑁 + 1 ) ) ∈ ℝ+ )
76 74 75 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ‘ ( 𝑁 + 1 ) ) ∈ ℝ+ )
77 76 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
78 nfcv ⊢ Ⅎ 𝑛 ( 𝑁 + 1 )
79 67 78 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ ( 𝑁 + 1 ) )
80 65 79 nffv ⊢ Ⅎ 𝑛 ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) )
81 2fveq3 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( log ‘ ( 𝐴 ‘ 𝑛 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) )
82 78 80 81 2 fvmptf ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ ) → ( 𝐵 ‘ ( 𝑁 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) )
83 74 77 82 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) = ( log ‘ ( 𝐴 ‘ ( 𝑁 + 1 ) ) ) )
84 83 77 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
85 73 84 resubcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
86 31 29 remulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℝ )
87 0le2 ⊢ 0 ≤ 2
88 87 a1i ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 2 )
89 0le1 ⊢ 0 ≤ 1
90 89 a1i ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 1 )
91 31 29 88 90 mulge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 2 · 1 ) )
92 86 91 ge0p1rpd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) + 1 ) ∈ ℝ+ )
93 92 rpreccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 1 ) + 1 ) ) ∈ ℝ+ )
94 39 rpge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
95 31 32 88 94 mulge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 2 · 𝑁 ) )
96 33 95 ge0p1rpd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ+ )
97 96 rpreccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ+ )
98 2z ⊢ 2 ∈ ℤ
99 98 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℤ )
100 1z ⊢ 1 ∈ ℤ
101 100 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
102 99 101 zmulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) ∈ ℤ )
103 97 102 rpexpcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ∈ ℝ+ )
104 93 103 rpmulcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 1 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 1 ) ) ) ∈ ℝ+ )
105 52 104 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ∈ ℝ+ )
106 105 rpgt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝐾 ‘ 1 ) )
107 85 61 resubcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) ∈ ℝ )
108 eqid ⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ ( 1 + 1 ) )
109 101 peano2zd ⊢ ( 𝑁 ∈ ℕ → ( 1 + 1 ) ∈ ℤ )
110 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
111 3 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) ) )
112 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 2 · 𝑘 ) = ( 2 · 𝑗 ) )
113 112 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑗 ) + 1 ) )
114 113 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) )
115 112 oveq2d ⊢ ( 𝑘 = 𝑗 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) )
116 114 115 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
117 116 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝑗 ) → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
118 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
119 2cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℂ )
120 nncn ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
121 120 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℂ )
122 119 121 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℂ )
123 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℂ )
124 122 123 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℂ )
125 0red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 0 ∈ ℝ )
126 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℝ )
127 30 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ )
128 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
129 128 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℝ )
130 127 129 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℝ )
131 130 126 readdcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
132 35 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 0 < 1 )
133 37 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ+ )
134 nnrp ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ+ )
135 134 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℝ+ )
136 133 135 rpmulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℝ+ )
137 126 136 ltaddrp2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 1 < ( ( 2 · 𝑗 ) + 1 ) )
138 125 126 131 132 137 lttrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 0 < ( ( 2 · 𝑗 ) + 1 ) )
139 138 gt0ne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
140 124 139 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℂ )
141 26 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑁 ∈ ℂ )
142 119 141 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℂ )
143 142 123 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
144 43 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
145 143 144 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
146 45 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℕ0 )
147 nnnn0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
148 147 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
149 146 148 nn0mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℕ0 )
150 145 149 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ∈ ℂ )
151 140 150 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) ∈ ℂ )
152 111 117 118 151 fvmptd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐾 ‘ 𝑗 ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
153 0red ⊢ ( 𝑗 ∈ ℕ → 0 ∈ ℝ )
154 1red ⊢ ( 𝑗 ∈ ℕ → 1 ∈ ℝ )
155 30 a1i ⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℝ )
156 155 128 remulcld ⊢ ( 𝑗 ∈ ℕ → ( 2 · 𝑗 ) ∈ ℝ )
157 156 154 readdcld ⊢ ( 𝑗 ∈ ℕ → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
158 35 a1i ⊢ ( 𝑗 ∈ ℕ → 0 < 1 )
159 37 a1i ⊢ ( 𝑗 ∈ ℕ → 2 ∈ ℝ+ )
160 159 134 rpmulcld ⊢ ( 𝑗 ∈ ℕ → ( 2 · 𝑗 ) ∈ ℝ+ )
161 154 160 ltaddrp2d ⊢ ( 𝑗 ∈ ℕ → 1 < ( ( 2 · 𝑗 ) + 1 ) )
162 153 154 157 158 161 lttrd ⊢ ( 𝑗 ∈ ℕ → 0 < ( ( 2 · 𝑗 ) + 1 ) )
163 162 gt0ne0d ⊢ ( 𝑗 ∈ ℕ → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
164 163 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
165 124 164 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℂ )
166 165 150 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) ∈ ℂ )
167 152 166 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐾 ‘ 𝑗 ) ∈ ℂ )
168 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
169 1 2 168 3 stirlinglem9 ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
170 110 13 167 169 clim2ser ⊢ ( 𝑁 ∈ ℕ → seq ( 1 + 1 ) ( + , 𝐾 ) ⇝ ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( seq 1 ( + , 𝐾 ) ‘ 1 ) ) )
171 peano2nn ⊢ ( 1 ∈ ℕ → ( 1 + 1 ) ∈ ℕ )
172 uznnssnn ⊢ ( ( 1 + 1 ) ∈ ℕ → ( ℤ≥ ‘ ( 1 + 1 ) ) ⊆ ℕ )
173 12 171 172 mp2b ⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) ⊆ ℕ
174 173 a1i ⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ ( 1 + 1 ) ) ⊆ ℕ )
175 174 sseld ⊢ ( 𝑁 ∈ ℕ → ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 𝑗 ∈ ℕ ) )
176 175 imdistani ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) )
177 176 152 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝐾 ‘ 𝑗 ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
178 30 a1i ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 2 ∈ ℝ )
179 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 𝑗 ∈ ℝ )
180 178 179 remulcld ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( 2 · 𝑗 ) ∈ ℝ )
181 1red ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 1 ∈ ℝ )
182 180 181 readdcld ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
183 173 sseli ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 𝑗 ∈ ℕ )
184 183 163 syl ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
185 182 184 rereccld ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℝ )
186 185 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℝ )
187 34 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
188 43 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
189 187 188 rereccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
190 176 149 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 2 · 𝑗 ) ∈ ℕ0 )
191 189 190 reexpcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ∈ ℝ )
192 186 191 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) ∈ ℝ )
193 177 192 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝐾 ‘ 𝑗 ) ∈ ℝ )
194 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 1 ∈ ℝ )
195 30 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 2 ∈ ℝ )
196 176 129 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 𝑗 ∈ ℝ )
197 195 196 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 2 · 𝑗 ) ∈ ℝ )
198 87 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 2 )
199 0red ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 0 ∈ ℝ )
200 87 a1i ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 0 ≤ 2 )
201 1p1e2 ⊢ ( 1 + 1 ) = 2
202 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → ( 1 + 1 ) ≤ 𝑗 )
203 201 202 eqbrtrrid ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 2 ≤ 𝑗 )
204 199 178 179 200 203 letrd ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) → 0 ≤ 𝑗 )
205 204 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 𝑗 )
206 195 196 198 205 mulge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 2 · 𝑗 ) )
207 197 206 ge0p1rpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ+ )
208 89 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 1 )
209 194 207 208 divge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) )
210 32 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 𝑁 ∈ ℝ )
211 195 210 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
212 94 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ 𝑁 )
213 195 210 198 212 mulge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 2 · 𝑁 ) )
214 211 213 ge0p1rpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ+ )
215 194 214 208 divge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) )
216 189 190 215 expge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) )
217 186 191 209 216 mulge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑗 ) ) ) )
218 217 177 breqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 0 ≤ ( 𝐾 ‘ 𝑗 ) )
219 108 109 170 193 218 iserge0 ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( seq 1 ( + , 𝐾 ) ‘ 1 ) ) )
220 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( + , 𝐾 ) ‘ 1 ) = ( 𝐾 ‘ 1 ) )
221 100 220 mp1i ⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( + , 𝐾 ) ‘ 1 ) = ( 𝐾 ‘ 1 ) )
222 221 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( seq 1 ( + , 𝐾 ) ‘ 1 ) ) = ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) )
223 219 222 breqtrd ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) )
224 4 107 61 223 leadd1dd ⊢ ( 𝑁 ∈ ℕ → ( 0 + ( 𝐾 ‘ 1 ) ) ≤ ( ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) + ( 𝐾 ‘ 1 ) ) )
225 52 51 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ∈ ℂ )
226 225 addid2d ⊢ ( 𝑁 ∈ ℕ → ( 0 + ( 𝐾 ‘ 1 ) ) = ( 𝐾 ‘ 1 ) )
227 73 recnd ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ 𝑁 ) ∈ ℂ )
228 84 recnd ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
229 227 228 subcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ∈ ℂ )
230 229 225 npcand ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) − ( 𝐾 ‘ 1 ) ) + ( 𝐾 ‘ 1 ) ) = ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
231 224 226 230 3brtr3d ⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ‘ 1 ) ≤ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
232 4 61 85 106 231 ltletrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )
233 84 73 posdifd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ ( 𝑁 + 1 ) ) < ( 𝐵 ‘ 𝑁 ) ↔ 0 < ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) ) )
234 232 233 mpbird ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ‘ ( 𝑁 + 1 ) ) < ( 𝐵 ‘ 𝑁 ) )