:: EUCLID_4 semantic presentation

theorem Th1: :: EUCLID_4:1

for n being Nat
for x being Element of REAL n holds
( (0 * x) + x = x & x + (0* n) = x )

proof end;

theorem Th2: :: EUCLID_4:2

for a being Real
for n being Nat holds a * (0* n) = 0* n

proof end;

theorem Th3: :: EUCLID_4:3

for n being Nat
for x being Element of REAL n holds
( 1 * x = x & 0 * x = 0* n )

proof end;

theorem Th4: :: EUCLID_4:4

for a, b being Real
for n being Nat
for x being Element of REAL n holds (a * b) * x = a * (b * x)

proof end;

theorem :: EUCLID_4:5

for a being Real
for n being Nat
for x being Element of REAL n holds
( not a * x = 0* n or a = 0 or x = 0* n )

proof end;

theorem Th6: :: EUCLID_4:6

for a being Real
for n being Nat
for x1, x2 being Element of REAL n holds a * (x1 + x2) = (a * x1) + (a * x2)

proof end;

theorem Th7: :: EUCLID_4:7

for a, b being Real
for n being Nat
for x being Element of REAL n holds (a + b) * x = (a * x) + (b * x)

proof end;

theorem :: EUCLID_4:8

for a being Real
for n being Nat
for x1, x2 being Element of REAL n holds
( not a * x1 = a * x2 or a = 0 or x1 = x2 )

proof end;

definition

let n be Nat;
let x1, x2 be Element of REAL n;
func Line x1,x2 -> Subset of (REAL n) equals :: EUCLID_4:def 1
{ (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;
coherence

proof end;

end;

:: deftheorem defines Line EUCLID_4:def 1 :

registration

let n be Nat;
let x1, x2 be Element of REAL n;
cluster Line x1,x2 -> non empty ;
coherence

proof end;

end;

Lm1: for n being Nat
for x1, x2 being Element of REAL n holds Line x1,x2 c= Line x2,x1

proof end;

theorem Th9: :: EUCLID_4:9

for n being Nat
for x1, x2 being Element of REAL n holds Line x1,x2 = Line x2,x1

proof end;

definition

let n be Nat;
let x1, x2 be Element of REAL n;
:: original: Line
redefine func Line x1,x2 -> Subset of (REAL n);
commutativity by Th9;

end;

theorem Th10: :: EUCLID_4:10

for n being Nat
for x1, x2 being Element of REAL n holds
( x1 in Line x1,x2 & x2 in Line x1,x2 )

proof end;

Lm2: for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 + (x2 + x3) = (x1 + x2) + x3

proof end;

theorem Th11: :: EUCLID_4:11

for n being Nat
for y1, x1, x2, y2 being Element of REAL n st y1 in Line x1,x2 & y2 in Line x1,x2 holds
Line y1,y2 c= Line x1,x2

proof end;

theorem Th12: :: EUCLID_4:12

for n being Nat
for y1, x1, x2, y2 being Element of REAL n st y1 in Line x1,x2 & y2 in Line x1,x2 & y1 <> y2 holds
Line x1,x2 c= Line y1,y2

proof end;

definition

let n be Nat;
let A be Subset of (REAL n);
attr A is being_line means :Def2: :: EUCLID_4:def 2
ex x1, x2 being Element of REAL n st
( x1 <> x2 & A = Line x1,x2 );

end;

:: deftheorem Def2 defines being_line EUCLID_4:def 2 :

notation

let n be Nat;
let A be Subset of (REAL n);
synonym A is_line for being_line A;

end;

Lm3: for n being Nat
for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line x1,x2

proof end;

theorem :: EUCLID_4:13

for n being Nat
for A, C being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is_line & C is_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C

proof end;

theorem Th14: :: EUCLID_4:14

for n being Nat
for A being Subset of (REAL n) st A is_line holds
ex x1, x2 being Element of REAL n st
( x1 in A & x2 in A & x1 <> x2 )

proof end;

theorem :: EUCLID_4:15

for n being Nat
for x1 being Element of REAL n
for A being Subset of (REAL n) st A is_line holds
ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A )

proof end;

definition

let n be Nat;
let x be Element of REAL n;
func Rn2Fin x -> FinSequence of REAL equals :: EUCLID_4:def 3
x;
correctness

proof end;

end;

:: deftheorem defines Rn2Fin EUCLID_4:def 3 :

definition

let n be Nat;
let x be Element of REAL n;
func |.x.| -> Real equals :: EUCLID_4:def 4
|.(Rn2Fin x).|;
correctness ;

end;

:: deftheorem defines |. EUCLID_4:def 4 :

definition

let n be Nat;
let x1, x2 be Element of REAL n;
func |(x1,x2)| -> Real equals :: EUCLID_4:def 5
|((Rn2Fin x1),(Rn2Fin x2))|;
correctness by XREAL_0:def 1;
commutativity ;

end;

:: deftheorem defines |( EUCLID_4:def 5 :

theorem Th16: :: EUCLID_4:16

for n being Nat
for x1, x2 being Element of REAL n holds |(x1,x2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 )) by EUCLID_2:10;

theorem :: EUCLID_4:17

for n being Nat
for x being Element of REAL n holds |(x,x)| >= 0 by EUCLID_2:11;

theorem Th18: :: EUCLID_4:18

for n being Nat
for x being Element of REAL n holds |.x.| ^2 = |(x,x)| by EUCLID_2:12;

theorem Th19: :: EUCLID_4:19

for n being Nat
for x being Element of REAL n holds 0 <= |.x.| by EUCLID_2:14;

theorem :: EUCLID_4:20

for n being Nat
for x being Element of REAL n holds |.x.| = sqrt |(x,x)|

proof end;

theorem Th21: :: EUCLID_4:21

for n being Nat
for x being Element of REAL n holds
( |(x,x)| = 0 iff |.x.| = 0 )

proof end;

Lm4: for n being Nat
for x being Element of REAL n holds x - (0* n) = x

proof end;

Lm5: for n being Nat
for x being Element of REAL n holds (0* n) - x = - x

proof end;

theorem Th22: :: EUCLID_4:22

for n being Nat
for x being Element of REAL n holds
( |(x,x)| = 0 iff x = 0* n )

proof end;

theorem Th23: :: EUCLID_4:23

for n being Nat
for x being Element of REAL n holds |(x,(0* n))| = 0

proof end;

theorem :: EUCLID_4:24

for n being Nat
for x being Element of REAL n holds |((0* n),x)| = 0 by Th23;

Lm6: for n being Nat
for x being Element of REAL n holds len (Rn2Fin x) = n
by EUCLID:2;

theorem Th25: :: EUCLID_4:25

for n being Nat
for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|

proof end;

theorem Th26: :: EUCLID_4:26

for n being Nat
for x1, x2 being Element of REAL n
for a being real number holds |((a * x1),x2)| = a * |(x1,x2)|

proof end;

theorem :: EUCLID_4:27

for n being Nat
for x1, x2 being Element of REAL n
for a being real number holds |(x1,(a * x2))| = a * |(x1,x2)| by Th26;

theorem Th28: :: EUCLID_4:28

for n being Nat
for x1, x2 being Element of REAL n holds |((- x1),x2)| = - |(x1,x2)|

proof end;

theorem :: EUCLID_4:29

for n being Nat
for x1, x2 being Element of REAL n holds |(x1,(- x2))| = - |(x1,x2)| by Th28;

theorem :: EUCLID_4:30

for n being Nat
for x1, x2 being Element of REAL n holds |((- x1),(- x2))| = |(x1,x2)|

proof end;

theorem Th31: :: EUCLID_4:31

for n being Nat
for x1, x2, x3 being Element of REAL n holds |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|

proof end;

theorem :: EUCLID_4:32

for n being Nat
for a, b being real number
for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)

