Step * of Lemma req-implies-req

[a,b,c,d:ℝ].  (a b) supposing ((c d) and ((d c) (b a)))
BY
(Auto
   THEN (RW (nRAddC ⌜-(a)⌝0⋅ THENA Auto)
   THEN (RW (nRAddC ⌜-(c)⌝(-1)⋅ THENA Auto)
   THEN ((Assert (-(c) c) r0 BY Auto) THEN (RWO "-1" (-2) THENA Auto))
   THEN (Assert (-(a) a) r0 BY
               Auto)
   THEN (RWO "-1" THENA Auto)) }

1
1. : ℝ
2. : ℝ
3. : ℝ
4. : ℝ
5. (d c) (b a)
6. r0 (-(c) d)
7. (-(c) c) r0
8. (-(a) a) r0
⊢ r0 (-(a) b)


Latex:


Latex:
\mforall{}[a,b,c,d:\mBbbR{}].    (a  =  b)  supposing  ((c  =  d)  and  ((d  -  c)  =  (b  -  a)))


By


Latex:
(Auto
  THEN  (RW  (nRAddC  \mkleeneopen{}-(a)\mkleeneclose{})  0\mcdot{}  THENA  Auto)
  THEN  (RW  (nRAddC  \mkleeneopen{}-(c)\mkleeneclose{})  (-1)\mcdot{}  THENA  Auto)
  THEN  ((Assert  (-(c)  +  c)  =  r0  BY  Auto)  THEN  (RWO  "-1"  (-2)  THENA  Auto))
  THEN  (Assert  (-(a)  +  a)  =  r0  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))




Home Index