:: EUCLID_2 semantic presentation

begin


theorem Th1: :: EUCLID_2:1
for n, i being Nat
for v being Element of n -tuples_on REAL holds (mlt (v,(0* n))) . i = 0
proof
let n, i be Nat; ::_thesis: for v being Element of n -tuples_on REAL holds (mlt (v,(0* n))) . i = 0
let v be Element of n -tuples_on REAL; ::_thesis: (mlt (v,(0* n))) . i = 0
A1: 0* n = n |-> 0 by EUCLID:def_4;
set v0 = (0* n) . i;
A2: dom (0* n) = Seg n by FINSEQ_2:124;
 ( i in Seg n or not i in Seg n ) ;
then A3: (0* n) . i = 0 by A1, A2, FUNCOP_1:7, FUNCT_1:def_2;
(mlt (v,(0* n))) . i = (v . i) * ((0* n) . i) by RVSUM_1:60
.= 0 by A3 ;
hence  (mlt (v,(0* n))) . i = 0 ; ::_thesis: verum
end;

theorem Th2: :: EUCLID_2:2
for n being Nat
for v being Element of n -tuples_on REAL holds mlt (v,(0* n)) = 0* n
proof
let n be Nat; ::_thesis: for v being Element of n -tuples_on REAL holds mlt (v,(0* n)) = 0* n
let v be Element of n -tuples_on REAL; ::_thesis: mlt (v,(0* n)) = 0* n
 len (0* n) = n by CARD_1:def_7;
then reconsider z = 0* n as Element of n -tuples_on REAL by FINSEQ_2:92;
A1: len (0* n) = n by CARD_1:def_7;
A2: for j being Nat st j in dom (0* n) holds
(mlt (v,(0* n))) . j = (0* n) . j
proof
let j be Nat; ::_thesis: ( j in dom (0* n) implies (mlt (v,(0* n))) . j = (0* n) . j )
assume  j in dom (0* n) ; ::_thesis: (mlt (v,(0* n))) . j = (0* n) . j
thus (mlt (v,(0* n))) . j = 0 by Th1
.= (n |-> 0) . j
.= (0* n) . j by EUCLID:def_4 ; ::_thesis: verum
end;
 len (mlt (v,z)) = n by CARD_1:def_7;
then  dom (mlt (v,(0* n))) = dom (0* n) by A1, FINSEQ_3:29;
hence  mlt (v,(0* n)) = 0* n by A2, FINSEQ_1:13; ::_thesis: verum
end;

begin

theorem Th3: :: EUCLID_2:3
for n being Nat
for y1, y2 being real-valued FinSequence
for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds
|(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2))
proof
let n be Nat; ::_thesis: for y1, y2 being real-valued FinSequence
for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds
|(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2))
let y1, y2 be real-valued FinSequence; ::_thesis: for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds
|(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2))
let x1, x2 be Element of REAL n; ::_thesis: ( x1 = y1 & x2 = y2 implies |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2))
reconsider w1 = x1, w2 = x2 as Element of n -tuples_on REAL by EUCLID:def_1;
set v1 = sqr (x1 + x2);
set v2 = sqr (x1 - x2);
set z1 = x1 + x2;
set z2 = x1 - x2;
A2: (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) = (1 / 4) * (((sqrt (Sum (sqr (x1 + x2)))) ^2) - (|.(x1 - x2).| ^2)) by EUCLID:def_5
.= (1 / 4) * (((sqrt (Sum (sqr (x1 + x2)))) ^2) - ((sqrt (Sum (sqr (x1 - x2)))) ^2)) by EUCLID:def_5 ;
 Sum (sqr (x1 + x2)) >= 0 by RVSUM_1:86;
then A3: (sqrt (Sum (sqr (x1 + x2)))) ^2 = Sum (sqr (x1 + x2)) by SQUARE_1:def_2;
A4: (Sum (sqr (x1 + x2))) - (Sum (sqr (x1 - x2))) = Sum ((sqr (x1 + x2)) - (sqr (x1 - x2))) by RVSUM_1:90;
 Sum (sqr (x1 - x2)) >= 0 by RVSUM_1:86;
