[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ |a * b| = |a| * |b|
[PROOFSTEP]
rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
cases' le_total a 0 with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : a ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
cases' le_total b 0 with hb hb
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : 0 ≤ a
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
cases' le_total b 0 with hb hb
[GOAL]
case inl.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
[PROOFSTEP]
simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul, mul_neg, neg_neg, *]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ |a * a| = a * a
[PROOFSTEP]
rw [abs_mul, abs_mul_abs_self]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = a ↔ 0 ≤ a
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = -a ↔ a ≤ 0
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
[PROOFSTEP]
by_cases h : 0 ≤ a
[GOAL]
case pos
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a
[PROOFSTEP]
exact ⟨abs_eq_self.mpr h, h⟩
[GOAL]
case neg
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ |a| = -a ∧ a < 0
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a < 0
⊢ |a| = -a ∧ a < 0
[PROOFSTEP]
exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ max a 0 + max (-a) 0 = |a|
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ |a| = max a 0 + max (-a) 0
[PROOFSTEP]
rcases le_total 0 a with (ha | ha)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
ha : 0 ≤ a
⊢ |a| = max a 0 + max (-a) 0
[PROOFSTEP]
simp [ha]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
ha : a ≤ 0
⊢ |a| = max a 0 + max (-a) 0
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = |b| ↔ a * a = b * b
[PROOFSTEP]
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|
[PROOFSTEP]
exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| < |b| ↔ a * a < b * b
[PROOFSTEP]
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|
[PROOFSTEP]
exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b
[PROOFSTEP]
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
[PROOFSTEP]
exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ |a| ≤ 1 ↔ a * a ≤ 1
[PROOFSTEP]
simpa only [abs_one, one_mul] using @abs_le_iff_mul_self_le α _ a 1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
[PROOFSTEP]
rw [abs_mul_abs_self]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b
[PROOFSTEP]
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg, neg_add_rev, neg_neg,
  add_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
⊢ |a| ∣ b ↔ a ∣ b
[PROOFSTEP]
cases' abs_choice a with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |a| = a
⊢ |a| ∣ b ↔ a ∣ b
[PROOFSTEP]
simp only [h, neg_dvd]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |a| = -a
⊢ |a| ∣ b ↔ a ∣ b
[PROOFSTEP]
simp only [h, neg_dvd]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
⊢ a ∣ |b| ↔ a ∣ b
[PROOFSTEP]
cases' abs_choice b with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |b| = b
⊢ a ∣ |b| ↔ a ∣ b
[PROOFSTEP]
simp only [h, dvd_neg]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a✝ b✝ a b : α
h : |b| = -b
⊢ a ∣ |b| ↔ a ∣ b
[PROOFSTEP]
simp only [h, dvd_neg]
