---

Step * of Lemma rless_functionality

∀x1,x2,y1,y2:ℝ.  (x1 < y1 ⇐⇒ x2 < y2) supposing ((y1 = y2) and (x1 = x2))
BY
{ (Auto
   THEN All
   (Unfold `req`)⋅
   THEN (AllHyps (RWO "rless-iff-large-diff") THENA Auto)
   THEN (InstHyp [⌜13⌝] (-1)⋅ THENA Auto)
   THEN (BLemma `rless-iff4` THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (D -1 THENA Auto)
   THEN (InstHyp [⌜m⌝] 5⋅ THENA Auto)
   THEN (InstHyp [⌜m⌝] 6⋅ THENA Auto)
   THEN RepeatFor 2 (((RWO "absval_ifthenelse" (-2) THENA Auto) THEN (SplitOnHypITE -2  THENA Auto)))
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}x1,x2,y1,y2:\mBbbR{}.    (x1  <  y1  \mLeftarrow{}{}\mRightarrow{}  x2  <  y2)  supposing  ((y1  =  y2)  and  (x1  =  x2))


By

---

Latex:
(Auto
  THEN  All
  (Unfold  `req`)\mcdot{}
  THEN  (AllHyps  (RWO  "rless-iff-large-diff")  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}13\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (BLemma  `rless-iff4`  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  -1  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (((RWO  "absval\_ifthenelse"  (-2)  THENA  Auto)  THEN  (SplitOnHypITE  -2    THENA  Auto)))
  THEN  Auto')

---

Home Index