proof end;

theorem :: EUCLID_4:33

for n being Nat
for x1, y1, y2 being Element of REAL n holds |(x1,(y1 + y2))| = |(x1,y1)| + |(x1,y2)| by Th25;

theorem :: EUCLID_4:34

for n being Nat
for x1, y1, y2 being Element of REAL n holds |(x1,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by Th31;

theorem Th35: :: EUCLID_4:35

for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th36: :: EUCLID_4:36

for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th37: :: EUCLID_4:37

for n being Nat
for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|

proof end;

theorem Th38: :: EUCLID_4:38

for n being Nat
for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|

proof end;

theorem :: EUCLID_4:39

for n being Nat
for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2 ) + (2 * |(x,y)|)) + (|.y.| ^2 )

proof end;

theorem :: EUCLID_4:40

for n being Nat
for x, y being Element of REAL n holds |.(x - y).| ^2 = ((|.x.| ^2 ) - (2 * |(x,y)|)) + (|.y.| ^2 )

proof end;

theorem :: EUCLID_4:41

for n being Nat
for x, y being Element of REAL n holds (|.(x + y).| ^2 ) + (|.(x - y).| ^2 ) = 2 * ((|.x.| ^2 ) + (|.y.| ^2 ))

proof end;

theorem :: EUCLID_4:42

for n being Nat
for x, y being Element of REAL n holds (|.(x + y).| ^2 ) - (|.(x - y).| ^2 ) = 4 * |(x,y)|

proof end;

theorem :: EUCLID_4:43

for n being Nat
for x, y being Element of REAL n holds abs |(x,y)| <= |.x.| * |.y.|

proof end;

theorem :: EUCLID_4:44

for n being Nat
for x, y being Element of REAL n holds |.(x + y).| <= |.x.| + |.y.|

