---

Step * 1 of Lemma hyptrans_ext


1. rv : InnerProductSpace
2. e : Point
3. s : ℝ
4. t : ℝ
5. x : Point
6. y : Point
7. x + (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # y + (y ⋅ e * (cosh(t) - r1))
+ (rsqrt(r1 + y^2) * sinh(t))*e
8. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))*e
9. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s)) ≠ (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))
⊢ x # y ∨ s ≠ t
BY
{ ((Assert ¬e # e BY
          Auto)
   THEN PromoteHyp (-1) 3
   THEN ((FLemma `rneq-radd` [-1] THENA Auto) THEN D -1)
   THEN (FLemma `rneq-rmul` [-1] THENA Auto)
   THEN D -1
   THEN Try ((FLemma `rneq_irreflexivity` [-1] THEN Auto))
   THEN Try (((FLemma `rsqrt-rneq` [-1] THENA Auto) THEN (FLemma `rneq-radd` [-1] THENA Auto) THEN D -1))
   THEN Try ((FLemma `rneq_irreflexivity` [-1] THEN Auto))
   THEN Try (((OrLeft  THENA Auto) THEN (FLemma `rv-ip-rneq` [-1] THENA Auto) THEN D -1 THEN Auto))
   THEN (OrRight THENA Auto)) }

1
1. rv : InnerProductSpace
2. e : Point
3. ¬e # e
4. s : ℝ
5. t : ℝ
6. x : Point
7. y : Point
8. x + (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # y + (y ⋅ e * (cosh(t) - r1))
+ (rsqrt(r1 + y^2) * sinh(t))*e
9. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))*e
10. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s)) ≠ (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))
11. x ⋅ e * (cosh(s) - r1) ≠ y ⋅ e * (cosh(t) - r1)
12. cosh(s) - r1 ≠ cosh(t) - r1
⊢ s ≠ t

2
1. rv : InnerProductSpace
2. e : Point
3. ¬e # e
4. s : ℝ
5. t : ℝ
6. x : Point
7. y : Point
8. x + (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # y + (y ⋅ e * (cosh(t) - r1))
+ (rsqrt(r1 + y^2) * sinh(t))*e
9. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))*e
10. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s)) ≠ (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))
11. rsqrt(r1 + x^2) * sinh(s) ≠ rsqrt(r1 + y^2) * sinh(t)
12. sinh(s) ≠ sinh(t)
⊢ s ≠ t

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  Point
3.  s  :  \mBbbR{}
4.  t  :  \mBbbR{}
5.  x  :  Point
6.  y  :  Point
7.  x  +  (x  \mcdot{}  e  *  (cosh(s)  -  r1))  +  (rsqrt(r1  +  x\^{}2)  *  sinh(s))*e  \#  y  +  (y  \mcdot{}  e  *  (cosh(t)  -  r1))
+  (rsqrt(r1  +  y\^{}2)  *  sinh(t))*e
8.  (x  \mcdot{}  e  *  (cosh(s)  -  r1))  +  (rsqrt(r1  +  x\^{}2)  *  sinh(s))*e  \#  (y  \mcdot{}  e  *  (cosh(t)  -  r1))
+  (rsqrt(r1  +  y\^{}2)  *  sinh(t))*e
9.  (x  \mcdot{}  e  *  (cosh(s)  -  r1))  +  (rsqrt(r1  +  x\^{}2)  *  sinh(s))  \mneq{}  (y  \mcdot{}  e  *  (cosh(t)  -  r1))
+  (rsqrt(r1  +  y\^{}2)  *  sinh(t))
\mvdash{}  x  \#  y  \mvee{}  s  \mneq{}  t


By

---

Latex:
((Assert  \mneg{}e  \#  e  BY
                Auto)
  THEN  PromoteHyp  (-1)  3
  THEN  ((FLemma  `rneq-radd`  [-1]  THENA  Auto)  THEN  D  -1)
  THEN  (FLemma  `rneq-rmul`  [-1]  THENA  Auto)
  THEN  D  -1
  THEN  Try  ((FLemma  `rneq\_irreflexivity`  [-1]  THEN  Auto))
  THEN  Try  (((FLemma  `rsqrt-rneq`  [-1]  THENA  Auto)
                        THEN  (FLemma  `rneq-radd`  [-1]  THENA  Auto)
                        THEN  D  -1))
  THEN  Try  ((FLemma  `rneq\_irreflexivity`  [-1]  THEN  Auto))
  THEN  Try  (((OrLeft    THENA  Auto)  THEN  (FLemma  `rv-ip-rneq`  [-1]  THENA  Auto)  THEN  D  -1  THEN  Auto))
  THEN  (OrRight  THENA  Auto))

---

Home Index