---

Step * 1 1 1 1 1 of Lemma implies-isometry-lemma5


1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. d : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = d) ∨ (||x - y|| = (r(2) * d))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| = (r(n) * d/r(m))) ⇒ (||f x - f y|| = ||x - y||))
7. s : ℝ
8. r : ℝ
9. n1 : ℕ+
10. m1 : ℕ+
11. s = (r(n1)/r(m1))
12. n : ℕ+
13. m : ℕ+
14. r = (r(n)/r(m))
15. x : Point(rv)
16. y : Point(rv)
17. ||x - y|| ∈ (r * d, s * d)
18. (s - r) = (r((n1 * m) - n * m1)/r(m1 * m))
⊢ ∃n,m:ℕ+. ((s - r) = (r(n)/r(m)))
BY
{ ((Assert (r * d) < (s * d) BY
          (All Reduce THEN Auto))
   THEN (RWO "-9 -6" (-1)⋅ THENA Auto)
   THEN (Assert (r(n)/r(m)) < (r(n1)/r(m1)) BY
               ((nRMul ⌜d⌝ 0⋅ THEN Auto) THEN nRNorm  (-1) THEN Auto))) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. d : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = d) ∨ (||x - y|| = (r(2) * d))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| = (r(n) * d/r(m))) ⇒ (||f x - f y|| = ||x - y||))
7. s : ℝ
8. r : ℝ
9. n1 : ℕ+
10. m1 : ℕ+
11. s = (r(n1)/r(m1))
12. n : ℕ+
13. m : ℕ+
14. r = (r(n)/r(m))
15. x : Point(rv)
16. y : Point(rv)
17. ||x - y|| ∈ (r * d, s * d)
18. (s - r) = (r((n1 * m) - n * m1)/r(m1 * m))
19. ((r(n)/r(m)) * d) < ((r(n1)/r(m1)) * d)
20. (r(n)/r(m)) < (r(n1)/r(m1))
⊢ ∃n,m:ℕ+. ((s - r) = (r(n)/r(m)))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point(rv)  {}\mrightarrow{}  Point(rv)
3.  d  :  \{r:\mBbbR{}|  r0  <  r\} 
4.  \mforall{}x,y:Point(rv).    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
5.  \mforall{}x,y:Point(rv).    (((||x  -  y||  =  d)  \mvee{}  (||x  -  y||  =  (r(2)  *  d)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
6.  \mforall{}n,m:\mBbbN{}\msupplus{}.  \mforall{}x,y:Point(rv).    ((||x  -  y||  =  (r(n)  *  d/r(m)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
7.  s  :  \mBbbR{}
8.  r  :  \mBbbR{}
9.  n1  :  \mBbbN{}\msupplus{}
10.  m1  :  \mBbbN{}\msupplus{}
11.  s  =  (r(n1)/r(m1))
12.  n  :  \mBbbN{}\msupplus{}
13.  m  :  \mBbbN{}\msupplus{}
14.  r  =  (r(n)/r(m))
15.  x  :  Point(rv)
16.  y  :  Point(rv)
17.  ||x  -  y||  \mmember{}  (r  *  d,  s  *  d)
18.  (s  -  r)  =  (r((n1  *  m)  -  n  *  m1)/r(m1  *  m))
\mvdash{}  \mexists{}n,m:\mBbbN{}\msupplus{}.  ((s  -  r)  =  (r(n)/r(m)))


By

---

Latex:
((Assert  (r  *  d)  <  (s  *  d)  BY
                (All  Reduce  THEN  Auto))
  THEN  (RWO  "-9  -6"  (-1)\mcdot{}  THENA  Auto)
  THEN  (Assert  (r(n)/r(m))  <  (r(n1)/r(m1))  BY
                          ((nRMul  \mkleeneopen{}d\mkleeneclose{}  0\mcdot{}  THEN  Auto)  THEN  nRNorm    (-1)  THEN  Auto)))

---

Home Index