proof end;

definition

let n be Nat;
let x1, x2 be Element of REAL n;
pred x1,x2 are_orthogonal means :Def6: :: EUCLID_4:def 6
|(x1,x2)| = 0;
symmetry ;

end;

:: deftheorem Def6 defines are_orthogonal EUCLID_4:def 6 :

Lm7: for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 - (x2 + x3) = (x1 - x2) - x3

proof end;

Lm8: for a being Real
for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )

proof end;

Lm9: for n being Nat
for x1, x2 being Element of REAL n holds x1 - x2 = x1 + (- x2)

proof end;

Lm10: for n being Nat
for x being Element of REAL n holds x - x = 0* n

proof end;

Lm11: for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0

proof end;

Lm12: for n being Nat
for y1, y2, x1, x2 being Element of REAL n st y1 in Line x1,x2 & y2 in Line x1,x2 holds
ex a being Real st y1 - y2 = a * (x1 - x2)

proof end;

Lm13: for n being Nat
for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line x1,x2 holds
|.(y1 - y2).| <= |.(y1 - x).| ) )

proof end;

theorem :: EUCLID_4:45

for n being Nat
for R being Subset of REAL
for x1, x2, y1 being Element of REAL n st R = { |.(y1 - x).| where x is Element of REAL n : x in Line x1,x2 } holds
ex y2 being Element of REAL n st
( y2 in Line x1,x2 & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )

proof end;

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
func Line p1,p2 -> Subset of (TOP-REAL n) equals :: EUCLID_4:def 7
{ (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ;
coherence

proof end;

end;

:: deftheorem defines Line EUCLID_4:def 7 :

registration

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
cluster Line p1,p2 -> non empty ;
coherence

proof end;

end;

Lm14: for n being Nat
for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )

proof end;

theorem Th46: :: EUCLID_4:46

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds Line p1,p2 = Line p2,p1

proof end;

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original: Line
redefine func Line p1,p2 -> Subset of (TOP-REAL n);
commutativity by Th46;

end;

theorem Th47: :: EUCLID_4:47

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds
( p1 in Line p1,p2 & p2 in Line p1,p2 )

proof end;

theorem Th48: :: EUCLID_4:48

for n being Nat
for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line p1,p2 & q2 in Line p1,p2 holds
Line q1,q2 c= Line p1,p2

proof end;

theorem Th49: :: EUCLID_4:49

for n being Nat
for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line p1,p2 & q2 in Line p1,p2 & q1 <> q2 holds
Line p1,p2 c= Line q1,q2

proof end;

definition

let n be Nat;
let A be Subset of (TOP-REAL n);
attr A is being_line means :Def8: :: EUCLID_4:def 8
ex p1, p2 being Point of (TOP-REAL n) st
( p1 <> p2 & A = Line p1,p2 );

end;

:: deftheorem Def8 defines being_line EUCLID_4:def 8 :

notation

let n be Nat;
let A be Subset of (TOP-REAL n);
synonym A is_line for being_line A;

end;

Lm15: for n being Nat
for A being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st A is_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line p1,p2

proof end;

theorem :: EUCLID_4:50

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for A, C being Subset of (TOP-REAL n) st A is_line & C is_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds
A = C

proof end;

theorem Th51: :: EUCLID_4:51

for n being Nat
for A being Subset of (TOP-REAL n) st A is_line holds
ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 )

proof end;

theorem :: EUCLID_4:52

for n being Nat
for p1 being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st A is_line holds
ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )

proof end;

definition

let n be Nat;
let p be Point of (TOP-REAL n);
func TPn2Rn p -> Element of REAL n equals :: EUCLID_4:def 9
p;
correctness by EUCLID:25;

end;

:: deftheorem defines TPn2Rn EUCLID_4:def 9 :

definition

let n be Nat;
let p be Point of (TOP-REAL n);
func |.p.| -> Real equals :: EUCLID_4:def 10
|.(TPn2Rn p).|;
correctness ;

end;

:: deftheorem defines |. EUCLID_4:def 10 :

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
func |(p1,p2)| -> Real equals :: EUCLID_4:def 11
|((TPn2Rn p1),(TPn2Rn p2))|;
correctness ;
commutativity ;

end;

:: deftheorem defines |( EUCLID_4:def 11 :

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
pred p1,p2 are_orthogonal means :Def12: :: EUCLID_4:def 12
|(p1,p2)| = 0;
symmetry ;

end;

:: deftheorem Def12 defines are_orthogonal EUCLID_4:def 12 :

theorem :: EUCLID_4:53

for n being Nat
for R being Subset of REAL
for p1, p2, q1 being Point of (TOP-REAL n) st R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line p1,p2 } holds
ex q2 being Point of (TOP-REAL n) st
( q2 in Line p1,p2 & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )

proof end;