---

Step * 4 1 of Lemma rational_set_blt


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index