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

State before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ ∏ p in primes (Finset.Ioc a b), p
Tactic:
rw [primes]
State after:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p

State before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p
Tactic:
rw [← @Finset.prod_filter_of_ne _ _ _ _ _ Nat.Prime]
State after:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ x in Finset.filter Nat.Prime (Finset.Ioc a b), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p

case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x

State before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ x in Finset.filter Nat.Prime (Finset.Ioc a b), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p

case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x
Tactic:
. apply Finset.prod_le_prod'
  simp
  intro p hbp _ hp
  replace hbp := lt_of_le_of_lt ha hbp
  conv => rhs; rw [← Nat.pow_one p]
  rw [pow_le_pow_iff (Nat.Prime.one_lt hp)]
  rw [Nat.sqrt_lt'] at hbp
  exact leOne hp hbp
State after:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x

State before:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x
Tactic:
. intro p _
  apply primeOfPowFactorizationNeOne
State after:
no goals

State before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ x in Finset.filter Nat.Prime (Finset.Ioc a b), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p
Tactic:
apply Finset.prod_le_prod'
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), i ∈ Finset.filter Nat.Prime (Finset.Ioc a b) → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), i ∈ Finset.filter Nat.Prime (Finset.Ioc a b) → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
Tactic:
simp
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), a < i → i ≤ b → Nat.Prime i → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), a < i → i ≤ b → Nat.Prime i → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
Tactic:
intro p hbp _ hp
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
hbp : a < p
a✝ : p ≤ b
hp : Nat.Prime p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
hbp : a < p
a✝ : p ≤ b
hp : Nat.Prime p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p
Tactic:
replace hbp := lt_of_le_of_lt ha hbp
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p
Tactic:
conv => rhs; rw [← Nat.pow_one p]
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p ^ 1

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p ^ 1
Tactic:
rw [pow_le_pow_iff (Nat.Prime.one_lt hp)]
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
rw [Nat.sqrt_lt'] at hbp
State after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1

State before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
exact leOne hp hbp
State after:
no goals

State before:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x
Tactic:
intro p _
State after:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ∈ Finset.Ioc a b
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≠ 1 → Nat.Prime p

State before:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ∈ Finset.Ioc a b
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≠ 1 → Nat.Prime p
Tactic:
apply primeOfPowFactorizationNeOne
State after:
no goals