Theorem: prodPrimesLePowFour (FromTheBook/Ch02/Bertrand/ProdPrimes.lean)

State before:
n : ℕ
⊢ prodPrimes n ≤ 4 ^ Nat.pred n
Tactic:
induction n using caseStrongRecOnOddPrimes with
| zero => simp
| two => simp
| not_prime n hp hi =>
  specialize hi n
  simp at hi
  cases n with
  | zero => simp
  | succ n =>
    simp only [Nat.pred_succ] at *
    simp [prodPrimes]
    rw [primesSuccEqPrimesSelf hp, Nat.add_one]
    rw [← prodPrimes, Nat.add_one]
    apply le_trans hi
    simp [pow_succ]
| odd_prime n hp hi =>
  simp
  conv => rhs; rw [two_mul, pow_add]
  specialize hi n.succ _
  . cases n with
    | zero => contradiction  | succ n => linarith
  simp at hi
  rw [prodPrimesSplit (by linarith : n.succ ≤ (2*n).succ)]
  apply Nat.mul_le_mul hi
  apply le_trans _ chooseHalfLePowFour
  exact prodPrimesIocLeChoose
State after:
no goals

State before:
case zero

⊢ prodPrimes 0 ≤ 4 ^ Nat.pred 0
Tactic:
simp
State after:
no goals

State before:
case two

⊢ prodPrimes 2 ≤ 4 ^ Nat.pred 2
Tactic:
simp
State after:
no goals

State before:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : ∀ (x : ℕ), x ≤ n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Tactic:
specialize hi n
State after:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : n ≤ n → prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)

State before:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : n ≤ n → prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Tactic:
simp at hi
State after:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)

State before:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Tactic:
cases n with
| zero => simp
| succ n =>
  simp only [Nat.pred_succ] at *
  simp [prodPrimes]
  rw [primesSuccEqPrimesSelf hp, Nat.add_one]
  rw [← prodPrimes, Nat.add_one]
  apply le_trans hi
  simp [pow_succ]
State after:
no goals

State before:
case not_prime.zero
hp : ¬Nat.Prime (Nat.succ Nat.zero)
hi : prodPrimes Nat.zero ≤ 4 ^ Nat.pred Nat.zero
⊢ prodPrimes (Nat.succ Nat.zero) ≤ 4 ^ Nat.pred (Nat.succ Nat.zero)
Tactic:
simp
State after:
no goals

State before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ Nat.pred (Nat.succ (Nat.succ n))
Tactic:
simp only [Nat.pred_succ] at *
State after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ (n + 1)

State before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ (n + 1)
Tactic:
simp [prodPrimes]
State after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ (Nat.succ n)))), p ≤ 4 ^ (n + 1)

State before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ (Nat.succ n)))), p ≤ 4 ^ (n + 1)
Tactic:
rw [primesSuccEqPrimesSelf hp, Nat.add_one]
State after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ n))), p ≤ 4 ^ Nat.succ n

State before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ n))), p ≤ 4 ^ Nat.succ n
Tactic:
rw [← prodPrimes, Nat.add_one]
State after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.succ n

State before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.succ n
Tactic:
apply le_trans hi
State after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ 4 ^ n ≤ 4 ^ Nat.succ n

State before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ 4 ^ n ≤ 4 ^ Nat.succ n
Tactic:
simp [pow_succ]
State after:
no goals

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ Nat.pred (Nat.succ (2 * n))
Tactic:
simp
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ (2 * n)

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ (2 * n)
Tactic:
conv => rhs; rw [two_mul, pow_add]
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
specialize hi n.succ _
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n

case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n

case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
. cases n with
  | zero => contradiction  | succ n => linarith
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
simp at hi
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
rw [prodPrimesSplit (by linarith : n.succ ≤ (2*n).succ)]
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) * ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n * 4 ^ n

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) * ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n * 4 ^ n
Tactic:
apply Nat.mul_le_mul hi
State after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n
Tactic:
apply le_trans _ chooseHalfLePowFour
State after:
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ Nat.choose (2 * n + 1) n

State before:
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ Nat.choose (2 * n + 1) n
Tactic:
exact prodPrimesIocLeChoose
State after:
no goals

State before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n
Tactic:
cases n with
| zero => contradiction  | succ n => linarith
State after:
no goals

State before:
case odd_prime.zero
hp : Nat.Prime (Nat.succ (2 * Nat.zero))
hi : ∀ (x : ℕ), x ≤ 2 * Nat.zero → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ Nat.zero ≤ 2 * Nat.zero
Tactic:
contradiction
State after:
no goals

State before:
case odd_prime.succ
n : ℕ
hp : Nat.Prime (Nat.succ (2 * Nat.succ n))
hi : ∀ (x : ℕ), x ≤ 2 * Nat.succ n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ (Nat.succ n) ≤ 2 * Nat.succ n
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ Nat.succ n ≤ Nat.succ (2 * n)
Tactic:
linarith
State after:
no goals