Step
*
of Lemma
eu-add-length-cancel-left
∀[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ]. x = y ∈ {p:Point| O_X_p} supposing z + x = z + y ∈ {p:Point| O_X_p}
BY
{ (Auto
THEN DSetVars
THEN MoveToConcl (-1)
THEN RepUR ``eu-add-length`` 0
THEN (Assert ¬(O = X ∈ Point) BY
Auto)
THEN (Assert ¬(O = z ∈ Point) BY
(NotEqualFromEuBetween⋅ THEN Auto))
THEN GeneralizeEuExtends [`a';`b']) }
1
1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. y : Point
5. O_X_y
6. z : Point
7. O_X_z
8. ¬(O = X ∈ Point)
9. ¬(O = z ∈ Point)
10. a : Point@i
11. O_z_a ∧ za=Xx@i
12. b : Point@i
13. O_z_b ∧ zb=Xy@i
⊢ (a = b ∈ {p:Point| O_X_p} )
⇒ (x = y ∈ {p:Point| O_X_p} )
Latex:
Latex:
\mforall{}[e:EuclideanPlane]. \mforall{}[x,y,z:\{p:Point| O\_X\_p\} ]. x = y supposing z + x = z + y
By
Latex:
(Auto
THEN DSetVars
THEN MoveToConcl (-1)
THEN RepUR ``eu-add-length`` 0
THEN (Assert \mneg{}(O = X) BY
Auto)
THEN (Assert \mneg{}(O = z) BY
(NotEqualFromEuBetween\mcdot{} THEN Auto))
THEN GeneralizeEuExtends [`a';`b'])
Home
Index