:: EUCLID_4 semantic presentation

theorem Th1: :: EUCLID_4:1

for b₁ being Nat
for b₂ being Element of REAL b₁ holds
( (0 * b₂) + b₂ = b₂ & b₂ + (0* b₁) = b₂ )

proof end;

theorem Th2: :: EUCLID_4:2

for b₁ being Real
for b₂ being Nat holds b₁ * (0* b₂) = 0* b₂

proof end;

theorem Th3: :: EUCLID_4:3

for b₁ being Nat
for b₂ being Element of REAL b₁ holds
( 1 * b₂ = b₂ & 0 * b₂ = 0* b₁ )

proof end;

theorem Th4: :: EUCLID_4:4

for b₁, b₂ being Real
for b₃ being Nat
for b₄ being Element of REAL b₃ holds (b₁ * b₂) * b₄ = b₁ * (b₂ * b₄)

proof end;

theorem Th5: :: EUCLID_4:5

for b₁ being Real
for b₂ being Nat
for b₃ being Element of REAL b₂ holds
( not b₁ * b₃ = 0* b₂ or b₁ = 0 or b₃ = 0* b₂ )

proof end;

theorem Th6: :: EUCLID_4:6

for b₁ being Real
for b₂ being Nat
for b₃, b₄ being Element of REAL b₂ holds b₁ * (b₃ + b₄) = (b₁ * b₃) + (b₁ * b₄)

proof end;

theorem Th7: :: EUCLID_4:7

for b₁, b₂ being Real
for b₃ being Nat
for b₄ being Element of REAL b₃ holds (b₁ + b₂) * b₄ = (b₁ * b₄) + (b₂ * b₄)

proof end;

theorem Th8: :: EUCLID_4:8

for b₁ being Real
for b₂ being Nat
for b₃, b₄ being Element of REAL b₂ holds
( not b₁ * b₃ = b₁ * b₄ or b₁ = 0 or b₃ = b₄ )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
func Line c₂,c₃ -> Subset of (REAL a₁) equals :: EUCLID_4:def 1
{ (((1 - b₁) * a₂) + (b₁ * a₃)) where B is Real : verum } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Line EUCLID_4:def 1 :

registration

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
cluster Line a₂,a₃ -> non empty ;
coherence

proof end;

end;

Lemma7: for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds Line b₂,b₃ c= Line b₃,b₂

proof end;

theorem Th9: :: EUCLID_4:9

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds Line b₂,b₃ = Line b₃,b₂

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
redefine func Line as Line c₂,c₃ -> Subset of (REAL a₁);
commutativity by Th9;

end;

theorem Th10: :: EUCLID_4:10

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds
( b₂ in Line b₂,b₃ & b₃ in Line b₂,b₃ )

proof end;

Lemma10: for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄

proof end;

theorem Th11: :: EUCLID_4:11

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁ st b₂ in Line b₃,b₄ & b₅ in Line b₃,b₄ holds
Line b₂,b₅ c= Line b₃,b₄

proof end;

theorem Th12: :: EUCLID_4:12

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁ st b₂ in Line b₃,b₄ & b₅ in Line b₃,b₄ & b₂ <> b₅ holds
Line b₃,b₄ c= Line b₂,b₅

proof end;

definition

let c₁ be Nat;
let c₂ be Subset of (REAL c₁);
attr a₂ is being_line means :Def2: :: EUCLID_4:def 2
ex b₁, b₂ being Element of REAL a₁ st
( b₁ <> b₂ & a₂ = Line b₁,b₂ );

end;

:: deftheorem Def2 defines being_line EUCLID_4:def 2 :

notation

let c₁ be Nat;
let c₂ be Subset of (REAL c₁);
synonym c₂ is_line for being_line c₂;

end;

Lemma14: for b₁ being Nat
for b₂ being Subset of (REAL b₁)
for b₃, b₄ being Element of REAL b₁ st b₂ is_line & b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ holds
b₂ = Line b₃,b₄

proof end;

theorem Th13: :: EUCLID_4:13

for b₁ being Nat
for b₂, b₃ being Subset of (REAL b₁)
for b₄, b₅ being Element of REAL b₁ st b₂ is_line & b₃ is_line & b₄ in b₂ & b₅ in b₂ & b₄ in b₃ & b₅ in b₃ & not b₄ = b₅ holds
b₂ = b₃

proof end;

theorem Th14: :: EUCLID_4:14

for b₁ being Nat
for b₂ being Subset of (REAL b₁) st b₂ is_line holds
ex b₃, b₄ being Element of REAL b₁ st
( b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ )

proof end;

theorem Th15: :: EUCLID_4:15

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Subset of (REAL b₁) st b₃ is_line holds
ex b₄ being Element of REAL b₁ st
( b₂ <> b₄ & b₄ in b₃ )

proof end;

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
func Rn2Fin c₂ -> FinSequence of REAL equals :: EUCLID_4:def 3
a₂;
correctness

