Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually (FormalBook/Chapter_02.lean)

State before:
n : ℕ
n_big : 512 ≤ n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
by_contra no_prime
State after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ False

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ False
Tactic:
have H1 : n * (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := bertrand_main_inequality n_big
State after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ False

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ False
Tactic:
have H2 : 4 ^ n < n * n.centralBinom :=
  Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_big)
State after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False
Tactic:
have H3 : n.centralBinom ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) :=
  centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_big) no_prime
State after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False
Tactic:
rw [mul_assoc] at H1
State after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False
Tactic:
exact not_le.2 H2 ((mul_le_mul_left' H3 n).trans H1)
State after:
no goals

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ 4 ≤ 512
Tactic:
norm_num1
State after:
no goals

State before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ 2 < 512
Tactic:
norm_num1
State after:
no goals