---

Step * 3 of Lemma rational_set_blt


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

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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index