# Irrational real numbers #

In this file we define a predicate Irrational on ℝ, prove that the n-th root of an integer number is irrational if it is not integer, and that √(q : ℚ) is irrational if and only if ¬IsSquare q ∧ 0 ≤ q.

We also provide dot-style constructors like Irrational.add_rat, Irrational.rat_sub etc.

With the Decidable instances in this file, is possible to prove Irrational √n using decide, when n is a numeric literal or cast; but this only works if you unseal Nat.sqrt.iter in before the theorem where you use this proof.

def Irrational (x : ) :

A real number is irrational if it is not equal to any rational number.

Equations
Instances For
theorem irrational_iff_ne_rational (x : ) :
∀ (a b : ), x a / b
theorem Transcendental.irrational {r : } (tr : ) :

A transcendental real number is irrational.

### Irrationality of roots of integer and rational numbers #

theorem irrational_nrt_of_notint_nrt {x : } (n : ) (m : ) (hxr : x ^ n = m) (hv : ¬∃ (y : ), x = y) (hnpos : 0 < n) :

If x^n, n > 0, is integer and is not the n-th power of an integer, then x is irrational.

theorem irrational_nrt_of_n_not_dvd_multiplicity {x : } (n : ) {m : } (hm : m 0) (p : ) [hp : Fact ()] (hxr : x ^ n = m) (hv : (multiplicity (p) m).get % n 0) :

If x^n = m is an integer and n does not divide the multiplicity p m, then x is irrational.

theorem irrational_sqrt_of_multiplicity_odd (m : ) (hm : 0 < m) (p : ) [hp : Fact ()] (Hpv : (multiplicity (p) m).get % 2 = 1) :
@[simp]
@[simp]
theorem irrational_sqrt_ofNat_iff {n : } [n.AtLeastTwo] :
theorem Nat.Prime.irrational_sqrt {p : } (hp : ) :

Irrationality of the Square Root of 2

@[deprecated irrational_sqrt_ratCast_iff]
theorem irrational_sqrt_rat_iff (q : ) :
q 0 q
instance instDecidableIrrationalSqrtOfNatReal {n : } [n.AtLeastTwo] :

This can be used as

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

Equations
• instDecidableIrrationalSqrtOfNatReal =

### Dot-style operations on Irrational#

#### Irrational number is not equal to a rational/integer/natural number #

theorem Irrational.ne_rat {x : } (h : ) (q : ) :
x q
theorem Irrational.ne_int {x : } (h : ) (m : ) :
x m
theorem Irrational.ne_nat {x : } (h : ) (m : ) :
x m
theorem Irrational.ne_zero {x : } (h : ) :
x 0
theorem Irrational.ne_one {x : } (h : ) :
x 1
@[simp]
theorem Irrational.ne_ofNat {x : } (h : ) (n : ) [n.AtLeastTwo] :
x
@[simp]
theorem Rat.not_irrational (q : ) :
@[simp]
theorem Int.not_irrational (m : ) :
@[simp]
theorem Nat.not_irrational (m : ) :
@[simp]
theorem not_irrational_ofNat (n : ) [n.AtLeastTwo] :

#### Addition of rational/integer/natural numbers #

theorem Irrational.add_cases {x : } {y : } :
Irrational (x + y)

If x + y is irrational, then at least one of x and y is irrational.

theorem Irrational.of_rat_add (q : ) {x : } (h : Irrational (q + x)) :
theorem Irrational.rat_add (q : ) {x : } (h : ) :
Irrational (q + x)
theorem Irrational.of_add_rat (q : ) {x : } :
Irrational (x + q)
theorem Irrational.add_rat (q : ) {x : } (h : ) :
Irrational (x + q)
theorem Irrational.of_int_add {x : } (m : ) (h : Irrational (m + x)) :
theorem Irrational.of_add_int {x : } (m : ) (h : Irrational (x + m)) :
theorem Irrational.int_add {x : } (h : ) (m : ) :
Irrational (m + x)
theorem Irrational.add_int {x : } (h : ) (m : ) :
Irrational (x + m)
theorem Irrational.of_nat_add {x : } (m : ) (h : Irrational (m + x)) :
theorem Irrational.of_add_nat {x : } (m : ) (h : Irrational (x + m)) :
theorem Irrational.nat_add {x : } (h : ) (m : ) :
Irrational (m + x)
theorem Irrational.add_nat {x : } (h : ) (m : ) :
Irrational (x + m)