then A5: (sqrt (Sum (sqr (x1 - x2)))) ^2 = Sum (sqr (x1 - x2)) by SQUARE_1:def_2;
A6: ((2 * (mlt (w1,w2))) + (sqr w2)) + (2 * (mlt (w1,w2))) = (2 * (mlt (w1,w2))) + ((2 * (mlt (w1,w2))) + (sqr w2))
.= ((2 * (mlt (w1,w2))) + (2 * (mlt (w1,w2)))) + (sqr w2) by FINSEQOP:28 ;
A7: (sqr w1) + ((2 * (mlt (w1,w2))) + (sqr w2)) = ((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1) ;
(sqr (x1 + x2)) - (sqr (x1 - x2)) = (((sqr w1) + (2 * (mlt (w1,w2)))) + (sqr w2)) - (sqr (w1 - w2)) by RVSUM_1:68
.= (((sqr w1) + (2 * (mlt (w1,w2)))) + (sqr w2)) - (((sqr w1) - (2 * (mlt (w1,w2)))) + (sqr w2)) by RVSUM_1:69
.= (((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - (((sqr w1) - (2 * (mlt (w1,w2)))) + (sqr w2)) by A7, FINSEQOP:28
.= ((((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - ((sqr w1) - (2 * (mlt (w1,w2))))) - (sqr w2) by RVSUM_1:39
.= (((((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - (sqr w1)) + (2 * (mlt (w1,w2)))) - (sqr w2) by RVSUM_1:41
.= (((2 * (mlt (w1,w2))) + (sqr w2)) + (2 * (mlt (w1,w2)))) - (sqr w2) by RVSUM_1:42
.= (2 * (mlt (w1,w2))) + (2 * (mlt (w1,w2))) by A6, RVSUM_1:42
.= (2 + 2) * (mlt (w1,w2)) by RVSUM_1:50
.= 4 * (mlt (w1,w2)) ;
then (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) = (1 / 4) * (4 * (Sum (mlt (w1,w2)))) by A2, A3, A5, A4, RVSUM_1:87
.= Sum (mlt (w1,w2)) ;
hence  |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) by A1; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_x_being_real-valued_FinSequence_holds_x_is_FinSequence_of_REAL
let x be real-valued FinSequence; ::_thesis: x is FinSequence of REAL
 rng x c= REAL ;
hence  x is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum
end;

theorem Th4: :: EUCLID_2:4
for x being real-valued FinSequence holds |.x.| ^2 = |(x,x)|
proof
let x be real-valued FinSequence; ::_thesis: |.x.| ^2 = |(x,x)|
A1: 0 <= |(x,x)| by RVSUM_1:119;
|.x.| ^2 = (sqrt (Sum (sqr x))) ^2 by EUCLID:def_5
.= |(x,x)| by A1, SQUARE_1:def_2 ;
hence  |.x.| ^2 = |(x,x)| ; ::_thesis: verum
end;

theorem Th5: :: EUCLID_2:5
for x being real-valued FinSequence holds |.x.| = sqrt |(x,x)|
proof
let x be real-valued FinSequence; ::_thesis: |.x.| = sqrt |(x,x)|
|.x.| = sqrt (|.x.| ^2) by EUCLID:9, SQUARE_1:22
.= sqrt |(x,x)| by Th4 ;
hence  |.x.| = sqrt |(x,x)| ; ::_thesis: verum
end;

theorem Th6: :: EUCLID_2:6
for x being real-valued FinSequence holds 0 <= |.x.|
proof
let x be real-valued FinSequence; ::_thesis: 0 <= |.x.|
 ( |.x.| = sqrt |(x,x)| & 0 <= |(x,x)| ) by Th5, RVSUM_1:119;
hence  0 <= |.x.| by SQUARE_1:def_2; ::_thesis: verum
end;

theorem Th7: :: EUCLID_2:7
for x being real-valued FinSequence holds
( |(x,x)| = 0 iff x = 0* (len x) )
proof
let x be real-valued FinSequence; ::_thesis: ( |(x,x)| = 0 iff x = 0* (len x) )
thus  ( |(x,x)| = 0 implies x = 0* (len x) ) ::_thesis: ( x = 0* (len x) implies |(x,x)| = 0 )
proof
 x is FinSequence of REAL by Lm1;
then reconsider y = x as Element of REAL (len x) by EUCLID:76;
assume  |(x,x)| = 0 ; ::_thesis: x = 0* (len x)
then  |.x.| ^2 = 0 by Th4;
then  |.x.| = 0 by XCMPLX_1:6;
then  y = 0* (len x) by EUCLID:8;
hence  x = 0* (len x) ; ::_thesis: verum
end;
assume  x = 0* (len x) ; ::_thesis: |(x,x)| = 0
then  |.x.| = 0 by EUCLID:7;
then  |(x,x)| = 0 ^2 by Th4;
hence  |(x,x)| = 0 ; ::_thesis: verum
end;

theorem :: EUCLID_2:8
for x being real-valued FinSequence holds
( |(x,x)| = 0 iff |.x.| = 0 )
proof
let x be real-valued FinSequence; ::_thesis: ( |(x,x)| = 0 iff |.x.| = 0 )
A1: ( |(x,x)| = 0 ^2 implies |.x.| = 0 )
proof
assume  |(x,x)| = 0 ^2 ; ::_thesis: |.x.| = 0
then  x = 0* (len x) by Th7;
hence  |.x.| = 0 by EUCLID:7; ::_thesis: verum
end;
 ( |.x.| = 0 implies |(x,x)| = 0 ^2 ) by Th4;
hence  ( |(x,x)| = 0 iff |.x.| = 0 ) by A1; ::_thesis: verum
end;

theorem Th9: :: EUCLID_2:9
for x being real-valued FinSequence holds |(x,(0* (len x)))| = 0
proof
let x be real-valued FinSequence; ::_thesis: |(x,(0* (len x)))| = 0
set n = len x;
 x is FinSequence of REAL by Lm1;
then reconsider p1 = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
A1: 0* (len x) = (len x) |-> 0 by EUCLID:def_4;
|(x,(0* (len x)))| = Sum (mlt (p1,(0* (len x))))
.= Sum (0* (len x)) by Th2
.= 0 by A1, RVSUM_1:81 ;
hence  |(x,(0* (len x)))| = 0 ; ::_thesis: verum
end;

theorem :: EUCLID_2:10
for x being real-valued FinSequence holds |((0* (len x)),x)| = 0 by Th9;

theorem Th11: :: EUCLID_2:11
for x, y being real-valued FinSequence st len x = len y holds
|.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) )
assume A1: len x = len y ; ::_thesis: |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)
|.(x + y).| ^2 = |((x + y),(x + y))| by Th4
.= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by A1, RVSUM_1:128
.= ((|.x.| ^2) + (2 * |(y,x)|)) + |(y,y)| by Th4
.= ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) by Th4 ;
hence  |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) ; ::_thesis: verum
end;

theorem Th12: :: EUCLID_2:12
for x, y being real-valued FinSequence st len x = len y holds
|.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) )
assume A1: len x = len y ; ::_thesis: |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)
|.(x - y).| ^2 = |((x - y),(x - y))| by Th4
.= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| by A1, RVSUM_1:129
.= ((|.x.| ^2) - (2 * |(y,x)|)) + |(y,y)| by Th4
.= ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) by Th4 ;
hence  |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) ; ::_thesis: verum
end;

