---

Step * 6 2 4 of Lemma qpositive_wf


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
BY
{ (D -1 THEN (D -1 THENA Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1  THEN  (D  -1  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index