Theorem: ZetaSum_aux1_4' (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
x : ℝ
hx : 0 < x
s : ℂ
⊢ ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re
Tactic:
simp [map_div₀, abs_ofReal, Complex.abs_cpow_eq_rpow_re_of_pos hx, ← abs_ofReal]
State after:
no goals