# Zulip Chat Archive

## Stream: new members

### Topic: casting between rational/real

#### Meyer Zinn (Nov 08 2020 at 23:52):

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 (Nov 08 2020 at 23:53):

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

#### Meyer Zinn (Nov 08 2020 at 23:54):

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 (Nov 09 2020 at 00:24):

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 (Nov 09 2020 at 00:34):

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 (Nov 09 2020 at 00:57):

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 (Nov 09 2020 at 01:17):

What is docs#rat.sqrt?

#### Mario Carneiro (Nov 09 2020 at 01:18):

`rat.sqrt 2`

is garbage

#### Mario Carneiro (Nov 09 2020 at 01:28):

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
```

Last updated: May 14 2021 at 06:16 UTC