[GOAL]
x : ℝ
⊢ Irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b
[PROOFSTEP]
simp only [Irrational, Rat.forall, cast_mk, not_exists, Set.mem_range, cast_coe_int, cast_div, eq_comm]
[GOAL]
r : ℝ
tr : Transcendental ℚ r
⊢ Irrational r
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
a : ℚ
tr : Transcendental ℚ ↑a
⊢ False
[PROOFSTEP]
exact tr (isAlgebraic_algebraMap a)
[GOAL]
x : ℝ
n : ℕ
m : ℤ
hxr : x ^ n = ↑m
hv : ¬∃ y, x = ↑y
hnpos : 0 < n
⊢ Irrational x
[PROOFSTEP]
rintro ⟨⟨N, D, P, C⟩, rfl⟩
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D) ^ n = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
[PROOFSTEP]
rw [← cast_pow] at hxr 
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
[PROOFSTEP]
have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
  rw [Int.cast_ne_zero, Int.coe_nat_ne_zero]
  exact P
[GOAL]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ ↑↑D ≠ 0
[PROOFSTEP]
rw [Int.cast_ne_zero, Int.coe_nat_ne_zero]
[GOAL]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ D ≠ 0
[PROOFSTEP]
exact P
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
⊢ False
[PROOFSTEP]
have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
[PROOFSTEP]
rw [num_den', cast_pow, cast_mk, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow, ← Int.cast_pow, ← Int.cast_mul,
  Int.cast_inj] at hxr 
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
[PROOFSTEP]
have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ N ^ n
⊢ False
[PROOFSTEP]
rw [← Int.dvd_natAbs, ← Int.coe_nat_pow, Int.coe_nat_dvd, Int.natAbs_pow, Nat.pow_dvd_pow_iff hnpos] at hdivn 
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ False
[PROOFSTEP]
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
[GOAL]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ D = 1
[PROOFSTEP]
rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ False
[PROOFSTEP]
refine' hv ⟨N, _⟩
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ ↑(mk' N 1) = ↑N
[PROOFSTEP]
rw [num_den', Int.ofNat_one, divInt_one, cast_coe_int]
[GOAL]
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
⊢ Irrational x
[PROOFSTEP]
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
[GOAL]
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
[PROOFSTEP]
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr 
[GOAL]
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
[PROOFSTEP]
simp [hxr, multiplicity.one_right (mt isUnit_iff_dvd_one.1 (mt Int.coe_nat_dvd.1 hp.1.not_dvd_one)), Nat.zero_mod] at hv 
[GOAL]
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ Irrational x
[PROOFSTEP]
refine' irrational_nrt_of_notint_nrt _ _ hxr _ hnpos
[GOAL]
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ ¬∃ y, x = ↑y
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False
[PROOFSTEP]
rw [← Int.cast_pow, Int.cast_inj] at hxr 
[GOAL]
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False
[PROOFSTEP]
subst m
[GOAL]
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ False
[PROOFSTEP]
have : y ≠ 0 := by
  rintro rfl
  rw [zero_pow hnpos] at hm 
  exact hm rfl
[GOAL]
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
[PROOFSTEP]
rw [zero_pow hnpos] at hm 
[GOAL]
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm✝ : 0 ^ n ≠ 0
hm : 0 ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
[PROOFSTEP]
exact hm rfl
[GOAL]
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
this : y ≠ 0
⊢ False
[PROOFSTEP]
erw [multiplicity.pow' (Nat.prime_iff_prime_int.1 hp.1) (finite_int_iff.2 ⟨hp.1.ne_one, this⟩), Nat.mul_mod_right] at hv 
[GOAL]
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
this : y ≠ 0
hv : 0 ≠ 0
⊢ False
[PROOFSTEP]
exact hv rfl
[GOAL]
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 ≠ 0
[PROOFSTEP]
rw [Hpv]
[GOAL]
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
p : ℕ
hp : Prime p
⊢ Part.get (multiplicity ↑p ↑p) (_ : multiplicity.Finite ↑p ↑p) % 2 = 1
[PROOFSTEP]
simp [multiplicity.multiplicity_self (mt isUnit_iff_dvd_one.1 (mt Int.coe_nat_dvd.1 hp.not_dvd_one))]
[GOAL]
⊢ Irrational (Real.sqrt 2)
[PROOFSTEP]
simpa using Nat.prime_two.irrational_sqrt
[GOAL]
q : ℚ
H1 : Rat.sqrt q * Rat.sqrt q = q
⊢ ↑(Rat.sqrt q) = Real.sqrt ↑q
[PROOFSTEP]
rw [← H1, cast_mul, sqrt_mul_self (cast_nonneg.2 <| Rat.sqrt_nonneg q), sqrt_eq, abs_of_nonneg (Rat.sqrt_nonneg q)]
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : ↑r = Real.sqrt ↑q
⊢ r * r = q
[PROOFSTEP]
rwa [eq_comm, sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul, Rat.cast_inj] at hr 
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ ↑r
[PROOFSTEP]
rw [← hr]
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ Real.sqrt ↑q
[PROOFSTEP]
exact Real.sqrt_nonneg _
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ ↑0 = Real.sqrt ↑q
[PROOFSTEP]
rw [cast_zero]
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ 0 = Real.sqrt ↑q
[PROOFSTEP]
exact (sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 <| le_of_not_le H2)).symm
[GOAL]
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑m
[PROOFSTEP]
rw [← Rat.cast_coe_int]
[GOAL]
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑↑m
[PROOFSTEP]
exact h.ne_rat _
[GOAL]
x : ℝ
h : Irrational x
⊢ x ≠ 0
[PROOFSTEP]
exact_mod_cast h.ne_nat 0
[GOAL]
x : ℝ
h : Irrational x
⊢ x ≠ 1
[PROOFSTEP]
simpa only [Nat.cast_one] using h.ne_nat 1
[GOAL]
q : ℚ
x y : ℝ
⊢ Irrational (x + y) → Irrational x ∨ Irrational y
[PROOFSTEP]
delta Irrational
[GOAL]
q : ℚ
x y : ℝ
⊢ ¬x + y ∈ Set.range Rat.cast → ¬x ∈ Set.range Rat.cast ∨ ¬y ∈ Set.range Rat.cast
[PROOFSTEP]
contrapose!
[GOAL]
q : ℚ
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x + y ∈ Set.range Rat.cast
[PROOFSTEP]
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
[GOAL]
case intro.intro.intro
q rx ry : ℚ
⊢ ↑rx + ↑ry ∈ Set.range Rat.cast
[PROOFSTEP]
exact ⟨rx + ry, cast_add rx ry⟩
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (↑(-q) + (↑q + x))
[PROOFSTEP]
rwa [cast_neg, neg_add_cancel_left]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑m + x)
⊢ Irrational x
[PROOFSTEP]
rw [← cast_coe_int] at h 
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑↑m + x)
⊢ Irrational x
[PROOFSTEP]
exact h.of_rat_add m
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)
[PROOFSTEP]
rw [← cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
[PROOFSTEP]
exact h.rat_add m
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational (-x)
x✝ : x ∈ Set.range Rat.cast
q : ℚ
hx : ↑q = x
⊢ ↑(-q) = -x
[PROOFSTEP]
rw [cast_neg, hx]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (- -x)
[PROOFSTEP]
rwa [neg_neg]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (x - ↑q)
[PROOFSTEP]
simpa only [sub_eq_add_neg, cast_neg] using h.add_rat (-q)
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (↑q - x)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.neg.rat_add q
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (x - ↑q)
⊢ Irrational (x + ↑(-q))
[PROOFSTEP]
simpa only [cast_neg, sub_eq_add_neg] using h
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (↑q - x)
⊢ Irrational (↑q + -x)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)
[PROOFSTEP]
simpa only [Rat.cast_coe_int] using h.sub_rat m
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)
[PROOFSTEP]
simpa only [Rat.cast_coe_int] using h.rat_sub m
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (x - ↑m)
⊢ Irrational (x - ↑↑m)
[PROOFSTEP]
rwa [Rat.cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑m - x)
⊢ Irrational (↑↑m - x)
[PROOFSTEP]
rwa [Rat.cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
⊢ Irrational (x * y) → Irrational x ∨ Irrational y
[PROOFSTEP]
delta Irrational
[GOAL]
q : ℚ
x y : ℝ
⊢ ¬x * y ∈ Set.range Rat.cast → ¬x ∈ Set.range Rat.cast ∨ ¬y ∈ Set.range Rat.cast
[PROOFSTEP]
contrapose!
[GOAL]
q : ℚ
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast
[PROOFSTEP]
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
[GOAL]
case intro.intro.intro
q rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast
[PROOFSTEP]
exact ⟨rx * ry, cast_mul rx ry⟩
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q * ↑q⁻¹)
[PROOFSTEP]
rwa [mul_assoc, ← cast_mul, mul_inv_cancel hq, cast_one, mul_one]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑↑m)
[PROOFSTEP]
rwa [cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑↑m * x)
[PROOFSTEP]
rwa [cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)
[PROOFSTEP]
rw [← cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
[PROOFSTEP]
refine' h.mul_rat _
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rwa [Int.cast_ne_zero]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational x⁻¹⁻¹
[PROOFSTEP]
rwa [inv_inv]
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x / ↑q)
[PROOFSTEP]
rw [div_eq_mul_inv, ← cast_inv]
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q⁻¹)
[PROOFSTEP]
exact h.mul_rat (inv_ne_zero hq)
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑m)
[PROOFSTEP]
rw [← cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)
[PROOFSTEP]
refine' h.div_rat _
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rwa [Int.cast_ne_zero]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rwa [Int.coe_nat_ne_zero]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (1 / x)
⊢ Irrational (↑1 / x)
[PROOFSTEP]
rwa [cast_one]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x
[PROOFSTEP]
rw [pow_zero] at h 
[GOAL]
q : ℚ
x y : ℝ
h : Irrational 1
⊢ Irrational x
[PROOFSTEP]
exact (h ⟨1, cast_one⟩).elim
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x
[PROOFSTEP]
rw [pow_succ] at h 
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x * x ^ n)
⊢ Irrational x
[PROOFSTEP]
exact h.mul_cases.elim id (of_pow n)
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x
[PROOFSTEP]
rw [zpow_ofNat] at h 
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
[PROOFSTEP]
exact h.of_pow _
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x
[PROOFSTEP]
rw [zpow_negSucc] at h 
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x
[PROOFSTEP]
exact h.of_inv.of_pow _
[GOAL]
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
⊢ 1 < natDegree p
[PROOFSTEP]
by_contra rid
[GOAL]
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
rid : ¬1 < natDegree p
⊢ False
[PROOFSTEP]
rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
rid : ¬1 < natDegree (↑C a * X + ↑C b)
⊢ False
[PROOFSTEP]
clear rid
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ False
[PROOFSTEP]
have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
[GOAL]
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ ↑a * x = -↑b
[PROOFSTEP]
simpa [eq_neg_iff_add_eq_zero] using x_is_root
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
⊢ False
[PROOFSTEP]
rcases em (a = 0) with (rfl | ha)
[GOAL]
case intro.intro.inl
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ False
[PROOFSTEP]
obtain rfl : b = 0 := by simpa
[GOAL]
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ b = 0
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.inl
x : ℝ
hx : Irrational x
p_nonzero : ↑C 0 * X + ↑C 0 ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C 0) = 0
this : ↑0 * x = -↑0
⊢ False
[PROOFSTEP]
simp at p_nonzero 
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False
[PROOFSTEP]
rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this 
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
refine' hx ⟨-b / a, _⟩
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ ↑(-↑b / ↑a) = x
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
assumption_mod_cast
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
assumption_mod_cast
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [mul_comm, irrational_rat_mul_iff]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_int, irrational_rat_mul_iff, Int.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_int, irrational_mul_rat_iff, Int.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_nat, irrational_rat_mul_iff, Nat.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_nat, irrational_mul_rat_iff, Nat.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [div_eq_mul_inv, ← cast_inv, irrational_mul_rat_iff, Ne.def, inv_eq_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_int, irrational_div_rat_iff, Int.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_nat, irrational_div_rat_iff, Nat.cast_ne_zero]
