---

Step * of Lemma ip-between-iff2

∀rv:InnerProductSpace. ∀a,b,c:Point.
  (a_b_c ⇐⇒ (a ≡ c ⇒ b ≡ c) ∧ (a # c ⇒ (∃t:ℝ. ((t ∈ [r0, r1]) ∧ b ≡ t*a + r1 - t*c))))
BY
{ Auto }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. a ≡ c
⊢ b ≡ c

2
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. a # c
⊢ ∃t:ℝ. ((t ∈ [r0, r1]) ∧ b ≡ t*a + r1 - t*c)

3
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. a ≡ c ⇒ b ≡ c
6. a # c ⇒ (∃t:ℝ. ((t ∈ [r0, r1]) ∧ b ≡ t*a + r1 - t*c))
⊢ a_b_c

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.
    (a\_b\_c  \mLeftarrow{}{}\mRightarrow{}  (a  \mequiv{}  c  {}\mRightarrow{}  b  \mequiv{}  c)  \mwedge{}  (a  \#  c  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  ((t  \mmember{}  [r0,  r1])  \mwedge{}  b  \mequiv{}  t*a  +  r1  -  t*c))))


By

---

Latex:
Auto

---

Home Index