---

Step * of Lemma geo-lt-add1-iff2

∀e:BasicGeometry. ∀a1,a2,b1,b2,c1,c2:Point.  (|a1a2| < |b1b2| ⇐⇒ |a1a2| + |c1c2| < |b1b2| + |c1c2|)
BY
{ Auto }

1
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2|
⊢ |a1a2| + |c1c2| < |b1b2| + |c1c2|

2
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| + |c1c2| < |b1b2| + |c1c2|
⊢ |a1a2| < |b1b2|

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a1,a2,b1,b2,c1,c2:Point.    (|a1a2|  <  |b1b2|  \mLeftarrow{}{}\mRightarrow{}  |a1a2|  +  |c1c2|  <  |b1b2|  +  |c1c2|)


By

---

Latex:
Auto

---

Home Index