Metamath Proof Explorer

Theorem stirlinglem12

Description: The sequence B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem12.1 ⊢ A = n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
stirlinglem12.2 ⊢ B = n ∈ ℕ ⟼ log ⁡ A ⁡ n
stirlinglem12.3 ⊢ F = n ∈ ℕ ⟼ 1 n ⁢ n + 1
Assertion stirlinglem12 ⊢ N ∈ ℕ → B ⁡ 1 − 1 4 ≤ B ⁡ N

Proof

Step Hyp Ref Expression
1 stirlinglem12.1 ⊢ A = n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
2 stirlinglem12.2 ⊢ B = n ∈ ℕ ⟼ log ⁡ A ⁡ n
3 stirlinglem12.3 ⊢ F = n ∈ ℕ ⟼ 1 n ⁢ n + 1
4 1nn ⊢ 1 ∈ ℕ
5 1 stirlinglem2 ⊢ 1 ∈ ℕ → A ⁡ 1 ∈ ℝ +
6 relogcl ⊢ A ⁡ 1 ∈ ℝ + → log ⁡ A ⁡ 1 ∈ ℝ
7 4 5 6 mp2b ⊢ log ⁡ A ⁡ 1 ∈ ℝ
8 nfcv ⊢ Ⅎ _ n 1
9 nfcv ⊢ Ⅎ _ n log
10 nfmpt1 ⊢ Ⅎ _ n n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
11 1 10 nfcxfr ⊢ Ⅎ _ n A
12 11 8 nffv ⊢ Ⅎ _ n A ⁡ 1
13 9 12 nffv ⊢ Ⅎ _ n log ⁡ A ⁡ 1
14 2fveq3 ⊢ n = 1 → log ⁡ A ⁡ n = log ⁡ A ⁡ 1
15 8 13 14 2 fvmptf ⊢ 1 ∈ ℕ ∧ log ⁡ A ⁡ 1 ∈ ℝ → B ⁡ 1 = log ⁡ A ⁡ 1
16 4 7 15 mp2an ⊢ B ⁡ 1 = log ⁡ A ⁡ 1
17 16 7 eqeltri ⊢ B ⁡ 1 ∈ ℝ
18 17 a1i ⊢ N ∈ ℕ → B ⁡ 1 ∈ ℝ
19 1 stirlinglem2 ⊢ N ∈ ℕ → A ⁡ N ∈ ℝ +
20 19 relogcld ⊢ N ∈ ℕ → log ⁡ A ⁡ N ∈ ℝ
21 nfcv ⊢ Ⅎ _ n N
22 11 21 nffv ⊢ Ⅎ _ n A ⁡ N
23 9 22 nffv ⊢ Ⅎ _ n log ⁡ A ⁡ N
24 2fveq3 ⊢ n = N → log ⁡ A ⁡ n = log ⁡ A ⁡ N
25 21 23 24 2 fvmptf ⊢ N ∈ ℕ ∧ log ⁡ A ⁡ N ∈ ℝ → B ⁡ N = log ⁡ A ⁡ N
26 20 25 mpdan ⊢ N ∈ ℕ → B ⁡ N = log ⁡ A ⁡ N
27 26 20 eqeltrd ⊢ N ∈ ℕ → B ⁡ N ∈ ℝ
28 4re ⊢ 4 ∈ ℝ
29 4ne0 ⊢ 4 ≠ 0
30 28 29 rereccli ⊢ 1 4 ∈ ℝ
31 30 a1i ⊢ N ∈ ℕ → 1 4 ∈ ℝ
32 fveq2 ⊢ k = j → B ⁡ k = B ⁡ j
33 fveq2 ⊢ k = j + 1 → B ⁡ k = B ⁡ j + 1
34 fveq2 ⊢ k = 1 → B ⁡ k = B ⁡ 1
35 fveq2 ⊢ k = N → B ⁡ k = B ⁡ N
36 elnnuz ⊢ N ∈ ℕ ↔ N ∈ ℤ ≥ 1
37 36 biimpi ⊢ N ∈ ℕ → N ∈ ℤ ≥ 1
38 elfznn ⊢ k ∈ 1 … N → k ∈ ℕ
39 1 stirlinglem2 ⊢ k ∈ ℕ → A ⁡ k ∈ ℝ +
40 38 39 syl ⊢ k ∈ 1 … N → A ⁡ k ∈ ℝ +
41 40 relogcld ⊢ k ∈ 1 … N → log ⁡ A ⁡ k ∈ ℝ
42 nfcv ⊢ Ⅎ _ n k
43 11 42 nffv ⊢ Ⅎ _ n A ⁡ k
44 9 43 nffv ⊢ Ⅎ _ n log ⁡ A ⁡ k
45 2fveq3 ⊢ n = k → log ⁡ A ⁡ n = log ⁡ A ⁡ k
46 42 44 45 2 fvmptf ⊢ k ∈ ℕ ∧ log ⁡ A ⁡ k ∈ ℝ → B ⁡ k = log ⁡ A ⁡ k
47 38 41 46 syl2anc ⊢ k ∈ 1 … N → B ⁡ k = log ⁡ A ⁡ k
48 47 adantl ⊢ N ∈ ℕ ∧ k ∈ 1 … N → B ⁡ k = log ⁡ A ⁡ k
49 40 rpcnd ⊢ k ∈ 1 … N → A ⁡ k ∈ ℂ
50 49 adantl ⊢ N ∈ ℕ ∧ k ∈ 1 … N → A ⁡ k ∈ ℂ
51 39 rpne0d ⊢ k ∈ ℕ → A ⁡ k ≠ 0
52 38 51 syl ⊢ k ∈ 1 … N → A ⁡ k ≠ 0
53 52 adantl ⊢ N ∈ ℕ ∧ k ∈ 1 … N → A ⁡ k ≠ 0
54 50 53 logcld ⊢ N ∈ ℕ ∧ k ∈ 1 … N → log ⁡ A ⁡ k ∈ ℂ
55 48 54 eqeltrd ⊢ N ∈ ℕ ∧ k ∈ 1 … N → B ⁡ k ∈ ℂ
56 32 33 34 35 37 55 telfsumo ⊢ N ∈ ℕ → ∑ j ∈ 1 ..^ N B ⁡ j − B ⁡ j + 1 = B ⁡ 1 − B ⁡ N
57 nnz ⊢ N ∈ ℕ → N ∈ ℤ
58 fzoval ⊢ N ∈ ℤ → 1 ..^ N = 1 … N − 1
59 57 58 syl ⊢ N ∈ ℕ → 1 ..^ N = 1 … N − 1
60 59 sumeq1d ⊢ N ∈ ℕ → ∑ j ∈ 1 ..^ N B ⁡ j − B ⁡ j + 1 = ∑ j = 1 N − 1 B ⁡ j − B ⁡ j + 1
61 56 60 eqtr3d ⊢ N ∈ ℕ → B ⁡ 1 − B ⁡ N = ∑ j = 1 N − 1 B ⁡ j − B ⁡ j + 1
62 fzfid ⊢ N ∈ ℕ → 1 … N − 1 ∈ Fin
63 elfznn ⊢ j ∈ 1 … N − 1 → j ∈ ℕ
64 63 adantl ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → j ∈ ℕ
65 1 stirlinglem2 ⊢ j ∈ ℕ → A ⁡ j ∈ ℝ +
66 65 relogcld ⊢ j ∈ ℕ → log ⁡ A ⁡ j ∈ ℝ
67 nfcv ⊢ Ⅎ _ n j
68 11 67 nffv ⊢ Ⅎ _ n A ⁡ j
69 9 68 nffv ⊢ Ⅎ _ n log ⁡ A ⁡ j
70 2fveq3 ⊢ n = j → log ⁡ A ⁡ n = log ⁡ A ⁡ j
71 67 69 70 2 fvmptf ⊢ j ∈ ℕ ∧ log ⁡ A ⁡ j ∈ ℝ → B ⁡ j = log ⁡ A ⁡ j
72 66 71 mpdan ⊢ j ∈ ℕ → B ⁡ j = log ⁡ A ⁡ j
73 72 66 eqeltrd ⊢ j ∈ ℕ → B ⁡ j ∈ ℝ
74 64 73 syl ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → B ⁡ j ∈ ℝ
75 peano2nn ⊢ j ∈ ℕ → j + 1 ∈ ℕ
76 1 stirlinglem2 ⊢ j + 1 ∈ ℕ → A ⁡ j + 1 ∈ ℝ +
77 75 76 syl ⊢ j ∈ ℕ → A ⁡ j + 1 ∈ ℝ +
78 77 relogcld ⊢ j ∈ ℕ → log ⁡ A ⁡ j + 1 ∈ ℝ
79 nfcv ⊢ Ⅎ _ n j + 1
80 11 79 nffv ⊢ Ⅎ _ n A ⁡ j + 1
81 9 80 nffv ⊢ Ⅎ _ n log ⁡ A ⁡ j + 1
82 2fveq3 ⊢ n = j + 1 → log ⁡ A ⁡ n = log ⁡ A ⁡ j + 1
83 79 81 82 2 fvmptf ⊢ j + 1 ∈ ℕ ∧ log ⁡ A ⁡ j + 1 ∈ ℝ → B ⁡ j + 1 = log ⁡ A ⁡ j + 1
84 75 78 83 syl2anc ⊢ j ∈ ℕ → B ⁡ j + 1 = log ⁡ A ⁡ j + 1
85 84 78 eqeltrd ⊢ j ∈ ℕ → B ⁡ j + 1 ∈ ℝ
86 63 85 syl ⊢ j ∈ 1 … N − 1 → B ⁡ j + 1 ∈ ℝ
87 86 adantl ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → B ⁡ j + 1 ∈ ℝ
88 74 87 resubcld ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → B ⁡ j − B ⁡ j + 1 ∈ ℝ
89 62 88 fsumrecl ⊢ N ∈ ℕ → ∑ j = 1 N − 1 B ⁡ j − B ⁡ j + 1 ∈ ℝ
90 30 a1i ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → 1 4 ∈ ℝ
91 63 nnred ⊢ j ∈ 1 … N − 1 → j ∈ ℝ
92 1red ⊢ j ∈ 1 … N − 1 → 1 ∈ ℝ
93 91 92 readdcld ⊢ j ∈ 1 … N − 1 → j + 1 ∈ ℝ
94 91 93 remulcld ⊢ j ∈ 1 … N − 1 → j ⁢ j + 1 ∈ ℝ
95 91 recnd ⊢ j ∈ 1 … N − 1 → j ∈ ℂ
96 1cnd ⊢ j ∈ 1 … N − 1 → 1 ∈ ℂ
97 95 96 addcld ⊢ j ∈ 1 … N − 1 → j + 1 ∈ ℂ
98 63 nnne0d ⊢ j ∈ 1 … N − 1 → j ≠ 0
99 75 nnne0d ⊢ j ∈ ℕ → j + 1 ≠ 0
100 63 99 syl ⊢ j ∈ 1 … N − 1 → j + 1 ≠ 0
101 95 97 98 100 mulne0d ⊢ j ∈ 1 … N − 1 → j ⁢ j + 1 ≠ 0
102 94 101 rereccld ⊢ j ∈ 1 … N − 1 → 1 j ⁢ j + 1 ∈ ℝ
103 102 adantl ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → 1 j ⁢ j + 1 ∈ ℝ
104 90 103 remulcld ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → 1 4 ⁢ 1 j ⁢ j + 1 ∈ ℝ
105 62 104 fsumrecl ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 4 ⁢ 1 j ⁢ j + 1 ∈ ℝ
106 eqid ⊢ i ∈ ℕ ⟼ 1 2 ⁢ i + 1 ⁢ 1 2 ⁢ j + 1 2 ⁢ i = i ∈ ℕ ⟼ 1 2 ⁢ i + 1 ⁢ 1 2 ⁢ j + 1 2 ⁢ i
107 eqid ⊢ i ∈ ℕ ⟼ 1 2 ⁢ j + 1 2 i = i ∈ ℕ ⟼ 1 2 ⁢ j + 1 2 i
108 1 2 106 107 stirlinglem10 ⊢ j ∈ ℕ → B ⁡ j − B ⁡ j + 1 ≤ 1 4 ⁢ 1 j ⁢ j + 1
109 64 108 syl ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → B ⁡ j − B ⁡ j + 1 ≤ 1 4 ⁢ 1 j ⁢ j + 1
110 62 88 104 109 fsumle ⊢ N ∈ ℕ → ∑ j = 1 N − 1 B ⁡ j − B ⁡ j + 1 ≤ ∑ j = 1 N − 1 1 4 ⁢ 1 j ⁢ j + 1
111 62 103 fsumrecl ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 ∈ ℝ
112 1red ⊢ N ∈ ℕ → 1 ∈ ℝ
113 4pos ⊢ 0 < 4
114 28 113 elrpii ⊢ 4 ∈ ℝ +
115 114 a1i ⊢ N ∈ ℕ → 4 ∈ ℝ +
116 0red ⊢ N ∈ ℕ → 0 ∈ ℝ
117 0lt1 ⊢ 0 < 1
118 117 a1i ⊢ N ∈ ℕ → 0 < 1
119 116 112 118 ltled ⊢ N ∈ ℕ → 0 ≤ 1
120 112 115 119 divge0d ⊢ N ∈ ℕ → 0 ≤ 1 4
121 eqid ⊢ ℤ ≥ N = ℤ ≥ N
122 eluznn ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ∈ ℕ
123 3 a1i ⊢ j ∈ ℕ → F = n ∈ ℕ ⟼ 1 n ⁢ n + 1
124 simpr ⊢ j ∈ ℕ ∧ n = j → n = j
125 124 oveq1d ⊢ j ∈ ℕ ∧ n = j → n + 1 = j + 1
126 124 125 oveq12d ⊢ j ∈ ℕ ∧ n = j → n ⁢ n + 1 = j ⁢ j + 1
127 126 oveq2d ⊢ j ∈ ℕ ∧ n = j → 1 n ⁢ n + 1 = 1 j ⁢ j + 1
128 id ⊢ j ∈ ℕ → j ∈ ℕ
129 nnre ⊢ j ∈ ℕ → j ∈ ℝ
130 1red ⊢ j ∈ ℕ → 1 ∈ ℝ
131 129 130 readdcld ⊢ j ∈ ℕ → j + 1 ∈ ℝ
132 129 131 remulcld ⊢ j ∈ ℕ → j ⁢ j + 1 ∈ ℝ
133 nncn ⊢ j ∈ ℕ → j ∈ ℂ
134 1cnd ⊢ j ∈ ℕ → 1 ∈ ℂ
135 133 134 addcld ⊢ j ∈ ℕ → j + 1 ∈ ℂ
136 nnne0 ⊢ j ∈ ℕ → j ≠ 0
137 133 135 136 99 mulne0d ⊢ j ∈ ℕ → j ⁢ j + 1 ≠ 0
138 132 137 rereccld ⊢ j ∈ ℕ → 1 j ⁢ j + 1 ∈ ℝ
139 123 127 128 138 fvmptd ⊢ j ∈ ℕ → F ⁡ j = 1 j ⁢ j + 1
140 122 139 syl ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → F ⁡ j = 1 j ⁢ j + 1
141 122 nnred ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ∈ ℝ
142 1red ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → 1 ∈ ℝ
143 141 142 readdcld ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j + 1 ∈ ℝ
144 141 143 remulcld ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ⁢ j + 1 ∈ ℝ
145 141 recnd ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ∈ ℂ
146 1cnd ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → 1 ∈ ℂ
147 145 146 addcld ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j + 1 ∈ ℂ
148 122 nnne0d ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ≠ 0
149 122 99 syl ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j + 1 ≠ 0
150 145 147 148 149 mulne0d ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ⁢ j + 1 ≠ 0
151 144 150 rereccld ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → 1 j ⁢ j + 1 ∈ ℝ
152 seqeq1 ⊢ N = 1 → seq N + F = seq 1 + F
153 3 trireciplem ⊢ seq 1 + F ⇝ 1
154 climrel ⊢ Rel ⁡ ⇝
155 154 releldmi ⊢ seq 1 + F ⇝ 1 → seq 1 + F ∈ dom ⁡ ⇝
156 153 155 mp1i ⊢ N = 1 → seq 1 + F ∈ dom ⁡ ⇝
157 152 156 eqeltrd ⊢ N = 1 → seq N + F ∈ dom ⁡ ⇝
158 157 adantl ⊢ N ∈ ℕ ∧ N = 1 → seq N + F ∈ dom ⁡ ⇝
159 simpl ⊢ N ∈ ℕ ∧ ¬ N = 1 → N ∈ ℕ
160 simpr ⊢ N ∈ ℕ ∧ ¬ N = 1 → ¬ N = 1
161 elnn1uz2 ⊢ N ∈ ℕ ↔ N = 1 ∨ N ∈ ℤ ≥ 2
162 161 birani ⊢ N ∈ ℕ ∧ ¬ N = 1 → N = 1 ∨ N ∈ ℤ ≥ 2
163 162 ord ⊢ N ∈ ℕ ∧ ¬ N = 1 → ¬ N = 1 → N ∈ ℤ ≥ 2
164 160 163 mpd ⊢ N ∈ ℕ ∧ ¬ N = 1 → N ∈ ℤ ≥ 2
165 uz2m1nn ⊢ N ∈ ℤ ≥ 2 → N − 1 ∈ ℕ
166 164 165 syl ⊢ N ∈ ℕ ∧ ¬ N = 1 → N − 1 ∈ ℕ
167 nncn ⊢ N ∈ ℕ → N ∈ ℂ
168 167 adantr ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → N ∈ ℂ
169 1cnd ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → 1 ∈ ℂ
170 168 169 npcand ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → N - 1 + 1 = N
171 170 eqcomd ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → N = N - 1 + 1
172 171 seqeq1d ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → seq N + F = seq N - 1 + 1 + F
173 nnuz ⊢ ℕ = ℤ ≥ 1
174 id ⊢ N − 1 ∈ ℕ → N − 1 ∈ ℕ
175 138 recnd ⊢ j ∈ ℕ → 1 j ⁢ j + 1 ∈ ℂ
176 139 175 eqeltrd ⊢ j ∈ ℕ → F ⁡ j ∈ ℂ
177 176 adantl ⊢ N − 1 ∈ ℕ ∧ j ∈ ℕ → F ⁡ j ∈ ℂ
178 153 a1i ⊢ N − 1 ∈ ℕ → seq 1 + F ⇝ 1
179 173 174 177 178 clim2ser ⊢ N − 1 ∈ ℕ → seq N - 1 + 1 + F ⇝ 1 − seq 1 + F ⁡ N − 1
180 179 adantl ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → seq N - 1 + 1 + F ⇝ 1 − seq 1 + F ⁡ N − 1
181 172 180 eqbrtrd ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → seq N + F ⇝ 1 − seq 1 + F ⁡ N − 1
182 154 releldmi ⊢ seq N + F ⇝ 1 − seq 1 + F ⁡ N − 1 → seq N + F ∈ dom ⁡ ⇝
183 181 182 syl ⊢ N ∈ ℕ ∧ N − 1 ∈ ℕ → seq N + F ∈ dom ⁡ ⇝
184 159 166 183 syl2anc ⊢ N ∈ ℕ ∧ ¬ N = 1 → seq N + F ∈ dom ⁡ ⇝
185 158 184 pm2.61dan ⊢ N ∈ ℕ → seq N + F ∈ dom ⁡ ⇝
186 121 57 140 151 185 isumrecl ⊢ N ∈ ℕ → ∑ j ∈ ℤ ≥ N 1 j ⁢ j + 1 ∈ ℝ
187 122 nnrpd ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ∈ ℝ +
188 187 rpge0d ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → 0 ≤ j
189 141 188 ge0p1rpd ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j + 1 ∈ ℝ +
190 187 189 rpmulcld ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → j ⁢ j + 1 ∈ ℝ +
191 119 adantr ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → 0 ≤ 1
192 142 190 191 divge0d ⊢ N ∈ ℕ ∧ j ∈ ℤ ≥ N → 0 ≤ 1 j ⁢ j + 1
193 121 57 140 151 185 192 isumge0 ⊢ N ∈ ℕ → 0 ≤ ∑ j ∈ ℤ ≥ N 1 j ⁢ j + 1
194 116 186 111 193 leadd2dd ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 + 0 ≤ ∑ j = 1 N − 1 1 j ⁢ j + 1 + ∑ j ∈ ℤ ≥ N 1 j ⁢ j + 1
195 111 recnd ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 ∈ ℂ
196 195 addridd ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 + 0 = ∑ j = 1 N − 1 1 j ⁢ j + 1
197 196 eqcomd ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 = ∑ j = 1 N − 1 1 j ⁢ j + 1 + 0
198 id ⊢ N ∈ ℕ → N ∈ ℕ
199 139 adantl ⊢ N ∈ ℕ ∧ j ∈ ℕ → F ⁡ j = 1 j ⁢ j + 1
200 133 adantl ⊢ N ∈ ℕ ∧ j ∈ ℕ → j ∈ ℂ
201 1cnd ⊢ N ∈ ℕ ∧ j ∈ ℕ → 1 ∈ ℂ
202 200 201 addcld ⊢ N ∈ ℕ ∧ j ∈ ℕ → j + 1 ∈ ℂ
203 200 202 mulcld ⊢ N ∈ ℕ ∧ j ∈ ℕ → j ⁢ j + 1 ∈ ℂ
204 136 adantl ⊢ N ∈ ℕ ∧ j ∈ ℕ → j ≠ 0
205 99 adantl ⊢ N ∈ ℕ ∧ j ∈ ℕ → j + 1 ≠ 0
206 200 202 204 205 mulne0d ⊢ N ∈ ℕ ∧ j ∈ ℕ → j ⁢ j + 1 ≠ 0
207 203 206 reccld ⊢ N ∈ ℕ ∧ j ∈ ℕ → 1 j ⁢ j + 1 ∈ ℂ
208 153 155 mp1i ⊢ N ∈ ℕ → seq 1 + F ∈ dom ⁡ ⇝
209 173 121 198 199 207 208 isumsplit ⊢ N ∈ ℕ → ∑ j ∈ ℕ 1 j ⁢ j + 1 = ∑ j = 1 N − 1 1 j ⁢ j + 1 + ∑ j ∈ ℤ ≥ N 1 j ⁢ j + 1
210 194 197 209 3brtr4d ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 ≤ ∑ j ∈ ℕ 1 j ⁢ j + 1
211 1zzd ⊢ ⊤ → 1 ∈ ℤ
212 139 adantl ⊢ ⊤ ∧ j ∈ ℕ → F ⁡ j = 1 j ⁢ j + 1
213 175 adantl ⊢ ⊤ ∧ j ∈ ℕ → 1 j ⁢ j + 1 ∈ ℂ
214 153 a1i ⊢ ⊤ → seq 1 + F ⇝ 1
215 173 211 212 213 214 isumclim ⊢ ⊤ → ∑ j ∈ ℕ 1 j ⁢ j + 1 = 1
216 215 mptru ⊢ ∑ j ∈ ℕ 1 j ⁢ j + 1 = 1
217 210 216 breqtrdi ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 j ⁢ j + 1 ≤ 1
218 111 112 31 120 217 lemul2ad ⊢ N ∈ ℕ → 1 4 ⁢ ∑ j = 1 N − 1 1 j ⁢ j + 1 ≤ 1 4 ⋅ 1
219 4cn ⊢ 4 ∈ ℂ
220 219 a1i ⊢ N ∈ ℕ → 4 ∈ ℂ
221 113 a1i ⊢ N ∈ ℕ → 0 < 4
222 221 gt0ne0d ⊢ N ∈ ℕ → 4 ≠ 0
223 220 222 reccld ⊢ N ∈ ℕ → 1 4 ∈ ℂ
224 103 recnd ⊢ N ∈ ℕ ∧ j ∈ 1 … N − 1 → 1 j ⁢ j + 1 ∈ ℂ
225 62 223 224 fsummulc2 ⊢ N ∈ ℕ → 1 4 ⁢ ∑ j = 1 N − 1 1 j ⁢ j + 1 = ∑ j = 1 N − 1 1 4 ⁢ 1 j ⁢ j + 1
226 223 mulridd ⊢ N ∈ ℕ → 1 4 ⋅ 1 = 1 4
227 218 225 226 3brtr3d ⊢ N ∈ ℕ → ∑ j = 1 N − 1 1 4 ⁢ 1 j ⁢ j + 1 ≤ 1 4
228 89 105 31 110 227 letrd ⊢ N ∈ ℕ → ∑ j = 1 N − 1 B ⁡ j − B ⁡ j + 1 ≤ 1 4
229 61 228 eqbrtrd ⊢ N ∈ ℕ → B ⁡ 1 − B ⁡ N ≤ 1 4
230 18 27 31 229 subled ⊢ N ∈ ℕ → B ⁡ 1 − 1 4 ≤ B ⁡ N