theorem :: EUCLID_2:13
for x, y being real-valued FinSequence st len x = len y holds
(|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) )
assume A1: len x = len y ; ::_thesis: (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))
then (|.(x + y).| ^2) + (|.(x - y).| ^2) = (((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)) + (|.(x - y).| ^2) by Th11
.= (((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)) + (((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)) by A1, Th12
.= 2 * ((|.x.| ^2) + (|.y.| ^2)) ;
hence  (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) ; ::_thesis: verum
end;

theorem :: EUCLID_2:14
for x, y being real-valued FinSequence st len x = len y holds
(|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| )
assume A1: len x = len y ; ::_thesis: (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|
then (|.(x + y).| ^2) - (|.(x - y).| ^2) = (((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)) - (|.(x - y).| ^2) by Th11
.= (((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)) - (((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)) by A1, Th12
.= 4 * |(x,y)| ;
hence  (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| ; ::_thesis: verum
end;

theorem Th15: :: EUCLID_2:15
for x, y being real-valued FinSequence st len x = len y holds
abs |(x,y)| <= |.x.| * |.y.|
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies abs |(x,y)| <= |.x.| * |.y.| )
assume A1: len x = len y ; ::_thesis: abs |(x,y)| <= |.x.| * |.y.|
A2: ( x = 0* (len x) implies abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) )
proof
assume  x = 0* (len x) ; ::_thesis: abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|)
then  ( |(x,y)| = 0 & |(x,x)| = 0 ) by A1, Th9;
hence  abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by ABSVALUE:2, SQUARE_1:17; ::_thesis: verum
end;
A3: ( x <> 0* (len x) implies abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) )
proof
A4: for t being real number holds ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0
proof
let t be real number ; ::_thesis: ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0
set s = t ^2 ;
A5: len (t * x) = len x by RVSUM_1:117;
 |(((t * x) + y),((t * x) + y))| >= 0 by RVSUM_1:119;
then  (|((t * x),(t * x))| + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, A5, RVSUM_1:128;
then  ((t * |((t * x),x)|) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A5, RVSUM_1:121;
then  ((t * (t * |(x,x)|)) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, RVSUM_1:121;
then  ((|(x,x)| * (t ^2)) + (2 * (|(x,y)| * t))) + |(y,y)| >= 0 by A1, RVSUM_1:121;
hence  ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0 ; ::_thesis: verum
end;
set w = abs |(x,y)|;
set u = |(x,y)|;
A6: |(x,x)| >= 0 by RVSUM_1:119;
assume  x <> 0* (len x) ; ::_thesis: abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|)
then  |(x,x)| <> 0 by Th7;
then  |(x,x)| > 0 by A6, XXREAL_0:1;
then  delta (|(x,x)|,(2 * |(x,y)|),|(y,y)|) <= 0 by A4, QUIN_1:10;
then  ((2 * |(x,y)|) ^2) - ((4 * |(x,x)|) * |(y,y)|) <= 0 by QUIN_1:def_1;
then  4 * ((|(x,y)| ^2) - (|(x,x)| * |(y,y)|)) <= 0 ;
then  (|(x,y)| ^2) - (|(x,x)| * |(y,y)|) <= 0 / 4 by XREAL_1:77;
then  |(x,y)| ^2 <= |(x,x)| * |(y,y)| by XREAL_1:50;
then  ( 0 <= (abs |(x,y)|) ^2 & (abs |(x,y)|) ^2 <= |(x,x)| * |(y,y)| ) by COMPLEX1:75, XREAL_1:63;
then  sqrt ((abs |(x,y)|) ^2) <= sqrt (|(x,x)| * |(y,y)|) by SQUARE_1:26;
then A7: abs |(x,y)| <= sqrt (|(x,x)| * |(y,y)|) by COMPLEX1:46, SQUARE_1:22;
 |(y,y)| >= 0 by RVSUM_1:119;
hence  abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by A6, A7, SQUARE_1:29; ::_thesis: verum
end;
 sqrt |(x,x)| = |.x.| by Th5;
hence  abs |(x,y)| <= |.x.| * |.y.| by A2, A3, Th5; ::_thesis: verum
end;

theorem Th16: :: EUCLID_2:16
for x, y being real-valued FinSequence st len x = len y holds
|.(x + y).| <= |.x.| + |.y.|
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |.(x + y).| <= |.x.| + |.y.| )
assume A1: len x = len y ; ::_thesis: |.(x + y).| <= |.x.| + |.y.|
then  ( |(x,y)| <= abs |(x,y)| & abs |(x,y)| <= |.x.| * |.y.| ) by Th15, ABSVALUE:4;
then  |(x,y)| <= |.x.| * |.y.| by XXREAL_0:2;
then  2 * |(x,y)| <= 2 * (|.x.| * |.y.|) by XREAL_1:64;
then A2: (|.x.| ^2) + (2 * |(x,y)|) <= (|.x.| ^2) + (2 * (|.x.| * |.y.|)) by XREAL_1:7;
 |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) by A1, Th11;
then A3: |.(x + y).| ^2 <= ((|.x.| ^2) + ((2 * |.x.|) * |.y.|)) + (|.y.| ^2) by A2, XREAL_1:7;
 0 <= |.(x + y).| ^2 by XREAL_1:63;
then  sqrt (|.(x + y).| ^2) <= sqrt ((|.x.| + |.y.|) ^2) by A3, SQUARE_1:26;
then A4: |.(x + y).| <= sqrt ((|.x.| + |.y.|) ^2) by Th6, SQUARE_1:22;
 ( 0 <= |.x.| & 0 <= |.y.| ) by Th6;
then  0 + 0 <= |.x.| + |.y.| by XREAL_1:7;
hence  |.(x + y).| <= |.x.| + |.y.| by A4, SQUARE_1:22; ::_thesis: verum
end;

begin

theorem :: EUCLID_2:17
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2))
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2))
let p1, p2 be Point of (TOP-REAL n); ::_thesis: |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2))
reconsider q1 = p1, q2 = p2 as Element of REAL n by EUCLID:22;
thus |(p1,p2)| = (1 / 4) * ((|.(q1 + q2).| ^2) - (|.(q1 - q2).| ^2)) by Th3
.= (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2)) ; ::_thesis: verum
end;

