---

Step * 4 2 1 of Lemma rational_set_blt


1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. ¬0 < a3 * a6
⊢ ↑((((a2 * a6) + ((-1) * a3 * a5) <z 0 ∧b a3 * a6 <z 0) ∨b(a3 * a5 =z a2 * a6))
  ∧b (¬b((((-1) * a2 * a6) + (a3 * a5) <z 0 ∧b a3 * a6 <z 0) ∨b(a2 * a6 =z a3 * a5))))
⇐⇒ ↑a2 * a6 <z a3 * a5
BY
{ ((Assert ℤ ⊆r Base BY
          Auto)
   THEN (RW assert_pushdownC 0 THENA Repeat (First [Hypothesis;MemCD; MemTypeCD;  IsTypeD]))
   ) }

1
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

---

Latex:

---

Latex:

1.  a5  :  \mBbbZ{}
2.  a6  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a2  :  \mBbbZ{}
4.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  \mneg{}0  <  a3  *  a6
\mvdash{}  \muparrow{}((((a2  *  a6)  +  ((-1)  *  a3  *  a5)  <z  0  \mwedge{}\msubb{}  a3  *  a6  <z  0)  \mvee{}\msubb{}(a3  *  a5  =\msubz{}  a2  *  a6))
    \mwedge{}\msubb{}  (\mneg{}\msubb{}((((-1)  *  a2  *  a6)  +  (a3  *  a5)  <z  0  \mwedge{}\msubb{}  a3  *  a6  <z  0)  \mvee{}\msubb{}(a2  *  a6  =\msubz{}  a3  *  a5))))
\mLeftarrow{}{}\mRightarrow{}  \muparrow{}a2  *  a6  <z  a3  *  a5


By

---

Latex:
((Assert  \mBbbZ{}  \msubseteq{}r  Base  BY
                Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Repeat  (First  [Hypothesis;MemCD;  MemTypeCD;    IsTypeD]))
  )

---

Home Index