:: EUCLID semantic presentation

definition

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

end;

:: deftheorem Def1 defines REAL EUCLID:def 1 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines absreal EUCLID:def 2 :

definition

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

end;

:: deftheorem Def3 defines abs EUCLID:def 3 :

definition

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

end;

:: deftheorem Def4 defines 0* EUCLID:def 4 :

definition

let c₁ be Nat;
redefine func 0* as 0* c₁ -> Element of REAL a₁;
coherence ;

end;

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
redefine func - as - c₂ -> Element of REAL a₁;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
redefine func + as c₂ + c₃ -> Element of REAL a₁;
coherence

proof end;

redefine func - as c₂ - c₃ -> Element of REAL a₁;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be real number ;
let c₃ be Element of REAL c₁;
redefine func * as c₂ * c₃ -> Element of REAL a₁;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
redefine func abs as abs c₂ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
redefine func sqr as sqr c₂ -> Element of a₁ -tuples_on REAL ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def5 defines |. EUCLID:def 5 :

theorem Th1: :: EUCLID:1

canceled;

theorem Th2: :: EUCLID:2

for b₁ being Nat
for b₂ being Element of REAL b₁ holds len b₂ = b₁ by FINSEQ_2:109;

theorem Th3: :: EUCLID:3

for b₁ being Nat
for b₂ being Element of REAL b₁ holds dom b₂ = Seg b₁

proof end;

theorem Th4: :: EUCLID:4

for b₁, b₂ being Nat
for b₃ being Element of REAL b₁ holds b₃ . b₂ in REAL

proof end;

theorem Th5: :: EUCLID:5

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st ( for b₄ being Nat st b₄ in Seg b₁ holds
b₂ . b₄ = b₃ . b₄ ) holds
b₂ = b₃ by FINSEQ_2:139;

Lemma6: for b₁ being Nat
for b₂ being Element of REAL b₁ holds dom (abs b₂) = dom b₂

proof end;

theorem Th6: :: EUCLID:6

for b₁, b₂ being Nat
for b₃ being real number
for b₄ being Element of REAL b₁ st b₃ = b₄ . b₂ holds
(abs b₄) . b₂ = abs b₃

proof end;

Lemma8: for b₁ being Nat
for b₂ being Element of REAL b₁ holds sqr (abs b₂) = sqr b₂

proof end;

theorem Th7: :: EUCLID:7

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

proof end;

theorem Th8: :: EUCLID:8

for b₁ being Nat
for b₂ being Element of REAL b₁ holds abs (- b₂) = abs b₂

proof end;

theorem Th9: :: EUCLID:9

for b₁ being Nat
for b₂ being real number
for b₃ being Element of REAL b₁ holds abs (b₂ * b₃) = (abs b₂) * (abs b₃)

proof end;

theorem Th10: :: EUCLID:10

for b₁ being Nat holds |.(0* b₁).| = 0

proof end;

theorem Th11: :: EUCLID:11

for b₁ being Nat
for b₂ being Element of REAL b₁ st |.b₂.| = 0 holds
b₂ = 0* b₁

proof end;

theorem Th12: :: EUCLID:12

for b₁ being Nat
for b₂ being Element of REAL b₁ holds |.b₂.| >= 0

proof end;

theorem Th13: :: EUCLID:13

for b₁ being Nat
for b₂ being Element of REAL b₁ holds |.(- b₂).| = |.b₂.|

proof end;

theorem Th14: :: EUCLID:14

for b₁ being Nat
for b₂ being real number
for b₃ being Element of REAL b₁ holds |.(b₂ * b₃).| = (abs b₂) * |.b₃.|

proof end;

theorem Th15: :: EUCLID:15

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds |.(b₂ + b₃).| <= |.b₂.| + |.b₃.|

proof end;

theorem Th16: :: EUCLID:16

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds |.(b₂ - b₃).| <= |.b₂.| + |.b₃.|

proof end;

theorem Th17: :: EUCLID:17

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds |.b₂.| - |.b₃.| <= |.(b₂ + b₃).|

proof end;

theorem Th18: :: EUCLID:18

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds |.b₂.| - |.b₃.| <= |.(b₂ - b₃).|

proof end;

theorem Th19: :: EUCLID:19

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds
( |.(b₂ - b₃).| = 0 iff b₂ = b₃ )

proof end;

theorem Th20: :: EUCLID:20

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ <> b₃ holds
|.(b₂ - b₃).| > 0