proof end;

end;

:: deftheorem Def3 defines Rn2Fin EUCLID_4:def 3 :

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
func |.c₂.| -> Real equals :: EUCLID_4:def 4
|.(Rn2Fin a₂).|;
correctness ;

end;

:: deftheorem Def4 defines |. EUCLID_4:def 4 :

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
func |(c₂,c₃)| -> Real equals :: EUCLID_4:def 5
|((Rn2Fin a₂),(Rn2Fin a₃))|;
correctness by XREAL_0:def 1;
commutativity ;

end;

:: deftheorem Def5 defines |( EUCLID_4:def 5 :

theorem Th16: :: EUCLID_4:16

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds |(b₂,b₃)| = (1 / 4) * ((|.(b₂ + b₃).| ^2 ) - (|.(b₂ - b₃).| ^2 )) by EUCLID_2:10;

theorem Th17: :: EUCLID_4:17

for b₁ being Nat
for b₂ being Element of REAL b₁ holds |(b₂,b₂)| >= 0 by EUCLID_2:11;

theorem Th18: :: EUCLID_4:18

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

theorem Th19: :: EUCLID_4:19

for b₁ being Nat
for b₂ being Element of REAL b₁ holds 0 <= |.b₂.| by EUCLID_2:14;

theorem Th20: :: EUCLID_4:20

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

proof end;

theorem Th21: :: EUCLID_4:21

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

proof end;

Lemma20: for b₁ being Nat
for b₂ being Element of REAL b₁ holds b₂ - (0* b₁) = b₂

proof end;

Lemma21: for b₁ being Nat
for b₂ being Element of REAL b₁ holds (0* b₁) - b₂ = - b₂

proof end;

theorem Th22: :: EUCLID_4:22

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

proof end;

theorem Th23: :: EUCLID_4:23

for b₁ being Nat
for b₂ being Element of REAL b₁ holds |(b₂,(0* b₁))| = 0

proof end;

theorem Th24: :: EUCLID_4:24

for b₁ being Nat
for b₂ being Element of REAL b₁ holds |((0* b₁),b₂)| = 0 by Th23;

Lemma24: for b₁ being Nat
for b₂ being Element of REAL b₁ holds len (Rn2Fin b₂) = b₁
by EUCLID:2;

theorem Th25: :: EUCLID_4:25

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

proof end;

theorem Th26: :: EUCLID_4:26

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

proof end;

theorem Th27: :: EUCLID_4:27

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁
for b₄ being real number holds |(b₂,(b₄ * b₃))| = b₄ * |(b₂,b₃)| by Th26;

theorem Th28: :: EUCLID_4:28

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

proof end;

theorem Th29: :: EUCLID_4:29

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

theorem Th30: :: EUCLID_4:30

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

proof end;

theorem Th31: :: EUCLID_4:31

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

proof end;

theorem Th32: :: EUCLID_4:32

for b₁ being Nat
for b₂, b₃ being real number
for b₄, b₅, b₆ being Element of REAL b₁ holds |(((b₂ * b₄) + (b₃ * b₅)),b₆)| = (b₂ * |(b₄,b₆)|) + (b₃ * |(b₅,b₆)|)

proof end;

theorem Th33: :: EUCLID_4:33

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds |(b₂,(b₃ + b₄))| = |(b₂,b₃)| + |(b₂,b₄)| by Th25;

theorem Th34: :: EUCLID_4:34

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds |(b₂,(b₃ - b₄))| = |(b₂,b₃)| - |(b₂,b₄)| by Th31;

theorem Th35: :: EUCLID_4:35

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

proof end;

theorem Th36: :: EUCLID_4:36

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

proof end;

theorem Th37: :: EUCLID_4:37

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

proof end;

theorem Th38: :: EUCLID_4:38

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

proof end;

theorem Th39: :: EUCLID_4:39

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

proof end;

theorem Th40: :: EUCLID_4:40

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

proof end;

theorem Th41: :: EUCLID_4:41

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

proof end;

theorem Th42: :: EUCLID_4:42

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds (|.(b₂ + b₃).| ^2 ) - (|.(b₂ - b₃).| ^2 ) = 4 * |(b₂,b₃)|

proof end;

theorem Th43: :: EUCLID_4:43

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

proof end;

theorem Th44: :: EUCLID_4:44

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

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
pred c₂,c₃ are_orthogonal means :Def6: :: EUCLID_4:def 6
|(a₂,a₃)| = 0;
symmetry ;

end;

:: deftheorem Def6 defines are_orthogonal EUCLID_4:def 6 :

Lemma34: for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

proof end;

Lemma35: for b₁ being Real
for b₂ being Nat
for b₃ being Element of REAL b₂ holds
( - (b₁ * b₃) = (- b₁) * b₃ & - (b₁ * b₃) = b₁ * (- b₃) )

proof end;

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

proof end;

Lemma37: for b₁ being Nat
for b₂ being Element of REAL b₁ holds b₂ - b₂ = 0* b₁

proof end;

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

proof end;

Lemma39: for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁ st b₂ in Line b₄,b₅ & b₃ in Line b₄,b₅ holds
ex b₆ being Real st b₂ - b₃ = b₆ * (b₄ - b₅)

proof end;

Lemma40: for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ ex b₅ being Element of REAL b₁ st
( b₅ in Line b₂,b₃ & b₂ - b₃,b₄ - b₅ are_orthogonal & ( for b₆ being Element of REAL b₁ st b₆ in Line b₂,b₃ holds
|.(b₄ - b₅).| <= |.(b₄ - b₆).| ) )

proof end;

theorem Th45: :: EUCLID_4:45

for b₁ being Nat
for b₂ being Subset of REAL
for b₃, b₄, b₅ being Element of REAL b₁ st b₂ = { |.(b₅ - b₆).| where B is Element of REAL b₁ : b₆ in Line b₃,b₄ } holds
ex b₆ being Element of REAL b₁ st
( b₆ in Line b₃,b₄ & |.(b₅ - b₆).| = lower_bound b₂ & b₃ - b₄,b₅ - b₆ are_orthogonal )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func Line c₂,c₃ -> Subset of (TOP-REAL a₁) equals :: EUCLID_4:def 7
{ (((1 - b₁) * a₂) + (b₁ * a₃)) where B is Real : verum } ;
coherence

proof end;

end;

:: deftheorem Def7 defines Line EUCLID_4:def 7 :

registration

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
cluster Line a₂,a₃ -> non empty ;
coherence

proof end;

end;

Lemma41: for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) ex b₄, b₅ being Element of REAL b₁ st
( b₂ = b₄ & b₃ = b₅ & Line b₄,b₅ = Line b₂,b₃ )

