Step
*
1
1
of Lemma
qbetween-qdist
.....equality.....
1. a : ℚ
2. b : ℚ
3. r : ℚ
4. s : ℚ
5. 0 ≤ (a - r)
6. 0 ≤ (s - a)
7. 0 ≤ (b - r)
8. 0 ≤ (s - b)
⊢ (s - r - a - b) = ((s - a) + (b - r)) ∈ ℚ
BY
{ xxx(xxx(RW (AddrC [2] (UnfoldTopC `qsub`)) 0)xxx
THEN (RWO "qminus-qsub" 0 THENA Auto)
THEN RepUR ``qsub`` 0
THEN xxx(RWW "qadd_assoc" 0 THENA Auto)xxx
THEN EqCD
THEN Auto
THEN xxx((RW (AddrC [2] (LemmaC `qadd_com`)) 0) THENA Auto)xxx
THEN (RWW "qadd_assoc<" 0 THENA Auto)
THEN EqCD
THEN Auto
THEN BLemma `qadd_com`
THEN Auto)xxx }
Latex:
Latex:
.....equality.....
1. a : \mBbbQ{}
2. b : \mBbbQ{}
3. r : \mBbbQ{}
4. s : \mBbbQ{}
5. 0 \mleq{} (a - r)
6. 0 \mleq{} (s - a)
7. 0 \mleq{} (b - r)
8. 0 \mleq{} (s - b)
\mvdash{} (s - r - a - b) = ((s - a) + (b - r))
By
Latex:
xxx(xxx(RW (AddrC [2] (UnfoldTopC `qsub`)) 0)xxx
THEN (RWO "qminus-qsub" 0 THENA Auto)
THEN RepUR ``qsub`` 0
THEN xxx(RWW "qadd\_assoc" 0 THENA Auto)xxx
THEN EqCD
THEN Auto
THEN xxx((RW (AddrC [2] (LemmaC `qadd\_com`)) 0) THENA Auto)xxx
THEN (RWW "qadd\_assoc<" 0 THENA Auto)
THEN EqCD
THEN Auto
THEN BLemma `qadd\_com`
THEN Auto)xxx
Home
Index