[GOAL]
r n : ℕ
⊢ choose (2 * n) (2 * n / 2) = choose (2 * n) n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left n zero_lt_two]
[GOAL]
n : ℕ
⊢ choose (2 * n + 2) (n + 1) * (n + 1) = choose (2 * n + 1) n * (2 * n + 2)
[PROOFSTEP]
rw [choose_succ_right_eq, choose_mul_succ_eq]
[GOAL]
n : ℕ
⊢ choose (2 * n + 1) n * (2 * n + 2) = 2 * (choose (2 * n + 1) n * (n + 1))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ 2 * (choose (2 * n + 1) n * (n + 1)) = 2 * (choose (2 * n + 1) n * (2 * n + 1 - n))
[PROOFSTEP]
rw [two_mul n, add_assoc, Nat.add_sub_cancel_left]
[GOAL]
n : ℕ
⊢ 2 * (choose (2 * n + 1) n * (2 * n + 1 - n)) = 2 * (choose (2 * n) n * (2 * n + 1))
[PROOFSTEP]
rw [choose_mul_succ_eq]
[GOAL]
n : ℕ
⊢ 2 * (choose (2 * n) n * (2 * n + 1)) = 2 * (2 * n + 1) * choose (2 * n) n
[PROOFSTEP]
rw [mul_assoc, mul_comm (2 * n + 1)]
[GOAL]
n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n IH
[GOAL]
case h
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
rcases lt_trichotomy n 4 with (hn | rfl | hn)
[GOAL]
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
clear IH
[GOAL]
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
exact False.elim ((not_lt.2 n_big) hn)
[GOAL]
case h.inr.inl
n : ℕ
n_big✝ : 4 ≤ n
IH : ∀ (m : ℕ), m < 4 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
case h.inr.inr
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.not_eq_zero_of_lt hn)
[GOAL]
case h.inr.inr.intro
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * centralBinom (n + 1)
[PROOFSTEP]
calc
  4 ^ (n + 1) < 4 * (n * centralBinom n) :=
    lt_of_eq_of_lt (pow_succ'' n 4) $
      (mul_lt_mul_left <| zero_lt_four' ℕ).mpr (IH n n.lt_succ_self (Nat.le_of_lt_succ hn))
  _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
  _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm
[GOAL]
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * centralBinom n) ≤ 2 * (2 * n + 1) * centralBinom n
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * centralBinom n ≤ 2 * (2 * n + 1) * centralBinom n
[PROOFSTEP]
linarith
[GOAL]
x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * (n + 4) * centralBinom (n + 4)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * ((n + 4) * centralBinom (n + 4))
[PROOFSTEP]
refine' le_mul_of_pos_left zero_lt_two
[GOAL]
n : ℕ
⊢ 2 ∣ centralBinom (n + 1)
[PROOFSTEP]
use(n + 1 + n).choose n
[GOAL]
case h
n : ℕ
⊢ centralBinom (n + 1) = 2 * choose (n + 1 + n) n
[PROOFSTEP]
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc, choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]
[GOAL]
n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom n
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos h]
[GOAL]
n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom (succ (pred n))
[PROOFSTEP]
exact two_dvd_centralBinom_succ n.pred
[GOAL]
n : ℕ
⊢ n + 1 ∣ centralBinom n
[PROOFSTEP]
have h_s : (n + 1).coprime (2 * n + 1) :=
  by
  rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
  exact coprime_one_left n
[GOAL]
n : ℕ
⊢ coprime (n + 1) (2 * n + 1)
[PROOFSTEP]
rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
[GOAL]
n : ℕ
⊢ coprime 1 n
[PROOFSTEP]
exact coprime_one_left n
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ centralBinom n
[PROOFSTEP]
apply h_s.dvd_of_dvd_mul_left
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * centralBinom n
[PROOFSTEP]
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * centralBinom n)
[PROOFSTEP]
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * centralBinom (n + 1)
[PROOFSTEP]
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)
