---

Step * 2 of Lemma rational_set_blt


1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
⊢ (((0 <z (a1 * a4) + ((-1) * a3) ∧b 0 <z a4) ∨b((a1 * a4) + ((-1) * a3) <z 0 ∧b a4 <z 0)) ∨b(a3 =z a1 * a4))
  ∧b (¬b(((0 <z a3 + (((-1) * a1) * a4) ∧b 0 <z a4) ∨b(a3 + (((-1) * a1) * a4) <z 0 ∧b a4 <z 0)) ∨b(a1 * a4 =z a3))) 
= if 0 <z a4 then a3 <z a4 * a1 else a4 * a1 <z a3 fi 
BY
{ (BoolCase ⌜0 <z a4⌝⋅ THENA Auto) }

1
1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
4. 0 < a4
⊢ (((0 <z (a1 * a4) + ((-1) * a3) ∧b tt) ∨b((a1 * a4) + ((-1) * a3) <z 0 ∧b ff)) ∨b(a3 =z a1 * a4))
  ∧b (¬b(((0 <z a3 + (((-1) * a1) * a4) ∧b tt) ∨b(a3 + (((-1) * a1) * a4) <z 0 ∧b ff)) ∨b(a1 * a4 =z a3))) 
= a3 <z a4 * a1

2
1. a3 : ℤ
2. a4 : ℤ-o
3. ¬0 < a4
4. a1 : ℤ
⊢ (((0 <z (a1 * a4) + ((-1) * a3) ∧b ff) ∨b((a1 * a4) + ((-1) * a3) <z 0 ∧b tt)) ∨b(a3 =z a1 * a4))
  ∧b (¬b(((0 <z a3 + (((-1) * a1) * a4) ∧b ff) ∨b(a3 + (((-1) * a1) * a4) <z 0 ∧b tt)) ∨b(a1 * a4 =z a3))) 
= a4 * a1 <z a3

---

Latex:

---

Latex:

1.  a3  :  \mBbbZ{}
2.  a4  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a1  :  \mBbbZ{}
\mvdash{}  (((0  <z  (a1  *  a4)  +  ((-1)  *  a3)  \mwedge{}\msubb{}  0  <z  a4)  \mvee{}\msubb{}((a1  *  a4)  +  ((-1)  *  a3)  <z  0  \mwedge{}\msubb{}  a4  <z  0))
    \mvee{}\msubb{}(a3  =\msubz{}  a1  *  a4))
    \mwedge{}\msubb{}  (\mneg{}\msubb{}(((0  <z  a3  +  (((-1)  *  a1)  *  a4)  \mwedge{}\msubb{}  0  <z  a4)  \mvee{}\msubb{}(a3  +  (((-1)  *  a1)  *  a4)  <z  0  \mwedge{}\msubb{}  a4  <z  0))
          \mvee{}\msubb{}(a1  *  a4  =\msubz{}  a3))) 
=  if  0  <z  a4  then  a3  <z  a4  *  a1  else  a4  *  a1  <z  a3  fi 


By

---

Latex:
(BoolCase  \mkleeneopen{}0  <z  a4\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index