[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' (k + n) ≤ card (filter Prime (range k)) + card (filter Prime (Ico k (k + n)))
[PROOFSTEP]
rw [primeCounting', count_eq_card_filter_range, range_eq_Ico, ← Ico_union_Ico_eq_Ico (zero_le k) le_self_add,
  filter_union]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ card (filter Prime (Ico 0 k) ∪ filter Prime (Ico k (k + n))) ≤
    card (filter Prime (Ico 0 k)) + card (filter Prime (Ico k (k + n)))
[PROOFSTEP]
apply card_union_le
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ card (filter Prime (range k)) + card (filter Prime (Ico k (k + n))) ≤ π' k + card (filter Prime (Ico k (k + n)))
[PROOFSTEP]
rw [primeCounting', count_eq_card_filter_range]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' k + card (filter Prime (Ico k (k + n))) ≤ π' k + card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
refine' add_le_add_left (card_le_of_subset _) k.primeCounting'
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ filter Prime (Ico k (k + n)) ⊆ filter (coprime a) (Ico k (k + n))
[PROOFSTEP]
simp only [subset_iff, and_imp, mem_filter, mem_Ico]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ ∀ ⦃x : ℕ⦄, k ≤ x → x < k + n → Prime x → (k ≤ x ∧ x < k + n) ∧ coprime a x
[PROOFSTEP]
intro p succ_k_le_p p_lt_n p_prime
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ (k ≤ p ∧ p < k + n) ∧ coprime a p
[PROOFSTEP]
constructor
[GOAL]
case left
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ k ≤ p ∧ p < k + n
[PROOFSTEP]
exact ⟨succ_k_le_p, p_lt_n⟩
[GOAL]
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ coprime a p
[PROOFSTEP]
rw [coprime_comm]
[GOAL]
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ coprime p a
[PROOFSTEP]
exact coprime_of_lt_prime h0 (gt_of_ge_of_gt succ_k_le_p h1) p_prime
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' k + card (filter (coprime a) (Ico k (k + n))) ≤ π' k + φ a * (n / a + 1)
[PROOFSTEP]
rw [add_le_add_iff_left]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ card (filter (coprime a) (Ico k (k + n))) ≤ φ a * (n / a + 1)
[PROOFSTEP]
exact Ico_filter_coprime_le k n h0