theorem Th18: :: EUCLID_2:18
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
proof
let n be Nat; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
reconsider f1 = p1, f2 = p2, f3 = p3 as FinSequence of REAL by EUCLID:24;
reconsider q1 = p1, q2 = p2 as Element of REAL n by EUCLID:22;
 len f2 = n by CARD_1:def_7;
then A1: ( len f1 = len f2 & len f2 = len f3 ) by CARD_1:def_7;
thus  |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| by A1, RVSUM_1:120; ::_thesis: verum
end;

theorem Th19: :: EUCLID_2:19
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
let x be real number ; ::_thesis: |((x * p1),p2)| = x * |(p1,p2)|
reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID:24;
reconsider q1 = p1 as Element of REAL n by EUCLID:22;
 ( len f1 = n & len f2 = n ) by CARD_1:def_7;
hence  |((x * p1),p2)| = x * |(p1,p2)| by RVSUM_1:121; ::_thesis: verum
end;

theorem :: EUCLID_2:20
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds |(p1,(x * p2))| = x * |(p1,p2)| by Th19;

theorem Th21: :: EUCLID_2:21
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |((- p1),p2)| = - |(p1,p2)|
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds |((- p1),p2)| = - |(p1,p2)|
let p1, p2 be Point of (TOP-REAL n); ::_thesis: |((- p1),p2)| = - |(p1,p2)|
|((- p1),p2)| = |(((- 1) * p1),p2)|
.= (- 1) * |(p1,p2)| by Th19 ;
hence  |((- p1),p2)| = - |(p1,p2)| ; ::_thesis: verum
end;

