:: EUCLID semantic presentation

definition

let n be Nat;
func REAL n -> FinSequence-DOMAIN of REAL equals :: EUCLID:def 1
n -tuples_on REAL ;
coherence ;

end;

:: deftheorem defines REAL EUCLID:def 1 :

definition

func absreal -> Function of REAL , REAL means :Def2: :: EUCLID:def 2
for r being real number holds it . r = abs r;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines absreal EUCLID:def 2 :

definition

let x be FinSequence of REAL ;
func abs x -> FinSequence of REAL equals :: EUCLID:def 3
absreal * x;
coherence ;

end;

:: deftheorem defines abs EUCLID:def 3 :

definition

let n be Nat;
func 0* n -> FinSequence of REAL equals :: EUCLID:def 4
n |-> 0;
coherence ;

end;

:: deftheorem defines 0* EUCLID:def 4 :

definition

let n be Nat;
:: original: 0*
redefine func 0* n -> Element of REAL n;
coherence ;

end;

definition

let n be Nat;
let x be Element of REAL n;
:: original: -
redefine func - x -> Element of REAL n;
coherence

proof end;

end;

definition

let n be Nat;
let x, y be Element of REAL n;
:: original: +
redefine func x + y -> Element of REAL n;
coherence

proof end;

:: original: -
redefine func x - y -> Element of REAL n;
coherence

proof end;

end;

definition

let n be Nat;
let r be real number ;
let x be Element of REAL n;
:: original: *
redefine func r * x -> Element of REAL n;
coherence

proof end;

end;

definition

let n be Nat;
let x be Element of REAL n;
:: original: abs
redefine func abs x -> Element of n -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

definition

let n be Nat;
let x be Element of REAL n;
:: original: sqr
redefine func sqr x -> Element of n -tuples_on REAL ;
coherence

proof end;

end;

definition

let x be FinSequence of REAL ;
func |.x.| -> Real equals :: EUCLID:def 5
sqrt (Sum (sqr x));
coherence ;

end;

:: deftheorem defines |. EUCLID:def 5 :

theorem :: EUCLID:1

canceled;

theorem Th2: :: EUCLID:2

for n being Nat
for x being Element of REAL n holds len x = n by FINSEQ_2:109;

theorem Th3: :: EUCLID:3

for n being Nat
for x being Element of REAL n holds dom x = Seg n

proof end;

theorem Th4: :: EUCLID:4

for n, k being Nat
for x being Element of REAL n holds x . k in REAL

proof end;

theorem Th5: :: EUCLID:5

for n being Nat
for x1, x2 being Element of REAL n st ( for k being Nat st k in Seg n holds
x1 . k = x2 . k ) holds
x1 = x2 by FINSEQ_2:139;

Lm1: for n being Nat
for x being Element of REAL n holds dom (abs x) = dom x

proof end;

theorem Th6: :: EUCLID:6

for n, k being Nat
for r being real number
for x being Element of REAL n st r = x . k holds
(abs x) . k = abs r

proof end;

Lm2: for n being Nat
for x being Element of REAL n holds sqr (abs x) = sqr x

proof end;

theorem :: EUCLID:7

for n being Nat holds abs (0* n) = n |-> 0

proof end;

theorem Th8: :: EUCLID:8

for n being Nat
for x being Element of REAL n holds abs (- x) = abs x

proof end;

theorem Th9: :: EUCLID:9

for n being Nat
for r being real number
for x being Element of REAL n holds abs (r * x) = (abs r) * (abs x)

proof end;

theorem Th10: :: EUCLID:10

for n being Nat holds |.(0* n).| = 0

proof end;

theorem Th11: :: EUCLID:11

for n being Nat
for x being Element of REAL n st |.x.| = 0 holds
x = 0* n

proof end;

theorem Th12: :: EUCLID:12

for n being Nat
for x being Element of REAL n holds |.x.| >= 0

proof end;

theorem Th13: :: EUCLID:13

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

proof end;

theorem Th14: :: EUCLID:14

for n being Nat
for r being real number
for x being Element of REAL n holds |.(r * x).| = (abs r) * |.x.|

proof end;

theorem Th15: :: EUCLID:15

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

proof end;

theorem Th16: :: EUCLID:16

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

proof end;

theorem :: EUCLID:17

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

proof end;

theorem :: EUCLID:18

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

proof end;

theorem Th19: :: EUCLID:19

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

proof end;

theorem :: EUCLID:20

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

