---

Step * of Lemma divides_of_absvals

∀a,b:ℤ.  (|a| | |b| ⇐⇒ a | b)
BY
{ ((UnivCD THENA Auto) THEN (RWO "absval_unfold" 0 THENA Auto) THEN Repeat (AutoSplit)) }

1
1. a : ℤ
2. ¬-1 < a
3. b : ℤ
4. ¬-1 < b
⊢ (-a) | (-b) ⇐⇒ a | b

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (|a|  |  |b|  \mLeftarrow{}{}\mRightarrow{}  a  |  b)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  Repeat  (AutoSplit))

---

Home Index