theorem :: EUCLID_2:22
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |(p1,(- p2))| = - |(p1,p2)| by Th21;

theorem :: EUCLID_2:23
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |((- p1),(- p2))| = |(p1,p2)|
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds |((- p1),(- p2))| = |(p1,p2)|
let p1, p2 be Point of (TOP-REAL n); ::_thesis: |((- p1),(- p2))| = |(p1,p2)|
|((- p1),(- p2))| = - |(p1,(- p2))| by Th21
.= - (- |(p1,p2)|) by Th21 ;
hence  |((- p1),(- p2))| = |(p1,p2)| ; ::_thesis: verum
end;

theorem Th24: :: EUCLID_2:24
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
proof
let n be Nat; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
|((p1 - p2),p3)| = |(p1,p3)| + |((- p2),p3)| by Th18
.= |(p1,p3)| + (- |(p2,p3)|) by Th21 ;
hence  |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| ; ::_thesis: verum
end;

theorem :: EUCLID_2:25
for n being Nat
for x, y being real number
for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
proof
let n be Nat; ::_thesis: for x, y being real number
for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
let x, y be real number ; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
|(((x * p1) + (y * p2)),p3)| = |((x * p1),p3)| + |((y * p2),p3)| by Th18
.= (x * |(p1,p3)|) + |((y * p2),p3)| by Th19
.= (x * |(p1,p3)|) + (y * |(p2,p3)|) by Th19 ;
hence  |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) ; ::_thesis: verum
end;

theorem :: EUCLID_2:26
for n being Nat
for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 + q2))| = |(p,q1)| + |(p,q2)| by Th18;

theorem :: EUCLID_2:27
for n being Nat
for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 - q2))| = |(p,q1)| - |(p,q2)| by Th24;

theorem Th28: :: EUCLID_2:28
for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
proof
let n be Nat; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
A1: ( |((p1 + p2),q1)| = |(p1,q1)| + |(p2,q1)| & |((p1 + p2),q2)| = |(p1,q2)| + |(p2,q2)| ) by Th18;
|((p1 + p2),(q1 + q2))| = |((p1 + p2),q1)| + |((p1 + p2),q2)| by Th18
.= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A1 ;
hence  |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum
end;

theorem Th29: :: EUCLID_2:29
for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
proof
let n be Nat; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
A1: ( |(p1,(q1 - q2))| = |(p1,q1)| - |(p1,q2)| & |(p2,(q1 - q2))| = |(p2,q1)| - |(p2,q2)| ) by Th24;
|((p1 - p2),(q1 - q2))| = |(p1,(q1 - q2))| - |(p2,(q1 - q2))| by Th24
.= ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by A1 ;
hence  |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum
end;

theorem Th30: :: EUCLID_2:30
for n being Nat
for p, q being Point of (TOP-REAL n) holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
let p, q be Point of (TOP-REAL n); ::_thesis: |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
 (|(p,p)| + |(p,q)|) + |(p,q)| = |(p,p)| + (2 * |(p,q)|) ;
