---

Step * 4 of Lemma rational_set_blt


1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
⊢ (((0 <z (a2 * a6) + (((-1) * a5) * a3) ∧b 0 <z a3 * a6) ∨b((a2 * a6) + (((-1) * a5) * a3) <z 0 ∧b a3 * a6 <z 0))
  ∨b(a5 * a3 =z a2 * a6))
  ∧b (¬b(((0 <z (a5 * a3) + (((-1) * a2) * a6) ∧b 0 <z a6 * a3) ∨b((a5 * a3) + (((-1) * a2) * a6) <z 0 ∧b a6 * a3 <z 0))
     ∨b(a2 * a6 =z a5 * a3))) 
= if 0 <z a6 * a3 then a3 * a5 <z a6 * a2 else a6 * a2 <z a3 * a5 fi 
BY
{ ((RW IntNormC 0⋅ THENA Auto)
   THEN AutoSplit
   THEN (RWW "band_ff_simp band_tt_simp bor_ff_simp" 0 THENA Auto)
   THEN Reduce 0) }

1
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

2
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{}
\mvdash{}  (((0  <z  (a2  *  a6)  +  (((-1)  *  a5)  *  a3)  \mwedge{}\msubb{}  0  <z  a3  *  a6)
    \mvee{}\msubb{}((a2  *  a6)  +  (((-1)  *  a5)  *  a3)  <z  0  \mwedge{}\msubb{}  a3  *  a6  <z  0))
    \mvee{}\msubb{}(a5  *  a3  =\msubz{}  a2  *  a6))
    \mwedge{}\msubb{}  (\mneg{}\msubb{}(((0  <z  (a5  *  a3)  +  (((-1)  *  a2)  *  a6)  \mwedge{}\msubb{}  0  <z  a6  *  a3)
          \mvee{}\msubb{}((a5  *  a3)  +  (((-1)  *  a2)  *  a6)  <z  0  \mwedge{}\msubb{}  a6  *  a3  <z  0))
          \mvee{}\msubb{}(a2  *  a6  =\msubz{}  a5  *  a3))) 
=  if  0  <z  a6  *  a3  then  a3  *  a5  <z  a6  *  a2  else  a6  *  a2  <z  a3  *  a5  fi 


By

---

Latex:
((RW  IntNormC  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  (RWW  "band\_ff\_simp  band\_tt\_simp  bor\_ff\_simp"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index