---

Step * 1 1 1 1 2 1 1 of Lemma rv-midpoint-unique


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. ||m - b|| = ||b - m||
6. a' : Point(rv)
7. m - a = a' ∈ Point(rv)
8. b' : Point(rv)
9. b - m = b' ∈ Point(rv)
10. ||a'|| = (||b - a||/r(2))
11. ||b'|| = (||b - a||/r(2))
12. (a' + b'^2 + a' - b'^2) = (a'^2 + a'^2 + b'^2 + b'^2)
⊢ (||a'||^2 + ||a'||^2 + ||b'||^2 + ||b'||^2) = ||b - a||^2
BY
{ ((RWO "-2 -3" 0 THENA Auto) THEN (GenConcl ⌜||b - a|| = x ∈ ℝ⌝⋅ THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. ||m - b|| = ||b - m||
6. a' : Point(rv)
7. m - a = a' ∈ Point(rv)
8. b' : Point(rv)
9. b - m = b' ∈ Point(rv)
10. ||a'|| = (||b - a||/r(2))
11. ||b'|| = (||b - a||/r(2))
12. (a' + b'^2 + a' - b'^2) = (a'^2 + a'^2 + b'^2 + b'^2)
13. x : ℝ
14. ||b - a|| = x ∈ ℝ
⊢ ((x/r(2))^2 + (x/r(2))^2 + (x/r(2))^2 + (x/r(2))^2) = x^2

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  m  :  Point(rv)
5.  ||m  -  b||  =  ||b  -  m||
6.  a'  :  Point(rv)
7.  m  -  a  =  a'
8.  b'  :  Point(rv)
9.  b  -  m  =  b'
10.  ||a'||  =  (||b  -  a||/r(2))
11.  ||b'||  =  (||b  -  a||/r(2))
12.  (a'  +  b'\^{}2  +  a'  -  b'\^{}2)  =  (a'\^{}2  +  a'\^{}2  +  b'\^{}2  +  b'\^{}2)
\mvdash{}  (||a'||\^{}2  +  ||a'||\^{}2  +  ||b'||\^{}2  +  ||b'||\^{}2)  =  ||b  -  a||\^{}2


By

---

Latex:
((RWO  "-2  -3"  0  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}||b  -  a||  =  x\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index