---

Step * 4 2 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
{ (BLemma `iff_imp_equal_bool` THENA Repeat (MemCD)) }

1
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

---

Latex:

---

Latex:

1.  a5  :  \mBbbZ{}
2.  a6  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a2  :  \mBbbZ{}
4.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  \mneg{}0  <  a3  *  a6
\mvdash{}  (((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))) 
=  a2  *  a6  <z  a3  *  a5


By

---

Latex:
(BLemma  `iff\_imp\_equal\_bool`  THENA  Repeat  (MemCD))

---

Home Index