#### Negation #

theorem Irrational.of_neg {x : } (h : Irrational (-x)) :
theorem Irrational.neg {x : } (h : ) :

#### Subtraction of rational/integer/natural numbers #

theorem Irrational.sub_rat (q : ) {x : } (h : ) :
Irrational (x - q)
theorem Irrational.rat_sub (q : ) {x : } (h : ) :
Irrational (q - x)
theorem Irrational.of_sub_rat (q : ) {x : } (h : Irrational (x - q)) :
theorem Irrational.of_rat_sub (q : ) {x : } (h : Irrational (q - x)) :
theorem Irrational.sub_int {x : } (h : ) (m : ) :
Irrational (x - m)
theorem Irrational.int_sub {x : } (h : ) (m : ) :
Irrational (m - x)
theorem Irrational.of_sub_int {x : } (m : ) (h : Irrational (x - m)) :
theorem Irrational.of_int_sub {x : } (m : ) (h : Irrational (m - x)) :
theorem Irrational.sub_nat {x : } (h : ) (m : ) :
Irrational (x - m)
theorem Irrational.nat_sub {x : } (h : ) (m : ) :
Irrational (m - x)
theorem Irrational.of_sub_nat {x : } (m : ) (h : Irrational (x - m)) :
theorem Irrational.of_nat_sub {x : } (m : ) (h : Irrational (m - x)) :

#### Multiplication by rational numbers #

theorem Irrational.mul_cases {x : } {y : } :
Irrational (x * y)
theorem Irrational.of_mul_rat (q : ) {x : } (h : Irrational (x * q)) :
theorem Irrational.mul_rat {x : } (h : ) {q : } (hq : q 0) :
Irrational (x * q)
theorem Irrational.of_rat_mul (q : ) {x : } :
Irrational (q * x)
theorem Irrational.rat_mul {x : } (h : ) {q : } (hq : q 0) :
Irrational (q * x)
theorem Irrational.of_mul_int {x : } (m : ) (h : Irrational (x * m)) :
theorem Irrational.of_int_mul {x : } (m : ) (h : Irrational (m * x)) :
theorem Irrational.mul_int {x : } (h : ) {m : } (hm : m 0) :
Irrational (x * m)
theorem Irrational.int_mul {x : } (h : ) {m : } (hm : m 0) :
Irrational (m * x)
theorem Irrational.of_mul_nat {x : } (m : ) (h : Irrational (x * m)) :
theorem Irrational.of_nat_mul {x : } (m : ) (h : Irrational (m * x)) :
theorem Irrational.mul_nat {x : } (h : ) {m : } (hm : m 0) :
Irrational (x * m)
theorem Irrational.nat_mul {x : } (h : ) {m : } (hm : m 0) :
Irrational (m * x)

#### Inverse #

theorem Irrational.of_inv {x : } (h : ) :
theorem Irrational.inv {x : } (h : ) :

#### Division #

