Theorem: BrunTitchmarsh.rem_eq (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).rem d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Tactic:
unfold Sieve.rem
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).multSum d - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).multSum d - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Tactic:
rw[multSum_eq x y z hx hz d hd]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Tactic:
simp [primeInterSieve, if_neg hd]
State after:
no goals