proof end;

theorem Th21: :: EUCLID:21

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds |.(b₂ - b₃).| = |.(b₃ - b₂).|

proof end;

theorem Th22: :: EUCLID:22

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds |.(b₂ - b₃).| <= |.(b₂ - b₄).| + |.(b₄ - b₃).|

proof end;

definition

let c₁ be Nat;
func Pitag_dist c₁ -> Function of [:(REAL a₁),(REAL a₁):], REAL means :Def6: :: EUCLID:def 6
for b₁, b₂ being Element of REAL a₁ holds a₂ . b₁,b₂ = |.(b₁ - b₂).|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :

theorem Th23: :: EUCLID:23

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds sqr (b₂ - b₃) = sqr (b₃ - b₂)

proof end;

theorem Th24: :: EUCLID:24

for b₁ being Nat holds Pitag_dist b₁ is_metric_of REAL b₁

proof end;

definition

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

proof end;

end;

:: deftheorem Def7 defines Euclid EUCLID:def 7 :

registration

let c₁ be Nat;
cluster Euclid a₁ -> non empty strict ;
coherence

proof end;

end;

definition

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

end;

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

registration

let c₁ be Nat;
cluster TOP-REAL a₁ -> non empty strict ;
coherence ;

end;

theorem Th25: :: EUCLID:25

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

theorem Th26: :: EUCLID:26

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds b₂ is Function of Seg b₁, REAL

proof end;

theorem Th27: :: EUCLID:27

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds b₂ is FinSequence of REAL

proof end;

theorem Th28: :: EUCLID:28

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being FinSequence st b₃ = b₂ holds
len b₃ = b₁

proof end;

definition

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

end;

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

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func c₂ + c₃ -> Point of (TOP-REAL a₁) means :Def10: :: EUCLID:def 10
for b₁, b₂ being Element of REAL a₁ st b₁ = a₂ & b₂ = a₃ holds
a₄ = b₁ + b₂;
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def10 defines + EUCLID:def 10 :

theorem Th29: :: EUCLID:29

for b₁ being Nat
for b₂ being Element of REAL b₁ holds sqr (abs b₂) = sqr b₂ by Lemma8;

theorem Th30: :: EUCLID:30

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th31: :: EUCLID:31

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( (0.REAL b₁) + b₂ = b₂ & b₂ + (0.REAL b₁) = b₂ )

proof end;

definition

let c₁ be real number ;
let c₂ be Nat;
let c₃ be Point of (TOP-REAL c₂);
func c₁ * c₃ -> Point of (TOP-REAL a₂) means :Def11: :: EUCLID:def 11
for b₁ being Element of REAL a₂ st b₁ = a₃ holds
a₄ = a₁ * b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines * EUCLID:def 11 :

theorem Th32: :: EUCLID:32

for b₁ being Nat
for b₂ being real number holds b₂ * (0.REAL b₁) = 0.REAL b₁

proof end;

theorem Th33: :: EUCLID:33

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( 1 * b₂ = b₂ & 0 * b₂ = 0.REAL b₁ )

proof end;

theorem Th34: :: EUCLID:34

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃, b₄ being real number holds (b₃ * b₄) * b₂ = b₃ * (b₄ * b₂)

proof end;

theorem Th35: :: EUCLID:35

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being real number holds
( not b₃ * b₂ = 0.REAL b₁ or b₃ = 0 or b₂ = 0.REAL b₁ )

proof end;

theorem Th36: :: EUCLID:36

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being real number holds b₄ * (b₂ + b₃) = (b₄ * b₂) + (b₄ * b₃)

proof end;

theorem Th37: :: EUCLID:37

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃, b₄ being real number holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂)

proof end;

theorem Th38: :: EUCLID:38

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being real number holds
( not b₄ * b₂ = b₄ * b₃ or b₄ = 0 or b₂ = b₃ )

proof end;

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
func - c₂ -> Point of (TOP-REAL a₁) means :Def12: :: EUCLID:def 12
for b₁ being Element of REAL a₁ st b₁ = a₂ holds
a₃ = - b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines - EUCLID:def 12 :

theorem Th39: :: EUCLID:39

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds - (- b₂) = b₂

proof end;

theorem Th40: :: EUCLID:40

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds b₂ + (- b₂) = 0.REAL b₁

proof end;

theorem Th41: :: EUCLID:41

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ + b₃ = 0.REAL b₁ holds
( b₂ = - b₃ & b₃ = - b₂ )

