---

Step * 5 2 of Lemma qpositive_wf


1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. (0 < a5 ∧ 0 < a6) ∨ (a5 < 0 ∧ a6 < 0)
7. ¬(a2 = 0 ∈ ℤ)
⊢ (0 < a2 ∧ 0 < a3) ∨ (a2 < 0 ∧ a3 < 0)
BY
{ (Decide a3 < 0
   THEN Auto
   THEN Decide a2 < 0
   THEN Auto
   THEN Try ((xxxOrRightxxx THEN Complete (Auto)))
   THEN Try ((xxxOrLeftxxx THEN Complete (Auto')))
   THEN xxxxxx(xxx(Assert 0 < a5 * a3 ⇐⇒ 0 < a2 * a6 BY
                         (HypSubst' 5 0 THEN Auto))xxx
               THEN xxx(RWO "pos_mul_arg_bounds" (-1))xxx
               THEN Auto
               THEN SplitOrHyps
               THEN ExRepD
               THEN Try (((D -1 THENA Auto) THEN xxx(D -1 THEN Complete (Auto))xxx))
               THEN Try (((D -1 THENA Auto) THEN xxx(D -2 THEN Complete (Auto))xxx)))xxxxxx)⋅ }

---

Latex:

---

Latex:

1.  a5  :  \mBbbZ{}
2.  a6  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a2  :  \mBbbZ{}
4.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  (a5  *  a3)  =  (a2  *  a6)
6.  (0  <  a5  \mwedge{}  0  <  a6)  \mvee{}  (a5  <  0  \mwedge{}  a6  <  0)
7.  \mneg{}(a2  =  0)
\mvdash{}  (0  <  a2  \mwedge{}  0  <  a3)  \mvee{}  (a2  <  0  \mwedge{}  a3  <  0)


By

---

Latex:
(Decide  a3  <  0
  THEN  Auto
  THEN  Decide  a2  <  0
  THEN  Auto
  THEN  Try  ((xxxOrRightxxx  THEN  Complete  (Auto)))
  THEN  Try  ((xxxOrLeftxxx  THEN  Complete  (Auto')))
  THEN  xxxxxx(xxx(Assert  0  <  a5  *  a3  \mLeftarrow{}{}\mRightarrow{}  0  <  a2  *  a6  BY
                                              (HypSubst'  5  0  THEN  Auto))xxx
                          THEN  xxx(RWO  "pos\_mul\_arg\_bounds"  (-1))xxx
                          THEN  Auto
                          THEN  SplitOrHyps
                          THEN  ExRepD
                          THEN  Try  (((D  -1  THENA  Auto)  THEN  xxx(D  -1  THEN  Complete  (Auto))xxx))
                          THEN  Try  (((D  -1  THENA  Auto)  THEN  xxx(D  -2  THEN  Complete  (Auto))xxx)))xxxxxx)\mcdot{}

---

Home Index