theorem Irrational.div_cases {x : } {y : } (h : Irrational (x / y)) :
theorem Irrational.of_rat_div (q : ) {x : } (h : Irrational (q / x)) :
theorem Irrational.of_div_rat (q : ) {x : } (h : Irrational (x / q)) :
theorem Irrational.rat_div {x : } (h : ) {q : } (hq : q 0) :
Irrational (q / x)
theorem Irrational.div_rat {x : } (h : ) {q : } (hq : q 0) :
Irrational (x / q)
theorem Irrational.of_int_div {x : } (m : ) (h : Irrational (m / x)) :
theorem Irrational.of_div_int {x : } (m : ) (h : Irrational (x / m)) :
theorem Irrational.int_div {x : } (h : ) {m : } (hm : m 0) :
Irrational (m / x)
theorem Irrational.div_int {x : } (h : ) {m : } (hm : m 0) :
Irrational (x / m)
theorem Irrational.of_nat_div {x : } (m : ) (h : Irrational (m / x)) :
theorem Irrational.of_div_nat {x : } (m : ) (h : Irrational (x / m)) :
theorem Irrational.nat_div {x : } (h : ) {m : } (hm : m 0) :
Irrational (m / x)
theorem Irrational.div_nat {x : } (h : ) {m : } (hm : m 0) :
Irrational (x / m)
theorem Irrational.of_one_div {x : } (h : Irrational (1 / x)) :

#### Natural and integer power #

theorem Irrational.of_mul_self {x : } (h : Irrational (x * x)) :
theorem Irrational.of_pow {x : } (n : ) :
Irrational (x ^ n)
theorem Irrational.of_zpow {x : } (m : ) :
Irrational (x ^ m)
theorem one_lt_natDegree_of_irrational_root (x : ) (p : ) (hx : ) (p_nonzero : p 0) (x_is_root : () p = 0) :
1 < p.natDegree

### Simplification lemmas about operations #

@[simp]
theorem irrational_rat_add_iff {q : } {x : } :
Irrational (q + x)
@[simp]
theorem irrational_int_add_iff {m : } {x : } :
Irrational (m + x)
@[simp]
theorem irrational_nat_add_iff {n : } {x : } :
Irrational (n + x)
@[simp]
theorem irrational_add_rat_iff {q : } {x : } :
Irrational (x + q)
@[simp]
theorem irrational_add_int_iff {m : } {x : } :
Irrational (x + m)
@[simp]
theorem irrational_add_nat_iff {n : } {x : } :
Irrational (x + n)
@[simp]
theorem irrational_rat_sub_iff {q : } {x : } :
Irrational (q - x)
@[simp]
theorem irrational_int_sub_iff {m : } {x : } :
Irrational (m - x)
@[simp]
theorem irrational_nat_sub_iff {n : } {x : } :
Irrational (n - x)
@[simp]
theorem irrational_sub_rat_iff {q : } {x : } :
Irrational (x - q)
@[simp]
theorem irrational_sub_int_iff {m : } {x : } :
Irrational (x - m)
@[simp]
theorem irrational_sub_nat_iff {n : } {x : } :
Irrational (x - n)
@[simp]
@[simp]
theorem irrational_inv_iff {x : } :
@[simp]
theorem irrational_rat_mul_iff {q : } {x : } :
Irrational (q * x) q 0
@[simp]
theorem irrational_mul_rat_iff {q : } {x : } :
Irrational (x * q) q 0
@[simp]
theorem irrational_int_mul_iff {m : } {x : } :
Irrational (m * x) m 0
@[simp]
theorem irrational_mul_int_iff {m : } {x : } :
Irrational (x * m) m 0
@[simp]
theorem irrational_nat_mul_iff {n : } {x : } :
Irrational (n * x) n 0
@[simp]
theorem irrational_mul_nat_iff {n : } {x : } :
Irrational (x * n) n 0
@[simp]
theorem irrational_rat_div_iff {q : } {x : } :
Irrational (q / x) q 0
@[simp]
theorem irrational_div_rat_iff {q : } {x : } :
Irrational (x / q) q 0
@[simp]
theorem irrational_int_div_iff {m : } {x : } :
Irrational (m / x) m 0
@[simp]
theorem irrational_div_int_iff {m : } {x : } :
Irrational (x / m) m 0
@[simp]
theorem irrational_nat_div_iff {n : } {x : } :
Irrational (n / x) n 0
@[simp]
theorem irrational_div_nat_iff {n : } {x : } :
Irrational (x / n) n 0
theorem exists_irrational_btwn {x : } {y : } (h : x < y) :
∃ (r : ), x < r r < y

There is an irrational number r between any two reals x < r < y.