proof end;

theorem Th42: :: EUCLID:42

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds - (b₂ + b₃) = (- b₂) + (- b₃)

proof end;

theorem Th43: :: EUCLID:43

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds - b₂ = (- 1) * b₂

proof end;

theorem Th44: :: EUCLID:44

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being real number holds
( - (b₃ * b₂) = (- b₃) * b₂ & - (b₃ * b₂) = b₃ * (- b₂) )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func c₂ - c₃ -> Point of (TOP-REAL a₁) means :Def13: :: EUCLID:def 13
for b₁, b₂ being Element of REAL a₁ st b₁ = a₂ & b₂ = a₃ holds
a₄ = b₁ - b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines - EUCLID:def 13 :

theorem Th45: :: EUCLID:45

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th46: :: EUCLID:46

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds b₂ - b₂ = 0.REAL b₁

proof end;

theorem Th47: :: EUCLID:47

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ - b₃ = 0.REAL b₁ holds
b₂ = b₃

proof end;

theorem Th48: :: EUCLID:48

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds
( - (b₂ - b₃) = b₃ - b₂ & - (b₂ - b₃) = (- b₂) + b₃ )

proof end;

theorem Th49: :: EUCLID:49

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds b₂ + (b₃ - b₄) = (b₂ + b₃) - b₄

proof end;

theorem Th50: :: EUCLID:50

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

proof end;

theorem Th51: :: EUCLID:51

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th52: :: EUCLID:52

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds
( b₂ = (b₂ + b₃) - b₃ & b₂ = (b₂ - b₃) + b₃ )

proof end;

theorem Th53: :: EUCLID:53

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being real number holds b₄ * (b₂ - b₃) = (b₄ * b₂) - (b₄ * b₃)

proof end;

theorem Th54: :: EUCLID:54

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃, b₄ being real number holds (b₃ - b₄) * b₂ = (b₃ * b₂) - (b₄ * b₂)

proof end;

theorem Th55: :: EUCLID:55

for b₁ being Point of (TOP-REAL 2) ex b₂, b₃ being Real st b₁ = <*b₂,b₃*> by FINSEQ_2:120;

definition

let c₁ be Point of (TOP-REAL 2);
func c₁ `1 -> Real means :Def14: :: EUCLID:def 14
for b₁ being FinSequence st a₁ = b₁ holds
a₂ = b₁ . 1;
existence

proof end;

uniqueness

proof end;

func c₁ `2 -> Real means :Def15: :: EUCLID:def 15
for b₁ being FinSequence st a₁ = b₁ holds
a₂ = b₁ . 2;
existence

proof end;

uniqueness

proof end;

end;

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

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

definition

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

proof end;

end;

:: deftheorem Def16 defines |[ EUCLID:def 16 :

theorem Th56: :: EUCLID:56

for b₁, b₂ being real number holds
( |[b₁,b₂]| `1 = b₁ & |[b₁,b₂]| `2 = b₂ )

proof end;

theorem Th57: :: EUCLID:57

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

proof end;

theorem Th58: :: EUCLID:58

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

theorem Th59: :: EUCLID:59

for b₁, b₂ being Point of (TOP-REAL 2) holds b₁ + b₂ = |[((b₁ `1 ) + (b₂ `1 )),((b₁ `2 ) + (b₂ `2 ))]|

proof end;

theorem Th60: :: EUCLID:60

for b₁, b₂, b₃, b₄ being real number holds |[b₁,b₂]| + |[b₃,b₄]| = |[(b₁ + b₃),(b₂ + b₄)]|

proof end;

theorem Th61: :: EUCLID:61

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

proof end;

theorem Th62: :: EUCLID:62

for b₁, b₂, b₃ being real number holds b₁ * |[b₂,b₃]| = |[(b₁ * b₂),(b₁ * b₃)]|

proof end;

theorem Th63: :: EUCLID:63

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

proof end;

theorem Th64: :: EUCLID:64

for b₁, b₂ being real number holds - |[b₁,b₂]| = |[(- b₁),(- b₂)]|

proof end;

theorem Th65: :: EUCLID:65

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

proof end;

theorem Th66: :: EUCLID:66

for b₁, b₂, b₃, b₄ being real number holds |[b₁,b₂]| - |[b₃,b₄]| = |[(b₁ - b₃),(b₂ - b₄)]|

proof end;