hence  |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by Th28; ::_thesis: verum
end;

theorem Th31: :: EUCLID_2:31
for n being Nat
for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
let p, q be Point of (TOP-REAL n); ::_thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
|((p - q),(p - q))| = ((|(p,p)| - |(p,q)|) - |(p,q)|) + |(q,q)| by Th29
.= (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ;
hence  |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; ::_thesis: verum
end;

theorem Th32: :: EUCLID_2:32
for n being Nat
for p being Point of (TOP-REAL n) holds |(p,(0. (TOP-REAL n)))| = 0
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds |(p,(0. (TOP-REAL n)))| = 0
let p be Point of (TOP-REAL n); ::_thesis: |(p,(0. (TOP-REAL n)))| = 0
reconsider f1 = p as FinSequence of REAL by EUCLID:24;
 len f1 = n by CARD_1:def_7;
then  0* (len f1) = 0. (TOP-REAL n) by EUCLID:70;
hence  |(p,(0. (TOP-REAL n)))| = 0 by Th9; ::_thesis: verum
end;

theorem :: EUCLID_2:33
for n being Nat
for p being Point of (TOP-REAL n) holds |((0. (TOP-REAL n)),p)| = 0 by Th32;

theorem :: EUCLID_2:34
for n being Nat holds |((0. (TOP-REAL n)),(0. (TOP-REAL n)))| = 0 by Th32;

theorem Th35: :: EUCLID_2:35
for n being Nat
for p being Point of (TOP-REAL n) holds |(p,p)| >= 0 by RVSUM_1:119;

theorem Th36: :: EUCLID_2:36
for n being Nat
for p being Point of (TOP-REAL n) holds |(p,p)| = |.p.| ^2 by Th4;

theorem Th37: :: EUCLID_2:37
for n being Nat
for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)|
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)|
let p be Point of (TOP-REAL n); ::_thesis: |.p.| = sqrt |(p,p)|
 n in NAT by ORDINAL1:def_12;
then |.p.| = sqrt (|.p.| ^2) by SQUARE_1:22, TOPRNS_1:25
.= sqrt |(p,p)| by Th36 ;
hence  |.p.| = sqrt |(p,p)| ; ::_thesis: verum
end;

theorem Th38: :: EUCLID_2:38
for n being Nat
for p being Point of (TOP-REAL n) holds 0 <= |.p.|
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds 0 <= |.p.|
let p be Point of (TOP-REAL n); ::_thesis: 0 <= |.p.|
 ( |.p.| = sqrt |(p,p)| & 0 <= |(p,p)| ) by Th35, Th37;
hence  0 <= |.p.| by SQUARE_1:def_2; ::_thesis: verum
end;

theorem Th39: :: EUCLID_2:39
for n being Nat holds |.(0. (TOP-REAL n)).| = 0
proof
let n be Nat; ::_thesis: |.(0. (TOP-REAL n)).| = 0
 n in NAT by ORDINAL1:def_12;
hence  |.(0. (TOP-REAL n)).| = 0 by TOPRNS_1:23; ::_thesis: verum
end;

theorem Th40: :: EUCLID_2:40
for n being Nat
for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff |.p.| = 0 )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff |.p.| = 0 )
let p be Point of (TOP-REAL n); ::_thesis: ( |(p,p)| = 0 iff |.p.| = 0 )
A1: ( |(p,p)| = 0 ^2 implies |.p.| = 0 )
proof
assume  |(p,p)| = 0 ^2 ; ::_thesis: |.p.| = 0
then  |.p.| ^2 = 0 by Th36;
hence  |.p.| = 0 by XCMPLX_1:6; ::_thesis: verum
end;
 ( |.p.| = 0 implies |(p,p)| = 0 ^2 ) by Th36;
hence  ( |(p,p)| = 0 iff |.p.| = 0 ) by A1; ::_thesis: verum
end;

theorem Th41: :: EUCLID_2:41
for n being Nat
for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )
let p be Point of (TOP-REAL n); ::_thesis: ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )
 ( |(p,p)| = 0 implies p = 0. (TOP-REAL n) )
proof
assume  |(p,p)| = 0 ; ::_thesis: p = 0. (TOP-REAL n)
then  ( n in NAT & |.p.| = 0 ) by Th40, ORDINAL1:def_12;
hence  p = 0. (TOP-REAL n) by TOPRNS_1:24; ::_thesis: verum
end;
hence  ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) ) by Th32; ::_thesis: verum
end;

