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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ primesBetween a b ≤ primesBetween a c
Tactic:
dsimp only [primesBetween]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊)).card ≤ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)).card

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊)).card ≤ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)).card
Tactic:
apply Finset.card_le_card
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) ⊆ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) ⊆ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)
Tactic:
intro p
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) → p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) → p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)
Tactic:
simp only [Finset.mem_filter, Finset.mem_Icc, Nat.ceil_le, and_imp]
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ a ≤ ↑p → p ≤ ⌊b⌋₊ → p.Prime → (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ a ≤ ↑p → p ≤ ⌊b⌋₊ → p.Prime → (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime
Tactic:
intro ha hb hp
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
ha : a ≤ ↑p
hb : p ≤ ⌊b⌋₊
hp : p.Prime
⊢ (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
ha : a ≤ ↑p
hb : p ≤ ⌊b⌋₊
hp : p.Prime
⊢ (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime
Tactic:
refine ⟨⟨ha, hb.trans (Nat.floor_mono hbc)⟩, hp⟩
State after:
no goals