sqrt2 irrational

Stream: new members

[Hank]

I tried to argue that 2 ∣ a*a implies 2 ∣ a because 2 is prime (see have a_even : 2 ∣ a below). I want to use the theorem nat.prime.dvd_mul, but there are always errors when I try to use it. How should I use it?

import data.nat.prime -- for nat.prime.dvd_mul
theorem sqrt2_irrational (a b : ℕ) (h : gcd a b = 1) : a * a ≠ 2 * b * b :=
begin
  by_contradiction,
  have a2_even: 2 ∣ a*a,
    rw h,
    rw mul_assoc,
    exact dvd.intro (b * b) rfl,

  have a_even : 2 ∣ a,
    rw nat.prime.dvd_mul (nat.prime 2) at a2_even, -- problem here
end

[Ruben Van de Velde]

How does it fail?

[Hank]

If I do rw nat.prime.dvd_mul (nat.prime 2) at a2_even, I get the error message

type mismatch at application
  nat.prime.dvd_mul (nat.prime 2)
term
  nat.prime 2
has type
  Prop : Type
but is expected to have type
  nat.prime ?m_1 : Prop

If I do rw nat.prime.dvd_mul 2 a a (nat.prime 2) at a2_even, I get the error message

invalid pre-numeral, universe level must be > 0

I don't know how to use this theorem correctly and would appreciate any guidance.

[Reid Barton]

You're putting the type nat.prime 2 where a proof that 2 is prime is needed.

[Reid Barton]

Instead you could use, for instance, docs#nat.prime_two

[Reid Barton]

or by norm_num