ProveIt.lean

-- This line imports the necessary definitions for real numbers.
import Mathlib.Data.Real.Basic
-- This line imports the definition of the square root function.
import Mathlib.Data.Real.Sqrt
-- This line imports the definition of the real power function.
import Mathlib.Analysis.SpecialFunctions.Pow.Real
-- This line imports tactics for numerical simplification.
import Mathlib.Tactic.NormNum
-- This line imports theorems about binomial coefficients.
import Mathlib.Data.Nat.Choose.Sum
-- This line imports theorems about powers of numbers.
import Mathlib.Algebra.GroupPower.Basic

-- This line opens the `Real` namespace, so we can write `sqrt` instead of `Real.sqrt`.
open Real

-- Type-level guarantee: A Digit is a natural number guaranteed to be less than 10
def Digit := {n : ℕ // n < 10}

-- This is the number we are interested in.
def problem_val := (sqrt 2 + sqrt 3)^2012

-- INTERMEDIATE THEOREM 1: The square of (√2 + √3) equals 5 + 2√6
-- This is a key algebraic simplification that makes the proof tractable
theorem sqrt_sum_squared : (sqrt 2 + sqrt 3)^2 = 5 + 2 * sqrt 6 :=
begin
  rw [add_sq (sqrt 2) (sqrt 3)],
  rw [sq_sqrt (by norm_num : (0 : ℝ) ≤ 2), sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)],
  rw [mul_comm (sqrt 2) (sqrt 3), ← sqrt_mul (by norm_num : (0 : ℝ) ≤ 2 * 3)],
  norm_num,
end

-- INTERMEDIATE THEOREM 2: The conjugate (√3 - √2)^2 also simplifies nicely
theorem conjugate_squared : (sqrt 3 - sqrt 2)^2 = 5 - 2 * sqrt 6 :=
begin
  rw [sub_sq (sqrt 3) (sqrt 2)],
  rw [sq_sqrt (by norm_num : (0 : ℝ) ≤ 3), sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)],
  rw [mul_comm (sqrt 2) (sqrt 3), ← sqrt_mul (by norm_num : (0 : ℝ) ≤ 2 * 3)],
  norm_num,
end

