:: by Kanchun and Yatsuka Nakamura

::

:: Received February 3, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

theorem :: 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))

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 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;
rng x c= REAL ;

hence x is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum

::$CT

theorem Th10: :: 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)

|.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)

proof end;

theorem Th11: :: 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)

|.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)

proof 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))

(|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))

proof 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)|

(|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|

proof end;

::$CT

theorem Th16: :: 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)|

for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|

proof end;

theorem Th17: :: EUCLID_2:19

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|

for p1, p2 being Point of (TOP-REAL n)

for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|

proof end;

theorem :: EUCLID_2:20

theorem :: EUCLID_2:22

theorem Th22: :: 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)|

for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|

proof end;

theorem :: EUCLID_2:25

for n being Nat

for x, y being Real

for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)

for x, y being Real

for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)

proof end;

theorem :: EUCLID_2:26

theorem :: EUCLID_2:27

theorem Th26: :: 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)|

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 end;

theorem Th27: :: 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)|

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 end;

theorem Th28: :: 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)|

for p, q being Point of (TOP-REAL n) holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem Th29: :: 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)|

for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem :: EUCLID_2:33

theorem :: EUCLID_2:42

theorem Th43: :: 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)

for p, q being Point of (TOP-REAL n) holds |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2)

proof end;

theorem Th44: :: 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)

for p, q being Point of (TOP-REAL n) holds |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2)

proof 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))

for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2))

proof 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)|

for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)|

proof 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))

for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))

proof end;

theorem :: EUCLID_2:54

theorem Th54: :: EUCLID_2:56

for n being Nat

for a being Real

for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

a * p,q are_orthogonal

for a being Real

for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

a * p,q are_orthogonal

proof end;

theorem :: EUCLID_2:57

for n being Nat

for a being Real

for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

p,a * q are_orthogonal by Th54;

for a being Real

for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

p,a * q are_orthogonal by Th54;

theorem :: EUCLID_2:58