---

Step * of Lemma q-triangle-inequality

∀[r,s:ℚ].  (|r + s| ≤ (|r| + |s|))
BY
{ (Auto
   THEN ((Unfold `qabs` 0 THEN Auto) THEN (CallByValueReduce 0 THENA Auto))
   THEN RepeatFor 3 ((SplitOnConclITE THEN Auto))
   THEN All (RWO "assert-qpositive")⋅
   THEN Auto
   THEN QNorm 0
   THEN Auto
   THEN Try ((RelRST THEN Auto))
   THEN SupposeNot⋅) }

1
1. r : ℚ
2. s : ℚ
3. 0 < r + s
4. 0 < r
5. ¬0 < s
6. ¬((r + s) ≤ (r + -(s)))
⊢ (r + s) ≤ (r + -(s))

2
1. r : ℚ
2. s : ℚ
3. 0 < r + s
4. ¬0 < r
5. 0 < s
6. ¬((r + s) ≤ (-(r) + s))
⊢ (r + s) ≤ (-(r) + s)

3
1. r : ℚ
2. s : ℚ
3. 0 < r + s
4. ¬0 < r
5. ¬0 < s
6. ¬((r + s) ≤ (-(r) + -(s)))
⊢ (r + s) ≤ (-(r) + -(s))

4
1. r : ℚ
2. s : ℚ
3. ¬0 < r + s
4. 0 < r
5. 0 < s
6. ¬((-(r) + -(s)) ≤ (r + s))
⊢ (-(r) + -(s)) ≤ (r + s)

5
1. r : ℚ
2. s : ℚ
3. ¬0 < r + s
4. 0 < r
5. ¬0 < s
6. ¬((-(r) + -(s)) ≤ (r + -(s)))
⊢ (-(r) + -(s)) ≤ (r + -(s))

6
1. r : ℚ
2. s : ℚ
3. ¬0 < r + s
4. ¬0 < r
5. 0 < s
6. ¬((-(r) + -(s)) ≤ (-(r) + s))
⊢ (-(r) + -(s)) ≤ (-(r) + s)

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].    (|r  +  s|  \mleq{}  (|r|  +  |s|))


By

---

Latex:
(Auto
  THEN  ((Unfold  `qabs`  0  THEN  Auto)  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  RepeatFor  3  ((SplitOnConclITE  THEN  Auto))
  THEN  All  (RWO  "assert-qpositive")\mcdot{}
  THEN  Auto
  THEN  QNorm  0
  THEN  Auto
  THEN  Try  ((RelRST  THEN  Auto))
  THEN  SupposeNot\mcdot{})

---

Home Index