---

Step * 4 2 1 1 of Lemma rational_set_blt


1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. ¬0 < a3 * a6
6. ℤ ⊆r Base
⊢ (((a2 * a6) + ((-1) * a3 * a5) < 0 ∧ a3 * a6 < 0) ∨ ((a3 * a5) = (a2 * a6) ∈ ℤ))
  ∧ (¬((((-1) * a2 * a6) + (a3 * a5) < 0 ∧ a3 * a6 < 0) ∨ ((a2 * a6) = (a3 * a5) ∈ ℤ)))
⇐⇒ a2 * a6 < a3 * a5
BY
{ (BoolCase ⌜a3 * a6 <z 0⌝⋅
   THEN Auto
   THEN (Assert ⌜(a3 * a6) = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN (FLemma `int_entire` [-1] THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  a5  :  \mBbbZ{}
2.  a6  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a2  :  \mBbbZ{}
4.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  \mneg{}0  <  a3  *  a6
6.  \mBbbZ{}  \msubseteq{}r  Base
\mvdash{}  (((a2  *  a6)  +  ((-1)  *  a3  *  a5)  <  0  \mwedge{}  a3  *  a6  <  0)  \mvee{}  ((a3  *  a5)  =  (a2  *  a6)))
    \mwedge{}  (\mneg{}((((-1)  *  a2  *  a6)  +  (a3  *  a5)  <  0  \mwedge{}  a3  *  a6  <  0)  \mvee{}  ((a2  *  a6)  =  (a3  *  a5))))
\mLeftarrow{}{}\mRightarrow{}  a2  *  a6  <  a3  *  a5


By

---

Latex:
(BoolCase  \mkleeneopen{}a3  *  a6  <z  0\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}(a3  *  a6)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (FLemma  `int\_entire`  [-1]  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index