---

Step * 6 2 of Lemma qpositive_wf


1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. (0 < a2 ∧ 0 < a3) ∨ (a2 < 0 ∧ a3 < 0)
7. ¬(a5 = 0 ∈ ℤ)
⊢ (0 < a5 ∧ 0 < a6) ∨ (a5 < 0 ∧ a6 < 0)
BY
{ (((Decide a6 < 0 THENA Auto) THENL [OrRight; OrLeft])
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN SupposeNot
   THEN (Assert 0 < a5 * a3 ⇐⇒ 0 < a2 * a6 BY
               (HypSubst' 5 0 THEN Auto))
   THEN ((RWO "pos_mul_arg_bounds" (-1)) THENA Auto)) }

1
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. 0 < a2
7. 0 < a3
8. ¬(a5 = 0 ∈ ℤ)
9. a6 < 0
10. ¬a5 < 0
11. ((a5 > 0) ∧ (a3 > 0)) ∨ (a5 < 0 ∧ a3 < 0) ⇐⇒ ((a2 > 0) ∧ (a6 > 0)) ∨ (a2 < 0 ∧ a6 < 0)
⊢ a5 < 0

2
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. a2 < 0
7. a3 < 0
8. ¬(a5 = 0 ∈ ℤ)
9. a6 < 0
10. ¬a5 < 0
11. ((a5 > 0) ∧ (a3 > 0)) ∨ (a5 < 0 ∧ a3 < 0) ⇐⇒ ((a2 > 0) ∧ (a6 > 0)) ∨ (a2 < 0 ∧ a6 < 0)
⊢ a5 < 0

3
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. 0 < a2
7. 0 < a3
8. ¬(a5 = 0 ∈ ℤ)
9. ¬a6 < 0
10. ¬0 < a5
11. ((a5 > 0) ∧ (a3 > 0)) ∨ (a5 < 0 ∧ a3 < 0) ⇐⇒ ((a2 > 0) ∧ (a6 > 0)) ∨ (a2 < 0 ∧ a6 < 0)
⊢ 0 < a5

4
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. a2 < 0
7. a3 < 0
8. ¬(a5 = 0 ∈ ℤ)
9. ¬a6 < 0
10. ¬0 < a5
11. ((a5 > 0) ∧ (a3 > 0)) ∨ (a5 < 0 ∧ a3 < 0) ⇐⇒ ((a2 > 0) ∧ (a6 > 0)) ∨ (a2 < 0 ∧ a6 < 0)
⊢ 0 < a5

---

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  <  a2  \mwedge{}  0  <  a3)  \mvee{}  (a2  <  0  \mwedge{}  a3  <  0)
7.  \mneg{}(a5  =  0)
\mvdash{}  (0  <  a5  \mwedge{}  0  <  a6)  \mvee{}  (a5  <  0  \mwedge{}  a6  <  0)


By

---

Latex:
(((Decide  a6  <  0  THENA  Auto)  THENL  [OrRight;  OrLeft])
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  SupposeNot
  THEN  (Assert  0  <  a5  *  a3  \mLeftarrow{}{}\mRightarrow{}  0  <  a2  *  a6  BY
                          (HypSubst'  5  0  THEN  Auto))
  THEN  ((RWO  "pos\_mul\_arg\_bounds"  (-1))  THENA  Auto))

---

Home Index