Theorem: prodPrimesSplit (FromTheBook/Ch02/Bertrand/Util.lean)

State before:
b a : ℕ
ha : a ≤ b
⊢ prodPrimes b = prodPrimes a * ∏ p in primes (Finset.Ioc a b), p
Tactic:
rw [← Nat.Ico_succ_succ]
State after:
b a : ℕ
ha : a ≤ b
⊢ prodPrimes b = prodPrimes a * ∏ p in primes (Finset.Ico (Nat.succ a) (Nat.succ b)), p

State before:
b a : ℕ
ha : a ≤ b
⊢ prodPrimes b = prodPrimes a * ∏ p in primes (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Tactic:
simp [prodPrimes, primes]
State after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p

State before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Tactic:
rw [Finset.range_eq_Ico]
State after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p

State before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Tactic:
rw [← Finset.prod_union]
State after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x

b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))

State before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x

b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Tactic:
. rw [← Finset.filter_union]
  rw [Finset.Ico_union_Ico_eq_Ico (Nat.zero_le a.succ) (Nat.succ_le_succ ha)]
State after:
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))

State before:
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Tactic:
. apply Finset.disjoint_filter_filter
  apply Finset.Ico_disjoint_Ico_consecutive
State after:
no goals

State before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x
Tactic:
rw [← Finset.filter_union]
State after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a) ∪ Finset.Ico (Nat.succ a) (Nat.succ b)), x

State before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a) ∪ Finset.Ico (Nat.succ a) (Nat.succ b)), x
Tactic:
rw [Finset.Ico_union_Ico_eq_Ico (Nat.zero_le a.succ) (Nat.succ_le_succ ha)]
State after:
no goals

State before:
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Tactic:
apply Finset.disjoint_filter_filter
State after:
case a
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.Ico 0 (Nat.succ a)) (Finset.Ico (Nat.succ a) (Nat.succ b))

State before:
case a
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.Ico 0 (Nat.succ a)) (Finset.Ico (Nat.succ a) (Nat.succ b))
Tactic:
apply Finset.Ico_disjoint_Ico_consecutive
State after:
no goals