theorem :: EUCLID_2:42
for n being Nat
for p being Point of (TOP-REAL n) holds
( |.p.| = 0 iff p = 0. (TOP-REAL n) )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds
( |.p.| = 0 iff p = 0. (TOP-REAL n) )
let p be Point of (TOP-REAL n); ::_thesis: ( |.p.| = 0 iff p = 0. (TOP-REAL n) )
 n in NAT by ORDINAL1:def_12;
hence  ( |.p.| = 0 iff p = 0. (TOP-REAL n) ) by Th39, TOPRNS_1:24; ::_thesis: verum
end;

theorem :: EUCLID_2:43
for n being Nat
for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )
let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )
 ( p <> 0. (TOP-REAL n) implies |(p,p)| > 0 )
proof
assume  p <> 0. (TOP-REAL n) ; ::_thesis: |(p,p)| > 0
then A1: |(p,p)| <> 0 by Th41;
 0 <= |(p,p)| by Th35;
hence  |(p,p)| > 0 by A1, XXREAL_0:1; ::_thesis: verum
end;
hence  ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 ) by Th41; ::_thesis: verum
end;

theorem :: EUCLID_2:44
for n being Nat
for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |.p.| > 0 )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |.p.| > 0 )
let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) iff |.p.| > 0 )
 ( p <> 0. (TOP-REAL n) implies |.p.| > 0 )
proof
assume A1: p <> 0. (TOP-REAL n) ; ::_thesis: |.p.| > 0
 ( n in NAT & 0 <= |.p.| ) by Th38, ORDINAL1:def_12;
hence  |.p.| > 0 by A1, TOPRNS_1:24, XXREAL_0:1; ::_thesis: verum
end;
hence  ( p <> 0. (TOP-REAL n) iff |.p.| > 0 ) by Th39; ::_thesis: verum
end;

theorem Th45: :: EUCLID_2:45
for n being Nat
for p, q being Point of (TOP-REAL n) holds |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2)
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2)
let p, q be Point of (TOP-REAL n); ::_thesis: |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2)
|.(p + q).| ^2 = |((p + q),(p + q))| by Th36
.= (|(p,p)| + (2 * |(q,p)|)) + |(q,q)| by Th30
.= ((|.p.| ^2) + (2 * |(q,p)|)) + |(q,q)| by Th36
.= ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) by Th36 ;
hence  |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) ; ::_thesis: verum
end;

theorem Th46: :: EUCLID_2:46
for n being Nat
for p, q being Point of (TOP-REAL n) holds |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2)
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2)
let p, q be Point of (TOP-REAL n); ::_thesis: |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2)
|.(p - q).| ^2 = |((p - q),(p - q))| by Th36
.= (|(p,p)| - (2 * |(q,p)|)) + |(q,q)| by Th31
.= ((|.p.| ^2) - (2 * |(q,p)|)) + |(q,q)| by Th36
.= ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) by Th36 ;
hence  |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) ; ::_thesis: verum
end;

theorem :: EUCLID_2:47
for n being Nat
for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2))
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2))
let p, q be Point of (TOP-REAL n); ::_thesis: (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2))
A1: ((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2) = ((|.p.| ^2) + (|.q.| ^2)) - (2 * |(p,q)|) ;
(|.(p + q).| ^2) + (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) + (|.(p - q).| ^2) by Th45
.= (((|.p.| ^2) + (|.q.| ^2)) + (2 * |(p,q)|)) + (((|.p.| ^2) + (|.q.| ^2)) - (2 * |(p,q)|)) by A1, Th46
.= 2 * ((|.p.| ^2) + (|.q.| ^2)) ;
hence  (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2)) ; ::_thesis: verum
end;

theorem :: EUCLID_2:48
for n being Nat
for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)|
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)|
let p, q be Point of (TOP-REAL n); ::_thesis: (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)|
(|.(p + q).| ^2) - (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (|.(p - q).| ^2) by Th45
.= (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2)) by Th46
.= 4 * |(p,q)| ;
hence  (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)| ; ::_thesis: verum
end;

theorem :: EUCLID_2:49
for n being Nat
for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
let p, q be Point of (TOP-REAL n); ::_thesis: |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
(|.(p + q).| ^2) - (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (|.(p - q).| ^2) by Th45
.= (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2)) by Th46
.= 4 * |(p,q)| ;
hence  |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2)) ; ::_thesis: verum
end;

