casting between rational/real

Stream: new members

[Meyer Zinn]

I'm trying to show that irrational_sqrt_two -> rat.sqrt(2) * rat.sqrt(2) \ne 2. mathlib comes with a proof that the sqrt of 2 : R is irrational, but the irrational_sqrt_rat_iff theorem takes a proof that the sqrt of 2 : Q is irrational. How should I approach this? Do I need a lemma that the sqrt of 2 : Q is irrational using the fact that sqrt 2 : R is irrational?

[Meyer Zinn]

Actually, I just realized this approach doesn't make sense, since rat.sqrt is not related to real.sqrt (I think?)

[Meyer Zinn]

Will need to find a different proof approach. My ultimate goal is to show that there is no integer $n$ such that $n^2=2$.

[Yakov Pechersky]

For all n : Z, n <= n * n. So if n * n = 2, then n <= 2. Split on -2 and below, 2, then finish on case bash on -1, 0, 1?

[Bryan Gin-ge Chen]

This is a little slow, but it works:

import tactic
example : ¬ (∃ (n : ℤ), n * n = 2) :=
begin
  push_neg,
  intros n hn,
  by_cases h : 2 ≤ abs n,
  { have : 4 ≤ (abs n)*(abs n) := calc
      4 = 2*2 : dec_trivial
      ... ≤ (abs n) * (abs n) : mul_le_mul h h dec_trivial (le_trans dec_trivial h),
    rw [←abs_mul_abs_self] at hn,
    linarith },
  { simp only [abs_lt, not_le] at h,
    obtain ⟨h₁, h₂⟩ := h,
    interval_cases n,
    all_goals { linarith } }
end

[Bryan Gin-ge Chen]

Here's a similar proof using Yakov's idea:

import tactic

-- this seems to be missing from mathlib?
lemma int.le_mul_self (n : ℤ) : n ≤ n * n :=
begin
  rw [←int.nat_abs_mul_self'],
  calc n ≤ (n.nat_abs : ℤ) : int.le_nat_abs
     ... ≤ _ : by exact_mod_cast nat.le_mul_self _,
end

example : ¬ (∃ (n : ℤ), n * n = 2) :=
begin
  push_neg,
  intros n hn,
  by_cases h : 2 < abs n,
  { rw [←abs_mul_abs_self] at hn,
    have : abs n ≤ 2 := by { rw ←hn, exact int.le_mul_self _ },
    linarith },
  { simp only [abs_le, not_lt] at h,
    obtain ⟨h₁, h₂⟩ := h,
    interval_cases n,
    all_goals { linarith } }
end

[Mario Carneiro]

What is docs#rat.sqrt?

[Mario Carneiro]

rat.sqrt 2 is garbage

[Mario Carneiro]

Here's a proof that actually uses irrational_sqrt_two instead of reproving it:

import data.rat.sqrt data.real.irrational

example : ¬ ∃ (n : ℤ), n * n = 2 :=
begin
  rintro ⟨n, e⟩,
  apply (irrational_iff_ne_rational _).1 irrational_sqrt_two (abs n) 1,
  simp,
  rw [real.sqrt_eq_iff_mul_self_eq _ (abs_nonneg _), ← abs_mul, abs_mul_self],
  {exact_mod_cast e}, {norm_num},
end