---

Step * of Lemma ip-between-inner-trans

No Annotations
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  (a_b_d ⇒ b_c_d ⇒ a_b_c)
BY
{ ((Auto THEN (StableCases ⌜c # d⌝⋅ THENA Auto) THEN Try ((Fold `ss-eq` (-1) THEN RWO "-1" 0 THEN Auto)))
   THEN ((StableCases ⌜a # b⌝⋅ THENA Auto) THEN Try ((Fold `ss-eq` (-1) THEN RWO "-1" 0 THEN Auto)))
   THEN (StableCases ⌜b # c⌝⋅ THENA Auto)
   THEN Try ((Fold `ss-eq` (-1) THEN RWO "-1" 0 THEN Auto))
   THEN (StableCases ⌜b # d⌝⋅ THENA Auto)
   THEN ((Fold `ss-eq` (-1) THEN RWO "-1<" (-5) THEN Auto)
   ORELSE ((All (RWO "ip-between-iff") THENA EAuto 1) THEN ExRepD)
   )) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. d : Point(rv)
6. t1 : ℝ
7. t1 ∈ (r0, r1)
8. b ≡ t1*a + r1 - t1*d
9. t : ℝ
10. t ∈ (r0, r1)
11. c ≡ t*b + r1 - t*d
12. c # d
13. a # b
14. b # c
15. b # d
⊢ ∃t:ℝ. ((t ∈ (r0, r1)) ∧ b ≡ t*a + r1 - t*c)

2
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. d : Point(rv)
6. a_b_d
7. b_c_b
8. c # d
9. a # b
10. b # c
11. b ≡ d
⊢ a_b_c

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c,d:Point(rv)].    (a\_b\_d  {}\mRightarrow{}  b\_c\_d  {}\mRightarrow{}  a\_b\_c)


By

---

Latex:
((Auto
    THEN  (StableCases  \mkleeneopen{}c  \#  d\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  Try  ((Fold  `ss-eq`  (-1)  THEN  RWO  "-1"  0  THEN  Auto)))
  THEN  ((StableCases  \mkleeneopen{}a  \#  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Try  ((Fold  `ss-eq`  (-1)  THEN  RWO  "-1"  0  THEN  Auto)))
  THEN  (StableCases  \mkleeneopen{}b  \#  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((Fold  `ss-eq`  (-1)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (StableCases  \mkleeneopen{}b  \#  d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((Fold  `ss-eq`  (-1)  THEN  RWO  "-1<"  (-5)  THEN  Auto)
  ORELSE  ((All  (RWO  "ip-between-iff")  THENA  EAuto  1)  THEN  ExRepD)
  ))

---

Home Index