theorem :: EUCLID_2:50
for n being Nat
for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)|
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)|
let p, q be Point of (TOP-REAL n); ::_thesis: |(p,q)| <= |(p,p)| + |(q,q)|
 ( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th35;
then  0 + 0 <= |(p,p)| + |(q,q)| by XREAL_1:7;
then A1: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72;
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th31
.= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ;
then  2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by Th35, XREAL_1:11;
then  (2 * |(p,q)|) / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72;
then  0 + |(p,q)| <= ((|(p,p)| + |(q,q)|) / 2) + ((|(p,p)| + |(q,q)|) / 2) by A1, XREAL_1:7;
hence  |(p,q)| <= |(p,p)| + |(q,q)| ; ::_thesis: verum
end;

theorem :: EUCLID_2:51
for n being Nat
for p, q being Point of (TOP-REAL n) holds abs |(p,q)| <= |.p.| * |.q.|
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds abs |(p,q)| <= |.p.| * |.q.|
let p, q be Point of (TOP-REAL n); ::_thesis: abs |(p,q)| <= |.p.| * |.q.|
 ( len p = n & len q = n ) by CARD_1:def_7;
hence  abs |(p,q)| <= |.p.| * |.q.| by Th15; ::_thesis: verum
end;

theorem :: EUCLID_2:52
for n being Nat
for p, q being Point of (TOP-REAL n) holds |.(p + q).| <= |.p.| + |.q.|
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |.(p + q).| <= |.p.| + |.q.|
let p, q be Point of (TOP-REAL n); ::_thesis: |.(p + q).| <= |.p.| + |.q.|
A1: ( len p = n & len q = n ) by CARD_1:def_7;
thus  |.(p + q).| <= |.p.| + |.q.| by A1, Th16; ::_thesis: verum
end;

theorem Th53: :: EUCLID_2:53
for n being Nat
for p being Point of (TOP-REAL n) holds p, 0. (TOP-REAL n) are_orthogonal
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds p, 0. (TOP-REAL n) are_orthogonal
let p be Point of (TOP-REAL n); ::_thesis: p, 0. (TOP-REAL n) are_orthogonal
 |(p,(0. (TOP-REAL n)))| = 0 by Th32;
hence  p, 0. (TOP-REAL n) are_orthogonal by RVSUM_1:def_17; ::_thesis: verum
end;

theorem :: EUCLID_2:54
for n being Nat
for p being Point of (TOP-REAL n) holds 0. (TOP-REAL n),p are_orthogonal by Th53;

theorem Th55: :: EUCLID_2:55
for n being Nat
for p being Point of (TOP-REAL n) holds
( p,p are_orthogonal iff p = 0. (TOP-REAL n) )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds
( p,p are_orthogonal iff p = 0. (TOP-REAL n) )
let p be Point of (TOP-REAL n); ::_thesis: ( p,p are_orthogonal iff p = 0. (TOP-REAL n) )
 ( p,p are_orthogonal iff |(p,p)| = 0 ) by RVSUM_1:def_17;
hence  ( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) by Th41; ::_thesis: verum
end;

theorem Th56: :: EUCLID_2:56
for n being Nat
for a being real number
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
a * p,q are_orthogonal
proof
let n be Nat; ::_thesis: for a being real number
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
a * p,q are_orthogonal
let a be real number ; ::_thesis: for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
a * p,q are_orthogonal
let p, q be Point of (TOP-REAL n); ::_thesis: ( p,q are_orthogonal implies a * p,q are_orthogonal )
assume  p,q are_orthogonal ; ::_thesis: a * p,q are_orthogonal
then  |(p,q)| = 0 by RVSUM_1:def_17;
then  a * |(p,q)| = 0 ;
then  |((a * p),q)| = 0 by Th19;
hence  a * p,q are_orthogonal by RVSUM_1:def_17; ::_thesis: verum
end;

theorem :: EUCLID_2:57
for n being Nat
for a being real number
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
p,a * q are_orthogonal by Th56;

theorem :: EUCLID_2:58
for n being Nat
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) holds
p = 0. (TOP-REAL n)
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) holds
p = 0. (TOP-REAL n)
let p be Point of (TOP-REAL n); ::_thesis: ( ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) implies p = 0. (TOP-REAL n) )
assume  for q being Point of (TOP-REAL n) holds p,q are_orthogonal ; ::_thesis: p = 0. (TOP-REAL n)
then  p,p are_orthogonal ;
hence  p = 0. (TOP-REAL n) by Th55; ::_thesis: verum
end;