Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.range b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p
Tactic:
rw [Finset.range_eq_Ico]
State after:
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.Ico 0 b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p

State before:
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.Ico 0 b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p
Tactic:
rw [← Finset.prod_subset (Finset.Ico_subset_Ico_left (Nat.zero_le a)) _]
State after:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 0 b → ¬x ∈ Finset.Ico a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1

State before:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 0 b → ¬x ∈ Finset.Ico a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
simp
State after:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x < b → (a ≤ x → b ≤ x) → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1

State before:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x < b → (a ≤ x → b ≤ x) → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
intro x hxb hbx
State after:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1

State before:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
rw [Nat.factorization_eq_zero_of_non_prime]
State after:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ 0 = 1

case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x

State before:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ 0 = 1

case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x
Tactic:
simp
State after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x

State before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x
Tactic:
intro hp
State after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp : Nat.Prime x
⊢ False

State before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp : Nat.Prime x
⊢ False
Tactic:
have hp := Nat.Prime.two_le hp
State after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp✝ : Nat.Prime x
hp : 2 ≤ x
⊢ False

State before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp✝ : Nat.Prime x
hp : 2 ≤ x
⊢ False
Tactic:
specialize hbx (le_trans ha hp)
State after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hp✝ : Nat.Prime x
hp : 2 ≤ x
hbx : b ≤ x
⊢ False

State before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hp✝ : Nat.Prime x
hp : 2 ≤ x
hbx : b ≤ x
⊢ False
Tactic:
linarith
State after:
no goals