proof end;

theorem Th21: :: EUCLID:21

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

proof end;

theorem Th22: :: EUCLID:22

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

proof end;

definition

let n be Nat;
func Pitag_dist n -> Function of [:(REAL n),(REAL n):], REAL means :Def6: :: EUCLID:def 6
for x, y being Element of REAL n holds it . x,y = |.(x - y).|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :

theorem :: EUCLID:23

for n being Nat
for x, y being Element of REAL n holds sqr (x - y) = sqr (y - x)

proof end;

theorem Th24: :: EUCLID:24

for n being Nat holds Pitag_dist n is_metric_of REAL n

proof end;

definition

let n be Nat;
func Euclid n -> strict MetrSpace equals :: EUCLID:def 7
MetrStruct(# (REAL n),(Pitag_dist n) #);
coherence

proof end;

end;

:: deftheorem defines Euclid EUCLID:def 7 :

registration

let n be Nat;
cluster Euclid n -> non empty strict ;
coherence

proof end;

end;

definition

let n be Nat;
func TOP-REAL n -> strict TopSpace equals :: EUCLID:def 8
TopSpaceMetr (Euclid n);
coherence ;

end;

:: deftheorem defines TOP-REAL EUCLID:def 8 :

registration

let n be Nat;
cluster TOP-REAL n -> non empty strict ;
coherence ;

end;

theorem :: EUCLID:25

for n being Nat holds the carrier of (TOP-REAL n) = REAL n ;

theorem Th26: :: EUCLID:26

for n being Nat
for p being Point of (TOP-REAL n) holds p is Function of Seg n, REAL

proof end;

theorem Th27: :: EUCLID:27

for n being Nat
for p being Point of (TOP-REAL n) holds p is FinSequence of REAL

proof end;

theorem Th28: :: EUCLID:28

for n being Nat
for p being Point of (TOP-REAL n)
for f being FinSequence st f = p holds
len f = n

proof end;

definition

let n be Nat;
func 0.REAL n -> Point of (TOP-REAL n) equals :: EUCLID:def 9
0* n;
coherence ;

end;

:: deftheorem defines 0.REAL EUCLID:def 9 :

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
func p1 + p2 -> Point of (TOP-REAL n) means :Def10: :: EUCLID:def 10
for p1', p2' being Element of REAL n st p1' = p1 & p2' = p2 holds
it = p1' + p2';
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def10 defines + EUCLID:def 10 :

theorem :: EUCLID:29

for n being Nat
for x being Element of REAL n holds sqr (abs x) = sqr x by Lm2;

theorem Th30: :: EUCLID:30

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

proof end;

theorem Th31: :: EUCLID:31

for n being Nat
for p being Point of (TOP-REAL n) holds
( (0.REAL n) + p = p & p + (0.REAL n) = p )

proof end;

definition

let x be real number ;
let n be Nat;
let p be Point of (TOP-REAL n);
func x * p -> Point of (TOP-REAL n) means :Def11: :: EUCLID:def 11
for p' being Element of REAL n st p' = p holds
it = x * p';
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines * EUCLID:def 11 :

theorem Th32: :: EUCLID:32

for n being Nat
for x being real number holds x * (0.REAL n) = 0.REAL n

proof end;

theorem Th33: :: EUCLID:33

for n being Nat
for p being Point of (TOP-REAL n) holds
( 1 * p = p & 0 * p = 0.REAL n )

proof end;

theorem Th34: :: EUCLID:34

for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x * y) * p = x * (y * p)

proof end;

theorem :: EUCLID:35

for n being Nat
for p being Point of (TOP-REAL n)
for x being real number holds
( not x * p = 0.REAL n or x = 0 or p = 0.REAL n )

proof end;

theorem Th36: :: EUCLID:36

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds x * (p1 + p2) = (x * p1) + (x * p2)

proof end;

theorem Th37: :: EUCLID:37

for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x + y) * p = (x * p) + (y * p)

proof end;

theorem :: EUCLID:38

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds
( not x * p1 = x * p2 or x = 0 or p1 = p2 )

proof end;

definition

let n be Nat;
let p be Point of (TOP-REAL n);
func - p -> Point of (TOP-REAL n) means :Def12: :: EUCLID:def 12
for p' being Element of REAL n st p' = p holds
it = - p';
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines - EUCLID:def 12 :

theorem Th39: :: EUCLID:39

for n being Nat
for p being Point of (TOP-REAL n) holds - (- p) = p

