---

Step * 1 of Lemma qless-minus


1. a : ℚ
2. b : ℚ
⊢ uiff(↑((qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(a - b) ∨bqeq(b;a))));↑((qpositive(-(a) - -(b)) ∨bqeq(-(b);-(a)))
∧b (¬b(qpositive(-(b) - -(a)) ∨bqeq(-(a);-(b))))))
BY
{ TACTIC:((RW assert_pushdownC 0 THENA Auto) THEN QNorm 0 THEN Auto THEN QNorm (-1) THEN QNorm 0 THEN Auto) }

1
1. a : ℚ
2. b : ℚ
3. [%] : (0 < -(a) + b ∨ (a = b ∈ ℚ)) ∧ (¬(0 < a + -(b) ∨ (b = a ∈ ℚ)))
⊢ 0 < -(a) + b ∨ (-(b) = -(a) ∈ ℚ)

2
1. a : ℚ
2. b : ℚ
3. 0 < -(a) + b ∨ (a = b ∈ ℚ)
4. ¬(0 < a + -(b) ∨ (b = a ∈ ℚ))
⊢ ¬(0 < a + -(b) ∨ (-(a) = -(b) ∈ ℚ))

3
1. a : ℚ
2. b : ℚ
3. [%] : (0 < -(a) + b ∨ (-(b) = -(a) ∈ ℚ)) ∧ (¬(0 < a + -(b) ∨ (-(a) = -(b) ∈ ℚ)))
⊢ 0 < -(a) + b ∨ (a = b ∈ ℚ)

4
1. a : ℚ
2. b : ℚ
3. 0 < -(a) + b ∨ (-(b) = -(a) ∈ ℚ)
4. ¬(0 < a + -(b) ∨ (-(a) = -(b) ∈ ℚ))
⊢ ¬(0 < a + -(b) ∨ (b = a ∈ ℚ))

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
\mvdash{}  uiff(\muparrow{}((qpositive(b  -  a)  \mvee{}\msubb{}qeq(a;b))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(qpositive(a  -  b)  \mvee{}\msubb{}qeq(b;a))));\muparrow{}((qpositive(-(a) 
-  -(b))
\mvee{}\msubb{}qeq(-(b);-(a)))
\mwedge{}\msubb{}  (\mneg{}\msubb{}(qpositive(-(b)  -  -(a))  \mvee{}\msubb{}qeq(-(a);-(b))))))


By

---

Latex:
TACTIC:((RW  assert\_pushdownC  0  THENA  Auto)
                THEN  QNorm  0
                THEN  Auto
                THEN  QNorm  (-1)
                THEN  QNorm  0
                THEN  Auto)

---

Home Index