Metamath Proof Explorer

Theorem stirlinglem11

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

Ref Expression
Hypotheses stirlinglem11.1 ⊢ A = n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
stirlinglem11.2 ⊢ B = n ∈ ℕ ⟼ log ⁡ A ⁡ n
stirlinglem11.3 ⊢ K = k ∈ ℕ ⟼ 1 2 ⁢ k + 1 ⁢ 1 2 ⋅ N + 1 2 ⁢ k
Assertion stirlinglem11 ⊢ N ∈ ℕ → B ⁡ N + 1 < B ⁡ N

Proof

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