proof end;

theorem :: EUCLID:40

for n being Nat
for p being Point of (TOP-REAL n) holds p + (- p) = 0.REAL n

proof end;

theorem :: EUCLID:41

for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 + p2 = 0.REAL n holds
( p1 = - p2 & p2 = - p1 )

proof end;

theorem Th42: :: EUCLID:42

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

proof end;

theorem Th43: :: EUCLID:43

for n being Nat
for p being Point of (TOP-REAL n) holds - p = (- 1) * p

proof end;

theorem Th44: :: EUCLID:44

for n being Nat
for p being Point of (TOP-REAL n)
for x being real number holds
( - (x * p) = (- x) * p & - (x * p) = x * (- p) )

proof end;

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
func p1 - p2 -> Point of (TOP-REAL n) means :Def13: :: EUCLID:def 13
for p1', p2' being Element of REAL n st p1' = p1 & p2' = p2 holds
it = p1' - p2';
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines - EUCLID:def 13 :

theorem Th45: :: EUCLID:45

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

proof end;

theorem Th46: :: EUCLID:46

for n being Nat
for p being Point of (TOP-REAL n) holds p - p = 0.REAL n

proof end;

theorem :: EUCLID:47

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

proof end;

theorem :: EUCLID:48

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

proof end;

theorem Th49: :: EUCLID:49

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

proof end;

theorem Th50: :: EUCLID:50

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

proof end;

theorem :: EUCLID:51

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

proof end;

theorem :: EUCLID:52

for n being Nat
for p, p1 being Point of (TOP-REAL n) holds
( p = (p + p1) - p1 & p = (p - p1) + p1 )

proof end;

theorem :: EUCLID:53

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds x * (p1 - p2) = (x * p1) - (x * p2)

proof end;

theorem :: EUCLID:54

for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x - y) * p = (x * p) - (y * p)

proof end;

theorem Th55: :: EUCLID:55

for p being Point of (TOP-REAL 2) ex x, y being Real st p = <*x,y*> by FINSEQ_2:120;

definition

let p be Point of (TOP-REAL 2);
func p `1 -> Real means :Def14: :: EUCLID:def 14
for f being FinSequence st p = f holds
it = f . 1;
existence

proof end;

uniqueness

proof end;

func p `2 -> Real means :Def15: :: EUCLID:def 15
for f being FinSequence st p = f holds
it = f . 2;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines `1 EUCLID:def 14 :

:: deftheorem Def15 defines `2 EUCLID:def 15 :

definition

let x, y be real number ;
func |[x,y]| -> Point of (TOP-REAL 2) equals :: EUCLID:def 16
<*x,y*>;
coherence

proof end;

end;

:: deftheorem defines |[ EUCLID:def 16 :

theorem Th56: :: EUCLID:56

for x, y being real number holds
( |[x,y]| `1 = x & |[x,y]| `2 = y )

proof end;

theorem Th57: :: EUCLID:57

for p being Point of (TOP-REAL 2) holds p = |[(p `1 ),(p `2 )]|

proof end;

theorem :: EUCLID:58

0.REAL 2 = |[0,0]| by FINSEQ_2:75;

theorem Th59: :: EUCLID:59

for p1, p2 being Point of (TOP-REAL 2) holds p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 ))]|

proof end;

theorem :: EUCLID:60

for x1, y1, x2, y2 being real number holds |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]|

proof end;

theorem Th61: :: EUCLID:61

for x being real number
for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1 )),(x * (p `2 ))]|

proof end;

theorem :: EUCLID:62

for x, x1, y1 being real number holds x * |[x1,y1]| = |[(x * x1),(x * y1)]|

proof end;

theorem Th63: :: EUCLID:63

for p being Point of (TOP-REAL 2) holds - p = |[(- (p `1 )),(- (p `2 ))]|

proof end;

theorem :: EUCLID:64

for x1, y1 being real number holds - |[x1,y1]| = |[(- x1),(- y1)]|

proof end;

theorem Th65: :: EUCLID:65

for p1, p2 being Point of (TOP-REAL 2) holds p1 - p2 = |[((p1 `1 ) - (p2 `1 )),((p1 `2 ) - (p2 `2 ))]|

proof end;

theorem :: EUCLID:66

for x1, y1, x2, y2 being real number holds |[x1,y1]| - |[x2,y2]| = |[(x1 - x2),(y1 - y2)]|

proof end;