---

Step * 2 of Lemma ip-gt-iff


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. d : Point(rv)
6. ||a - b|| < ||c - d||
⊢ cd > ab
BY
{ ((Assert r0 < ||c - d|| BY
          (Assert ⌜r0 ≤ ||a - b||⌝⋅ THEN Auto))
   THEN D 0
   THEN (Assert (||a - b||/||c - d||) ∈ [r0, r1] BY
               (Reduce 0 THEN D 0 THEN nRMul ⌜||c - d||⌝ 0⋅ THEN Auto))) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. d : Point(rv)
6. ||a - b|| < ||c - d||
7. r0 < ||c - d||
8. (||a - b||/||c - d||) ∈ [r0, r1]
⊢ ∃w:Point(rv). (c_w_d ∧ cw=ab ∧ w # d)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  c  :  Point(rv)
5.  d  :  Point(rv)
6.  ||a  -  b||  <  ||c  -  d||
\mvdash{}  cd  >  ab


By

---

Latex:
((Assert  r0  <  ||c  -  d||  BY
                (Assert  \mkleeneopen{}r0  \mleq{}  ||a  -  b||\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  D  0
  THEN  (Assert  (||a  -  b||/||c  -  d||)  \mmember{}  [r0,  r1]  BY
                          (Reduce  0  THEN  D  0  THEN  nRMul  \mkleeneopen{}||c  -  d||\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index