proof end;

theorem Th46: :: EUCLID_4:46

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

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
redefine func Line as Line c₂,c₃ -> Subset of (TOP-REAL a₁);
commutativity by Th46;

end;

theorem Th47: :: EUCLID_4:47

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

proof end;

theorem Th48: :: EUCLID_4:48

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₂ in Line b₃,b₄ & b₅ in Line b₃,b₄ holds
Line b₂,b₅ c= Line b₃,b₄

proof end;

theorem Th49: :: EUCLID_4:49

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₂ in Line b₃,b₄ & b₅ in Line b₃,b₄ & b₂ <> b₅ holds
Line b₃,b₄ c= Line b₂,b₅

proof end;

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
attr a₂ is being_line means :Def8: :: EUCLID_4:def 8
ex b₁, b₂ being Point of (TOP-REAL a₁) st
( b₁ <> b₂ & a₂ = Line b₁,b₂ );

end;

:: deftheorem Def8 defines being_line EUCLID_4:def 8 :

notation

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
synonym c₂ is_line for being_line c₂;

end;

Lemma47: for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₂ is_line & b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ holds
b₂ = Line b₃,b₄

proof end;

theorem Th50: :: EUCLID_4:50

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being Subset of (TOP-REAL b₁) st b₄ is_line & b₅ is_line & b₂ in b₄ & b₃ in b₄ & b₂ in b₅ & b₃ in b₅ & not b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th51: :: EUCLID_4:51

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ is_line holds
ex b₃, b₄ being Point of (TOP-REAL b₁) st
( b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ )

proof end;

theorem Th52: :: EUCLID_4:52

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) st b₃ is_line holds
ex b₄ being Point of (TOP-REAL b₁) st
( b₂ <> b₄ & b₄ in b₃ )

proof end;

definition

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

end;

:: deftheorem Def9 defines TPn2Rn EUCLID_4:def 9 :

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
func |.c₂.| -> Real equals :: EUCLID_4:def 10
|.(TPn2Rn a₂).|;
correctness ;

end;

:: deftheorem Def10 defines |. EUCLID_4:def 10 :

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func |(c₂,c₃)| -> Real equals :: EUCLID_4:def 11
|((TPn2Rn a₂),(TPn2Rn a₃))|;
correctness ;
commutativity ;

end;

:: deftheorem Def11 defines |( EUCLID_4:def 11 :

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
pred c₂,c₃ are_orthogonal means :Def12: :: EUCLID_4:def 12
|(a₂,a₃)| = 0;
symmetry ;

end;

:: deftheorem Def12 defines are_orthogonal EUCLID_4:def 12 :

theorem Th53: :: EUCLID_4:53

for b₁ being Nat
for b₂ being Subset of REAL
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₂ = { |.(b₅ - b₆).| where B is Point of (TOP-REAL b₁) : b₆ in Line b₃,b₄ } holds
ex b₆ being Point of (TOP-REAL b₁) st
( b₆ in Line b₃,b₄ & |.(b₅ - b₆).| = lower_bound b₂ & b₃ - b₄,b₅ - b₆ are_orthogonal )

proof end;