-- INTERMEDIATE THEOREM 3: The conjugate raised to 2012 is extremely small
-- This is crucial for proving that the fractional part has many 9s
theorem conjugate_is_tiny : (sqrt 3 - sqrt 2)^2012 < 10^(-500 : ℝ) :=
begin
  -- Rewrite using the squared form
  rw [← pow_mul],
  have h_conj_sq : (sqrt 3 - sqrt 2)^2 = 5 - 2 * sqrt 6 := conjugate_squared,
  rw [h_conj_sq],
  
  let y := 5 - 2 * sqrt 6,
  
  -- Show y < 1/9
  have h_y_lt_1_9 : y < 1/9,
  {
    unfold_let y,
    rw [sub_lt_comm, ← div_lt_iff' (by norm_num)],
    norm_num,
    rw [lt_sub_iff_add_lt, ← add_lt_add_iff_left (2 * sqrt 6)],
    norm_num,
    apply lt_of_pow_lt_pow_left,
    norm_num,
    rw [sq_sqrt, mul_pow],
    norm_num,
  },
  
  -- Show (1/9)^1006 < 10^(-500)
  have h_pow_lt : y^1006 < (1/9)^1006,
  {
    apply pow_lt_pow_of_lt_left h_y_lt_1_9,
    norm_num,
    norm_num,
  },
  
  have h_10_pow_500 : (1/9 : ℝ)^1006 < 10^(-500 : ℝ),
  {
    rw [div_pow, one_pow, ← rpow_neg_one, ← rpow_nat_cast, ← rpow_mul],
    rw [← rpow_neg_one, ← rpow_nat_cast],
    apply rpow_lt_rpow_of_exponent_lt,
    norm_num,
    rw [neg_lt_neg_iff, mul_lt_mul_left (by norm_num)],
    apply log_lt_log,
    norm_num,
    norm_num,
  },
  
  exact lt_trans h_pow_lt h_10_pow_500,
end

-- This function returns the nth digit of a real number after the decimal point.
def get_nth_digit (x : ℝ) (n : ℕ) : ℕ :=
  -- First, we get the fractional part of the number.
  let frac_part := x - ⌊x⌋
  -- Then, we scale the fractional part by 10^n to move the nth digit to the units place.
  let scaled := frac_part * (10^n)
  -- Finally, we take the floor of the scaled number, convert it to a natural number, and take the result modulo 10.
  ⌊scaled⌋.toNat % 10

-- Type-safe version: Returns a Digit type, guaranteeing the result is 0-9
def get_nth_digit_typed (x : ℝ) (n : ℕ) : Digit :=
  let result := get_nth_digit x n
  -- The modulo 10 operation ensures the result is always < 10
  ⟨result, by {
    have h : result < 10 := nat.mod_lt result (by norm_num : 0 < 10),
    exact h
  }⟩

-- This is the main lemma of the proof. It proves two things:
-- 1. `problem_val + (sqrt 3 - sqrt 2)^2012` is an integer.
-- 2. `0 < (sqrt 3 - sqrt 2)^2012 < 10^(-500)`.
lemma sum_is_int_and_small_conjugate : (∃ (k : ℤ), problem_val + (sqrt 3 - sqrt 2)^2012 = k) ∧ (0 < (sqrt 3 - sqrt 2)^2012 ∧ (sqrt 3 - sqrt 2)^2012 < 10^(-500)) :=
begin
  -- We first rewrite `problem_val` as `(5 + 2 * sqrt 6)^1006`.
  have h_problem_val_rw : problem_val = (5 + 2 * sqrt 6)^1006,
  {
    -- This is done by squaring `(sqrt 2 + sqrt 3)` and then raising the result to the power of 1006.
    rw [problem_val, ← pow_mul, add_sq (sqrt 2) (sqrt 3)],
    norm_num,
    rw [sq_sqrt (by norm_num), sq_sqrt (by norm_num)],
    norm_num,
    rw mul_comm (sqrt 2) (sqrt 3),
    rw ← sqrt_mul (by norm_num),
    norm_num,
  },
  -- We do the same for the conjugate value.
  have h_conjugate_val_rw : (sqrt 3 - sqrt 2)^2012 = (5 - 2 * sqrt 6)^1006,
  {
    rw [← pow_mul, sub_sq (sqrt 3) (sqrt 2)],
    norm_num,
    rw [sq_sqrt (by norm_num), sq_sqrt (by norm_num)],
    norm_num,
    rw mul_comm (sqrt 2) (sqrt 3),
    rw ← sqrt_mul (by norm_num),
    norm_num,
  },
  -- We now work with the rewritten values.
  rw [h_problem_val_rw, h_conjugate_val_rw],
  let x := 5 + 2 * sqrt 6,
  let y := 5 - 2 * sqrt 6,
  let n := 1006,
  -- We prove that the sum is an integer.
  have h_sum_is_int : ∃ (k : ℤ), x^n + y^n = k,
  {
    let u := 2 * sqrt 6,
    let v := 5,
    have h_x_v_u : x = v + u := by { simp [x, v, u] },
    have h_y_v_u : y = v - u := by { simp [y, v, u] },
    rw [h_x_v_u, h_y_v_u],
    -- We use the binomial theorem to expand both terms.
    rw [add_pow, add_pow],
    -- We combine the two sums.
    rw ← finset.sum_add_distrib,
    -- We show that the sum is equal to an integer.
    use 2 * (finset.range 504).sum (λ i, (nat.choose 1006 (2*i)) * 5^(1006-2*i) * 24^i),
    norm_cast,
    rw ← finset.sum_even_inds', 
    apply finset.sum_congr rfl,
    intros k hk,
    simp only [finset.mem_range] at hk,
    -- The terms with odd powers of `sqrt 6` cancel out.
    rw [pow_add_neg_pow_of_even (by simp [even_mul])],
    rw [pow_mul, ← mul_pow, ← sq_sqrt (by norm_num)],
    ring,
  },
  -- We now have the two parts of the proof.
  split,
  { exact h_sum_is_int },
  {
    let y := 5 - 2 * sqrt 6,
    -- We prove that the conjugate is positive.
    have h_y_pos : 0 < y, by { norm_num, rw sub_pos, apply lt_of_pow_lt_pow_left, norm_num, rw sq_sqrt, norm_num },
    split,
    { apply pow_pos h_y_pos },
    {
      -- We prove that the conjugate is less than 1/9.
      have h_y_lt_1_9 : y < 1/9,
      {
        rw [y, sub_lt_comm, ← div_lt_iff' (by norm_num)],
        norm_num,
        rw [lt_sub_iff_add_lt, ← add_lt_add_iff_left (2*sqrt 6)],
        norm_num,
        apply lt_of_pow_lt_pow_left, 
        norm_num,
        rw [sq_sqrt, mul_pow], 
        norm_num,
      },
      -- We raise this inequality to the power of 1006.
      have h_pow_lt : y^1006 < (1/9)^1006, from pow_lt_pow_of_lt_left h_y_lt_1_9 (by norm_num) (by norm_num),
      -- We use logarithms to show that `(1/9)^1006 < 10^(-500)`.
      have h_10_pow_500 : (1/9)^1006 < 10^(-500),
      {
        rw [div_pow, one_pow, ← rpow_neg_one, ← rpow_nat_cast, ← rpow_mul, ← rpow_neg_one, ← rpow_nat_cast],
        apply rpow_lt_rpow_of_exponent_lt,
        norm_num,
        rw [neg_lt_neg_iff, mul_lt_mul_left (by norm_num)],
        apply log_lt_log,
        norm_num,
        norm_num,
      },
      -- We combine the inequalities.
      exact lt_trans h_pow_lt h_10_pow_500,
    },
  },
end

-- This is the main theorem.
theorem prove_it_is_9 : get_nth_digit problem_val 500 = 9 :=
begin
  -- We use the lemma we just proved.
  rcases sum_is_int_and_small_conjugate with ⟨⟨k, hk_sum⟩, ⟨h_conj_pos, h_conj_small⟩⟩,
  -- We rewrite the goal using the definition of `get_nth_digit`.
  rw [get_nth_digit, problem_val],
  -- We use the fact that the sum is an integer.
  rw hk_sum,
  -- We compute the floor of `k - conjugate_val`.
  have h_floor : ⌊(k : ℝ) - (sqrt 3 - sqrt 2) ^ 2012⌋ = k - 1,
  {
    rw floor_sub_int,
    apply floor_eq_zero_iff.mpr,
    split,
    { linarith },
    { apply pow_lt_one; linarith [sqrt_lt_sqrt.mpr (by norm_num)] },
  },
  rw h_floor,
  -- We simplify the expression for the scaled fractional part.
  rw [sub_sub_cancel, ← one_sub_pow, ← mul_sub, ← one_mul (10^500)],
  -- We compute the floor of the scaled fractional part.
  have h_floor_scaled : ⌊10^500 - (sqrt 3 - sqrt 2)^2012 * 10^500⌋ = 10^500 - 1,
  {
    rw floor_sub_int,
    apply floor_eq_zero_iff.mpr,
    split,
    { apply mul_pos, apply pow_pos, linarith [sqrt_lt_sqrt.mpr (by norm_num)] },
    { rw [← div_lt_iff' (pow_pos (by norm_num) 500), one_div],
      exact h_conj_small,
    },
  },
  rw h_floor_scaled,
  -- We compute the final result modulo 10.
  rw [int.to_nat_sub, nat.sub_one, nat.mod_eq_of_lt],
  { norm_num },
  { apply nat.one_le_pow, norm_num, norm_num },
end