Theorem: ZetaSum_aux1_5a (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)
Tactic:
apply div_le_div_of_nonneg_right _ _
State after:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1

a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ 0 ≤ x ^ (s.re + 1)

State before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1
Tactic:
exact le_trans (ZetaSum_aux1_3 x) (by norm_num)
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ 1 / 2 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ 0 ≤ x ^ (s.re + 1)
Tactic:
apply Real.rpow_nonneg <| le_of_lt (ZetaSum_aux1_1' apos h)
State after:
no goals