| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq2 5146 | . . 3
⊢ ((𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) → ((abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ↔ (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))) | 
| 2 |  | breq2 5146 | . . 3
⊢ (((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) → ((abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ↔ (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))) | 
| 3 |  | lgamgulm.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 4 | 3 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℕ) | 
| 5 | 4 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑅 ∈ ℕ) | 
| 6 |  | lgamgulm.u | . . . . 5
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} | 
| 7 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑡 → (abs‘𝑥) = (abs‘𝑡)) | 
| 8 | 7 | breq1d 5152 | . . . . . . 7
⊢ (𝑥 = 𝑡 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑡) ≤ 𝑅)) | 
| 9 |  | fvoveq1 7455 | . . . . . . . . 9
⊢ (𝑥 = 𝑡 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑡 + 𝑘))) | 
| 10 | 9 | breq2d 5154 | . . . . . . . 8
⊢ (𝑥 = 𝑡 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))) | 
| 11 | 10 | ralbidv 3177 | . . . . . . 7
⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))) | 
| 12 | 8, 11 | anbi12d 632 | . . . . . 6
⊢ (𝑥 = 𝑡 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘))))) | 
| 13 | 12 | cbvrabv 3446 | . . . . 5
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑅) ≤ (abs‘(𝑥 + 𝑘)))} = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))} | 
| 14 | 6, 13 | eqtri 2764 | . . . 4
⊢ 𝑈 = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))} | 
| 15 |  | simplrl 776 | . . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑛 ∈ ℕ) | 
| 16 |  | simprr 772 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) | 
| 17 | 16 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑦 ∈ 𝑈) | 
| 18 |  | simpr 484 | . . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → (2 · 𝑅) ≤ 𝑛) | 
| 19 | 5, 14, 15, 17, 18 | lgamgulmlem3 27075 | . . 3
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) | 
| 20 | 3, 6 | lgamgulmlem1 27073 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 21 | 20 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 22 | 21, 16 | sseldd 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 23 | 22 | eldifad 3962 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ ℂ) | 
| 24 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℕ) | 
| 25 | 24 | peano2nnd 12284 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈ ℕ) | 
| 26 | 25 | nnrpd 13076 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈
ℝ+) | 
| 27 | 24 | nnrpd 13076 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℝ+) | 
| 28 | 26, 27 | rpdivcld 13095 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) | 
| 29 | 28 | relogcld 26666 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) | 
| 30 | 29 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℂ) | 
| 31 | 23, 30 | mulcld 11282 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ) | 
| 32 | 24 | nncnd 12283 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℂ) | 
| 33 | 24 | nnne0d 12317 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ≠ 0) | 
| 34 | 23, 32, 33 | divcld 12044 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 / 𝑛) ∈ ℂ) | 
| 35 |  | 1cnd 11257 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℂ) | 
| 36 | 34, 35 | addcld 11281 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) ∈ ℂ) | 
| 37 | 22, 24 | dmgmdivn0 27072 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) ≠ 0) | 
| 38 | 36, 37 | logcld 26613 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑦 / 𝑛) + 1)) ∈ ℂ) | 
| 39 | 31, 38 | subcld 11621 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))) ∈ ℂ) | 
| 40 | 39 | abscld 15476 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) | 
| 41 | 31 | abscld 15476 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) ∈ ℝ) | 
| 42 | 38 | abscld 15476 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ∈ ℝ) | 
| 43 | 41, 42 | readdcld 11291 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) | 
| 44 | 4 | nnred 12282 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℝ) | 
| 45 | 44, 29 | remulcld 11292 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℝ) | 
| 46 | 4 | peano2nnd 12284 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℕ) | 
| 47 | 46 | nnrpd 13076 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈
ℝ+) | 
| 48 | 47, 27 | rpmulcld 13094 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 + 1) · 𝑛) ∈
ℝ+) | 
| 49 | 48 | relogcld 26666 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑅 + 1) · 𝑛)) ∈ ℝ) | 
| 50 |  | pire 26501 | . . . . . . . 8
⊢ π
∈ ℝ | 
| 51 | 50 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → π ∈
ℝ) | 
| 52 | 49, 51 | readdcld 11291 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((log‘((𝑅 + 1) · 𝑛)) + π) ∈ ℝ) | 
| 53 | 45, 52 | readdcld 11291 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ ℝ) | 
| 54 | 31, 38 | abs2dif2d 15498 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1))))) | 
| 55 | 23, 30 | absmuld 15494 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (abs‘(log‘((𝑛 + 1) / 𝑛))))) | 
| 56 | 28 | rpred 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑛 + 1) / 𝑛) ∈ ℝ) | 
| 57 | 32 | mullidd 11280 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 · 𝑛) = 𝑛) | 
| 58 | 24 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℝ) | 
| 59 | 58 | lep1d 12200 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ≤ (𝑛 + 1)) | 
| 60 | 57, 59 | eqbrtrd 5164 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 · 𝑛) ≤ (𝑛 + 1)) | 
| 61 |  | 1red 11263 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℝ) | 
| 62 | 58, 61 | readdcld 11291 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈ ℝ) | 
| 63 | 61, 62, 27 | lemuldivd 13127 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 · 𝑛) ≤ (𝑛 + 1) ↔ 1 ≤ ((𝑛 + 1) / 𝑛))) | 
| 64 | 60, 63 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ≤ ((𝑛 + 1) / 𝑛)) | 
| 65 | 56, 64 | logge0d 26673 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (log‘((𝑛 + 1) / 𝑛))) | 
| 66 | 29, 65 | absidd 15462 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑛 + 1) / 𝑛))) = (log‘((𝑛 + 1) / 𝑛))) | 
| 67 | 66 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) · (abs‘(log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛)))) | 
| 68 | 55, 67 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛)))) | 
| 69 | 23 | abscld 15476 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑦) ∈ ℝ) | 
| 70 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (abs‘𝑥) = (abs‘𝑦)) | 
| 71 | 70 | breq1d 5152 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑦) ≤ 𝑅)) | 
| 72 |  | fvoveq1 7455 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑦 + 𝑘))) | 
| 73 | 72 | breq2d 5154 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) | 
| 74 | 73 | ralbidv 3177 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) | 
| 75 | 71, 74 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))))) | 
| 76 | 75, 6 | elrab2 3694 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑈 ↔ (𝑦 ∈ ℂ ∧ ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))))) | 
| 77 | 76 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝑈 → ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) | 
| 78 | 77 | ad2antll 729 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) | 
| 79 | 78 | simpld 494 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑦) ≤ 𝑅) | 
| 80 | 69, 44, 29, 65, 79 | lemul1ad 12208 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛))) ≤ (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) | 
| 81 | 68, 80 | eqbrtrd 5164 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) ≤ (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) | 
| 82 | 36, 37 | absrpcld 15488 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ∈
ℝ+) | 
| 83 | 82 | relogcld 26666 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ∈ ℝ) | 
| 84 | 83 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ∈ ℂ) | 
| 85 | 84 | abscld 15476 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
(abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) | 
| 86 | 85, 51 | readdcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π) ∈
ℝ) | 
| 87 |  | abslogle 26661 | . . . . . . . 8
⊢ ((((𝑦 / 𝑛) + 1) ∈ ℂ ∧ ((𝑦 / 𝑛) + 1) ≠ 0) →
(abs‘(log‘((𝑦 /
𝑛) + 1))) ≤
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π)) | 
| 88 | 36, 37, 87 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ≤
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π)) | 
| 89 |  | 1rp 13039 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ | 
| 90 |  | relogdiv 26636 | . . . . . . . . . . . 12
⊢ ((1
∈ ℝ+ ∧ ((𝑅 + 1) · 𝑛) ∈ ℝ+) →
(log‘(1 / ((𝑅 + 1)
· 𝑛))) =
((log‘1) − (log‘((𝑅 + 1) · 𝑛)))) | 
| 91 | 89, 48, 90 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(1 / ((𝑅 + 1) · 𝑛))) = ((log‘1) −
(log‘((𝑅 + 1)
· 𝑛)))) | 
| 92 |  | log1 26628 | . . . . . . . . . . . . 13
⊢
(log‘1) = 0 | 
| 93 | 92 | oveq1i 7442 | . . . . . . . . . . . 12
⊢
((log‘1) − (log‘((𝑅 + 1) · 𝑛))) = (0 − (log‘((𝑅 + 1) · 𝑛))) | 
| 94 |  | df-neg 11496 | . . . . . . . . . . . 12
⊢
-(log‘((𝑅 + 1)
· 𝑛)) = (0 −
(log‘((𝑅 + 1)
· 𝑛))) | 
| 95 | 93, 94 | eqtr4i 2767 | . . . . . . . . . . 11
⊢
((log‘1) − (log‘((𝑅 + 1) · 𝑛))) = -(log‘((𝑅 + 1) · 𝑛)) | 
| 96 | 91, 95 | eqtr2di 2793 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → -(log‘((𝑅 + 1) · 𝑛)) = (log‘(1 / ((𝑅 + 1) · 𝑛)))) | 
| 97 | 46 | nnrecred 12318 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ∈ ℝ) | 
| 98 | 23, 32 | addcld 11281 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 + 𝑛) ∈ ℂ) | 
| 99 | 98 | abscld 15476 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 + 𝑛)) ∈ ℝ) | 
| 100 | 4 | nnrecred 12318 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / 𝑅) ∈ ℝ) | 
| 101 | 4 | nnrpd 13076 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈
ℝ+) | 
| 102 |  | 0le1 11787 | . . . . . . . . . . . . . . . 16
⊢ 0 ≤
1 | 
| 103 | 102 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ 1) | 
| 104 | 44 | lep1d 12200 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ≤ (𝑅 + 1)) | 
| 105 | 101, 47, 61, 103, 104 | lediv2ad 13100 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ≤ (1 / 𝑅)) | 
| 106 |  | oveq2 7440 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑦 + 𝑘) = (𝑦 + 𝑛)) | 
| 107 | 106 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (abs‘(𝑦 + 𝑘)) = (abs‘(𝑦 + 𝑛))) | 
| 108 | 107 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛)))) | 
| 109 | 78 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))) | 
| 110 | 24 | nnnn0d 12589 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℕ0) | 
| 111 | 108, 109,
110 | rspcdva 3622 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛))) | 
| 112 | 97, 100, 99, 105, 111 | letrd 11419 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ≤ (abs‘(𝑦 + 𝑛))) | 
| 113 | 97, 99, 27, 112 | lediv1dd 13136 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑅 + 1)) / 𝑛) ≤ ((abs‘(𝑦 + 𝑛)) / 𝑛)) | 
| 114 | 46 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℂ) | 
| 115 | 46 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ≠ 0) | 
| 116 | 114, 32, 115, 33 | recdiv2d 12062 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑅 + 1)) / 𝑛) = (1 / ((𝑅 + 1) · 𝑛))) | 
| 117 | 23, 32, 32, 33 | divdird 12082 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 + 𝑛) / 𝑛) = ((𝑦 / 𝑛) + (𝑛 / 𝑛))) | 
| 118 | 32, 33 | dividd 12042 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 / 𝑛) = 1) | 
| 119 | 118 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + (𝑛 / 𝑛)) = ((𝑦 / 𝑛) + 1)) | 
| 120 | 117, 119 | eqtr2d 2777 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) = ((𝑦 + 𝑛) / 𝑛)) | 
| 121 | 120 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) = (abs‘((𝑦 + 𝑛) / 𝑛))) | 
| 122 | 98, 32, 33 | absdivd 15495 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 + 𝑛) / 𝑛)) = ((abs‘(𝑦 + 𝑛)) / (abs‘𝑛))) | 
| 123 | 27 | rpge0d 13082 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ 𝑛) | 
| 124 | 58, 123 | absidd 15462 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑛) = 𝑛) | 
| 125 | 124 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 + 𝑛)) / (abs‘𝑛)) = ((abs‘(𝑦 + 𝑛)) / 𝑛)) | 
| 126 | 121, 122,
125 | 3eqtrrd 2781 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 + 𝑛)) / 𝑛) = (abs‘((𝑦 / 𝑛) + 1))) | 
| 127 | 113, 116,
126 | 3brtr3d 5173 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / ((𝑅 + 1) · 𝑛)) ≤ (abs‘((𝑦 / 𝑛) + 1))) | 
| 128 | 48 | rpreccld 13088 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / ((𝑅 + 1) · 𝑛)) ∈
ℝ+) | 
| 129 | 128, 82 | logled 26670 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / ((𝑅 + 1) · 𝑛)) ≤ (abs‘((𝑦 / 𝑛) + 1)) ↔ (log‘(1 / ((𝑅 + 1) · 𝑛))) ≤
(log‘(abs‘((𝑦 /
𝑛) +
1))))) | 
| 130 | 127, 129 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(1 / ((𝑅 + 1) · 𝑛))) ≤
(log‘(abs‘((𝑦 /
𝑛) + 1)))) | 
| 131 | 96, 130 | eqbrtrd 5164 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → -(log‘((𝑅 + 1) · 𝑛)) ≤ (log‘(abs‘((𝑦 / 𝑛) + 1)))) | 
| 132 | 36 | abscld 15476 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ∈ ℝ) | 
| 133 | 44, 61 | readdcld 11291 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℝ) | 
| 134 | 48 | rpred 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 + 1) · 𝑛) ∈ ℝ) | 
| 135 | 34 | abscld 15476 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) ∈ ℝ) | 
| 136 | 135, 61 | readdcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 / 𝑛)) + 1) ∈ ℝ) | 
| 137 | 34, 35 | abstrid 15496 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((abs‘(𝑦 / 𝑛)) + (abs‘1))) | 
| 138 |  | abs1 15337 | . . . . . . . . . . . . . 14
⊢
(abs‘1) = 1 | 
| 139 | 138 | oveq2i 7443 | . . . . . . . . . . . . 13
⊢
((abs‘(𝑦 /
𝑛)) + (abs‘1)) =
((abs‘(𝑦 / 𝑛)) + 1) | 
| 140 | 137, 139 | breqtrdi 5183 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((abs‘(𝑦 / 𝑛)) + 1)) | 
| 141 | 89 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈
ℝ+) | 
| 142 | 23 | absge0d 15484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (abs‘𝑦)) | 
| 143 | 24 | nnge1d 12315 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ≤ 𝑛) | 
| 144 | 69, 44, 141, 58, 142, 79, 143 | lediv12ad 13137 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / 𝑛) ≤ (𝑅 / 1)) | 
| 145 | 23, 32, 33 | absdivd 15495 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) = ((abs‘𝑦) / (abs‘𝑛))) | 
| 146 | 124 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / (abs‘𝑛)) = ((abs‘𝑦) / 𝑛)) | 
| 147 | 145, 146 | eqtr2d 2777 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / 𝑛) = (abs‘(𝑦 / 𝑛))) | 
| 148 | 4 | nncnd 12283 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℂ) | 
| 149 | 148 | div1d 12036 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 / 1) = 𝑅) | 
| 150 | 144, 147,
149 | 3brtr3d 5173 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) ≤ 𝑅) | 
| 151 | 135, 44, 61, 150 | leadd1dd 11878 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 / 𝑛)) + 1) ≤ (𝑅 + 1)) | 
| 152 | 132, 136,
133, 140, 151 | letrd 11419 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ (𝑅 + 1)) | 
| 153 | 47 | rpge0d 13082 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (𝑅 + 1)) | 
| 154 | 133, 58, 153, 143 | lemulge11d 12206 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ≤ ((𝑅 + 1) · 𝑛)) | 
| 155 | 132, 133,
134, 152, 154 | letrd 11419 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((𝑅 + 1) · 𝑛)) | 
| 156 | 82, 48 | logled 26670 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘((𝑦 / 𝑛) + 1)) ≤ ((𝑅 + 1) · 𝑛) ↔ (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛)))) | 
| 157 | 155, 156 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛))) | 
| 158 | 83, 49 | absled 15470 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ≤ (log‘((𝑅 + 1) · 𝑛)) ↔ (-(log‘((𝑅 + 1) · 𝑛)) ≤ (log‘(abs‘((𝑦 / 𝑛) + 1))) ∧ (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛))))) | 
| 159 | 131, 157,
158 | mpbir2and 713 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
(abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ≤ (log‘((𝑅 + 1) · 𝑛))) | 
| 160 | 85, 49, 51, 159 | leadd1dd 11878 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π) ≤ ((log‘((𝑅 + 1) · 𝑛)) + π)) | 
| 161 | 42, 86, 52, 88, 160 | letrd 11419 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ≤ ((log‘((𝑅 + 1) · 𝑛)) + π)) | 
| 162 | 41, 42, 45, 52, 81, 161 | le2addd 11883 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) | 
| 163 | 40, 43, 53, 54, 162 | letrd 11419 | . . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) | 
| 164 | 163 | adantr 480 | . . 3
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ ¬ (2 · 𝑅) ≤ 𝑛) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) | 
| 165 | 1, 2, 19, 164 | ifbothda 4563 | . 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) | 
| 166 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) | 
| 167 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) | 
| 168 | 166, 167 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) | 
| 169 | 168 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) | 
| 170 | 169 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝑧 · (log‘((𝑛 + 1) / 𝑛)))) | 
| 171 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛)) | 
| 172 | 171 | fvoveq1d 7454 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝑧 / 𝑛) + 1))) | 
| 173 | 170, 172 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) | 
| 174 | 173 | mpteq2dv 5243 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) | 
| 175 |  | lgamgulm.g | . . . . . . 7
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) | 
| 176 |  | cnex 11237 | . . . . . . . . 9
⊢ ℂ
∈ V | 
| 177 | 6, 176 | rabex2 5340 | . . . . . . . 8
⊢ 𝑈 ∈ V | 
| 178 | 177 | mptex 7244 | . . . . . . 7
⊢ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) ∈ V | 
| 179 | 174, 175,
178 | fvmpt 7015 | . . . . . 6
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) | 
| 180 | 179 | ad2antrl 728 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝐺‘𝑛) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) | 
| 181 | 180 | fveq1d 6907 | . . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝐺‘𝑛)‘𝑦) = ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦)) | 
| 182 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑧 · (log‘((𝑛 + 1) / 𝑛))) = (𝑦 · (log‘((𝑛 + 1) / 𝑛)))) | 
| 183 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑧 / 𝑛) = (𝑦 / 𝑛)) | 
| 184 | 183 | fvoveq1d 7454 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (log‘((𝑧 / 𝑛) + 1)) = (log‘((𝑦 / 𝑛) + 1))) | 
| 185 | 182, 184 | oveq12d 7450 | . . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) | 
| 186 |  | eqid 2736 | . . . . . 6
⊢ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) | 
| 187 |  | ovex 7465 | . . . . . 6
⊢ ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))) ∈ V | 
| 188 | 185, 186,
187 | fvmpt 7015 | . . . . 5
⊢ (𝑦 ∈ 𝑈 → ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) | 
| 189 | 188 | ad2antll 729 | . . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) | 
| 190 | 181, 189 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝐺‘𝑛)‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) | 
| 191 | 190 | fveq2d 6909 | . 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) = (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))))) | 
| 192 |  | breq2 5146 | . . . . 5
⊢ (𝑚 = 𝑛 → ((2 · 𝑅) ≤ 𝑚 ↔ (2 · 𝑅) ≤ 𝑛)) | 
| 193 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2)) | 
| 194 | 193 | oveq2d 7448 | . . . . . 6
⊢ (𝑚 = 𝑛 → ((2 · (𝑅 + 1)) / (𝑚↑2)) = ((2 · (𝑅 + 1)) / (𝑛↑2))) | 
| 195 | 194 | oveq2d 7448 | . . . . 5
⊢ (𝑚 = 𝑛 → (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) | 
| 196 | 169 | oveq2d 7448 | . . . . . 6
⊢ (𝑚 = 𝑛 → (𝑅 · (log‘((𝑚 + 1) / 𝑚))) = (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) | 
| 197 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑅 + 1) · 𝑚) = ((𝑅 + 1) · 𝑛)) | 
| 198 | 197 | fveq2d 6909 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (log‘((𝑅 + 1) · 𝑚)) = (log‘((𝑅 + 1) · 𝑛))) | 
| 199 | 198 | oveq1d 7447 | . . . . . 6
⊢ (𝑚 = 𝑛 → ((log‘((𝑅 + 1) · 𝑚)) + π) = ((log‘((𝑅 + 1) · 𝑛)) + π)) | 
| 200 | 196, 199 | oveq12d 7450 | . . . . 5
⊢ (𝑚 = 𝑛 → ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)) = ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) | 
| 201 | 192, 195,
200 | ifbieq12d 4553 | . . . 4
⊢ (𝑚 = 𝑛 → if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) | 
| 202 |  | lgamgulm.t | . . . 4
⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) | 
| 203 |  | ovex 7465 | . . . . 5
⊢ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ V | 
| 204 |  | ovex 7465 | . . . . 5
⊢ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ V | 
| 205 | 203, 204 | ifex 4575 | . . . 4
⊢ if((2
· 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ V | 
| 206 | 201, 202,
205 | fvmpt 7015 | . . 3
⊢ (𝑛 ∈ ℕ → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) | 
| 207 | 206 | ad2antrl 728 | . 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) | 
| 208 | 165, 191,
207 | 3brtr4d 5174 | 1
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) ≤ (𝑇‘𝑛)) |