a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
x : ℚ
ha : a /. b = x
⊢ Rat.Nonneg x ↔ 0 ≤ a
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
⊢ Rat.Nonneg (a /. b) ↔ 0 ≤ a
generalize ha : a /. b = x
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = mk' n₁ d₁
⊢ Rat.Nonneg (mk' n₁ d₁) ↔ 0 ≤ a
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
x : ℚ
ha : a /. b = x
⊢ Rat.Nonneg x ↔ 0 ≤ a
cases' x with n₁ d₁ h₁ c₁
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ Rat.Nonneg (mk' n₁ d₁) ↔ 0 ≤ a
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = mk' n₁ d₁
⊢ Rat.Nonneg (mk' n₁ d₁) ↔ 0 ≤ a
rw [num_den'] at ha
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ 0 ≤ n₁ ↔ 0 ≤ a
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ Rat.Nonneg (mk' n₁ d₁) ↔ 0 ≤ a
simp [Rat.Nonneg]
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
⊢ 0 ≤ n₁ ↔ 0 ≤ a
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ 0 ≤ n₁ ↔ 0 ≤ a
have d0 := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h₁)
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
⊢ 0 ≤ n₁ ↔ 0 ≤ a
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
⊢ 0 ≤ n₁ ↔ 0 ≤ a
have := (divInt_eq_iff (ne_of_gt h) (ne_of_gt d0)).1 ha
case mk'.mp
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ a

case mk'.mpr
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ n₁
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
⊢ 0 ≤ n₁ ↔ 0 ≤ a
constructor <;> intro h₂
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ a * ↑d₁
case mk'.mp
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ a
apply nonneg_of_mul_nonneg_left _ d0
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ n₁ * b
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ a * ↑d₁
rw [this]
no goals
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ n₁ * b
exact mul_nonneg h₂ (le_of_lt h)
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ n₁ * b
case mk'.mpr
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ n₁
apply nonneg_of_mul_nonneg_left _ h
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ a * ↑d₁
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ n₁ * b
rw [← this]
no goals
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ a * ↑d₁
exact mul_nonneg h₂ (Int.ofNat_zero_le _)