---

Step * of Lemma ip-inner-Pasch1

∀rv:InnerProductSpace. ∀a,b,c,p,q:Point.
  (a # p
  ⇒ b # c
  ⇒ a_p_c
  ⇒ b_q_c
  ⇒ (∃x:Point
       (a_x_q
       ∧ b_x_p
       ∧ (a # q ⇒ x # a)
       ∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
       ∧ ((b # p ∧ b # q) ⇒ x # b)
       ∧ ((b # p ∧ q # c) ⇒ x # p))))
BY
{ (Auto
   THEN (FLemma `ip-between-sep` [-2] THENA Auto)
   THEN ∀h:hyp. ((RWO "ip-between-iff2" h THENA Auto) THEN D h THEN (D h+1 THENA Auto)) 
   THEN RepeatFor 2 (Thin (-4))
   THEN ExRepD
   THEN RenameVar `s' (-3)
   THEN RenameVar `t' (-6)
   THEN All Reduce) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. a # p
8. b # c
9. a # c
10. t : ℝ
11. (r0 ≤ t) ∧ (t ≤ r1)
12. q ≡ t*b + r1 - t*c
13. s : ℝ
14. (r0 ≤ s) ∧ (s ≤ r1)
15. p ≡ s*a + r1 - s*c
⊢ ∃x:Point
   (a_x_q
   ∧ b_x_p
   ∧ (a # q ⇒ x # a)
   ∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
   ∧ ((b # p ∧ b # q) ⇒ x # b)
   ∧ ((b # p ∧ q # c) ⇒ x # p))

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c,p,q:Point.
    (a  \#  p
    {}\mRightarrow{}  b  \#  c
    {}\mRightarrow{}  a\_p\_c
    {}\mRightarrow{}  b\_q\_c
    {}\mRightarrow{}  (\mexists{}x:Point
              (a\_x\_q
              \mwedge{}  b\_x\_p
              \mwedge{}  (a  \#  q  {}\mRightarrow{}  x  \#  a)
              \mwedge{}  ((a  \#  q  \mwedge{}  p  \#  c  \mwedge{}  b  \#  q)  {}\mRightarrow{}  x  \#  q)
              \mwedge{}  ((b  \#  p  \mwedge{}  b  \#  q)  {}\mRightarrow{}  x  \#  b)
              \mwedge{}  ((b  \#  p  \mwedge{}  q  \#  c)  {}\mRightarrow{}  x  \#  p))))


By

---

Latex:
(Auto
  THEN  (FLemma  `ip-between-sep`  [-2]  THENA  Auto)
  THEN  \mforall{}h:hyp.  ((RWO  "ip-between-iff2"  h  THENA  Auto)  THEN  D  h  THEN  (D  h+1  THENA  Auto)) 
  THEN  RepeatFor  2  (Thin  (-4))
  THEN  ExRepD
  THEN  RenameVar  `s'  (-3)
  THEN  RenameVar  `t'  (-6)
  THEN  All  Reduce)

---

Home Index