[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a * a = b * b
[PROOFSTEP]
rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ ↑(natAbs a) = ↑(natAbs b)
[PROOFSTEP]
exact Int.coe_nat_inj'.symm
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a * a < b * b
[PROOFSTEP]
rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ ↑(natAbs a) < ↑(natAbs b)
[PROOFSTEP]
exact Int.ofNat_lt.symm
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ a * a ≤ b * b
[PROOFSTEP]
rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ ↑(natAbs a) ≤ ↑(natAbs b)
[PROOFSTEP]
exact Int.ofNat_le.symm
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
⊢ b ∣ c / a
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
a b✝ : ℤ
n : ℕ
b c : ℤ
h : 0 * b ∣ c
⊢ b ∣ c / 0
[PROOFSTEP]
simp only [Int.ediv_zero, dvd_zero]
[GOAL]
case inr
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
[PROOFSTEP]
rcases h with ⟨d, rfl⟩
[GOAL]
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ b ∣ a * b * d / a
[PROOFSTEP]
refine' ⟨d, _⟩
[GOAL]
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ a * b * d / a = b * d
[PROOFSTEP]
rw [mul_assoc, Int.mul_ediv_cancel_left _ ha]
[GOAL]
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0
[PROOFSTEP]
by_cases hm : m = 0
[GOAL]
case pos
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
hm : m = 0
⊢ x = 0
[PROOFSTEP]
subst m
[GOAL]
case pos
a b : ℤ
n : ℕ
x : ℤ
h1 : 0 ∣ x
h2 : |x| < 0
⊢ x = 0
[PROOFSTEP]
exact zero_dvd_iff.mp h1
[GOAL]
case neg
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
hm : ¬m = 0
⊢ x = 0
[PROOFSTEP]
rcases h1 with ⟨d, rfl⟩
[GOAL]
case neg.intro
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : |m * d| < m
⊢ m * d = 0
[PROOFSTEP]
apply mul_eq_zero_of_right
[GOAL]
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : |m * d| < m
⊢ d = 0
[PROOFSTEP]
rw [← abs_lt_one_iff, ← mul_lt_iff_lt_one_right (abs_pos.mpr hm), ← abs_mul]
[GOAL]
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : |m * d| < m
⊢ |m * d| < |m|
[PROOFSTEP]
exact lt_of_lt_of_le h2 (le_abs_self m)
