:: EUCLID_2 semantic presentation

theorem Th1: :: EUCLID_2:1

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL
for b₃ being Nat st b₃ in Seg b₁ holds
(mlt b₂,(0* b₁)) . b₃ = 0

proof end;

theorem Th2: :: EUCLID_2:2

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

proof end;

theorem Th3: :: EUCLID_2:3

for b₁ being FinSequence of REAL holds (- 1) * b₁ = - b₁

proof end;

theorem Th4: :: EUCLID_2:4

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
b₁ - b₂ = b₁ + (- b₂)

proof end;

theorem Th5: :: EUCLID_2:5

for b₁ being FinSequence of REAL holds len (- b₁) = len b₁

proof end;

theorem Th6: :: EUCLID_2:6

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
len (b₁ + b₂) = len b₁

proof end;

theorem Th7: :: EUCLID_2:7

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
len (b₁ - b₂) = len b₁

proof end;

theorem Th8: :: EUCLID_2:8

for b₁ being real number
for b₂ being FinSequence of REAL holds len (b₁ * b₂) = len b₂

proof end;

theorem Th9: :: EUCLID_2:9

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ holds
mlt (b₁ + b₂),b₃ = (mlt b₁,b₃) + (mlt b₂,b₃)

proof end;

definition

let c₁, c₂ be FinSequence of REAL ;
func |(c₁,c₂)| -> real number equals :: EUCLID_2:def 1
Sum (mlt a₁,a₂);
correctness ;
commutativity ;

end;

:: deftheorem Def1 defines |( EUCLID_2:def 1 :

theorem Th10: :: EUCLID_2:10

for b₁ being Nat
for b₂, b₃ being FinSequence of REAL
for b₄, b₅ being Element of REAL b₁ st b₄ = b₂ & b₅ = b₃ holds
|(b₂,b₃)| = (1 / 4) * ((|.(b₄ + b₅).| ^2 ) - (|.(b₄ - b₅).| ^2 ))

proof end;

theorem Th11: :: EUCLID_2:11

for b₁ being FinSequence of REAL holds |(b₁,b₁)| >= 0

proof end;

theorem Th12: :: EUCLID_2:12

for b₁ being FinSequence of REAL holds |.b₁.| ^2 = |(b₁,b₁)|

proof end;

theorem Th13: :: EUCLID_2:13

for b₁ being FinSequence of REAL holds |.b₁.| = sqrt |(b₁,b₁)|

proof end;

theorem Th14: :: EUCLID_2:14

for b₁ being FinSequence of REAL holds 0 <= |.b₁.|

proof end;

theorem Th15: :: EUCLID_2:15

for b₁ being FinSequence of REAL holds
( |(b₁,b₁)| = 0 iff b₁ = 0* (len b₁) )

proof end;

theorem Th16: :: EUCLID_2:16

for b₁ being FinSequence of REAL holds
( |(b₁,b₁)| = 0 iff |.b₁.| = 0 )

proof end;

theorem Th17: :: EUCLID_2:17

for b₁ being FinSequence of REAL holds |(b₁,(0* (len b₁)))| = 0

proof end;

theorem Th18: :: EUCLID_2:18

for b₁ being FinSequence of REAL holds |((0* (len b₁)),b₁)| = 0 by Th17;

theorem Th19: :: EUCLID_2:19

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ holds
|((b₁ + b₂),b₃)| = |(b₁,b₃)| + |(b₂,b₃)|

proof end;

theorem Th20: :: EUCLID_2:20

for b₁, b₂ being FinSequence of REAL
for b₃ being real number st len b₁ = len b₂ holds
|((b₃ * b₁),b₂)| = b₃ * |(b₁,b₂)|

proof end;

theorem Th21: :: EUCLID_2:21

for b₁, b₂ being FinSequence of REAL
for b₃ being real number st len b₁ = len b₂ holds
|(b₁,(b₃ * b₂))| = b₃ * |(b₁,b₂)|

proof end;

theorem Th22: :: EUCLID_2:22

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|((- b₁),b₂)| = - |(b₁,b₂)|

proof end;

theorem Th23: :: EUCLID_2:23

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|(b₁,(- b₂))| = - |(b₁,b₂)| by Th22;

theorem Th24: :: EUCLID_2:24

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|((- b₁),(- b₂))| = |(b₁,b₂)|

proof end;

theorem Th25: :: EUCLID_2:25

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ holds
|((b₁ - b₂),b₃)| = |(b₁,b₃)| - |(b₂,b₃)|

proof end;

theorem Th26: :: EUCLID_2:26

for b₁, b₂ being real number
for b₃, b₄, b₅ being FinSequence of REAL st len b₃ = len b₄ & len b₄ = len b₅ holds
|(((b₁ * b₃) + (b₂ * b₄)),b₅)| = (b₁ * |(b₃,b₅)|) + (b₂ * |(b₄,b₅)|)

proof end;

theorem Th27: :: EUCLID_2:27

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ holds
|(b₁,(b₂ + b₃))| = |(b₁,b₂)| + |(b₁,b₃)| by Th19;

theorem Th28: :: EUCLID_2:28

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ holds
|(b₁,(b₂ - b₃))| = |(b₁,b₂)| - |(b₁,b₃)| by Th25;

theorem Th29: :: EUCLID_2:29

for b₁, b₂, b₃, b₄ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ & len b₃ = len b₄ holds
|((b₁ + b₂),(b₃ + b₄))| = ((|(b₁,b₃)| + |(b₁,b₄)|) + |(b₂,b₃)|) + |(b₂,b₄)|

proof end;

theorem Th30: :: EUCLID_2:30

for b₁, b₂, b₃, b₄ being FinSequence of REAL st len b₁ = len b₂ & len b₂ = len b₃ & len b₃ = len b₄ holds
|((b₁ - b₂),(b₃ - b₄))| = ((|(b₁,b₃)| - |(b₁,b₄)|) - |(b₂,b₃)|) + |(b₂,b₄)|

proof end;

theorem Th31: :: EUCLID_2:31

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|((b₁ + b₂),(b₁ + b₂))| = (|(b₁,b₁)| + (2 * |(b₁,b₂)|)) + |(b₂,b₂)|

proof end;

theorem Th32: :: EUCLID_2:32

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|((b₁ - b₂),(b₁ - b₂))| = (|(b₁,b₁)| - (2 * |(b₁,b₂)|)) + |(b₂,b₂)|

proof end;

theorem Th33: :: EUCLID_2:33

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|.(b₁ + b₂).| ^2 = ((|.b₁.| ^2 ) + (2 * |(b₂,b₁)|)) + (|.b₂.| ^2 )

proof end;

theorem Th34: :: EUCLID_2:34

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|.(b₁ - b₂).| ^2 = ((|.b₁.| ^2 ) - (2 * |(b₂,b₁)|)) + (|.b₂.| ^2 )

proof end;

theorem Th35: :: EUCLID_2:35

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
(|.(b₁ + b₂).| ^2 ) + (|.(b₁ - b₂).| ^2 ) = 2 * ((|.b₁.| ^2 ) + (|.b₂.| ^2 ))

proof end;

theorem Th36: :: EUCLID_2:36

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
(|.(b₁ + b₂).| ^2 ) - (|.(b₁ - b₂).| ^2 ) = 4 * |(b₁,b₂)|

proof end;

theorem Th37: :: EUCLID_2:37

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
abs |(b₁,b₂)| <= |.b₁.| * |.b₂.|

proof end;

theorem Th38: :: EUCLID_2:38

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
|.(b₁ + b₂).| <= |.b₁.| + |.b₂.|

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func |(c₂,c₃)| -> real number means :Def2: :: EUCLID_2:def 2
ex b₁, b₂ being FinSequence of REAL st
( b₁ = a₂ & b₂ = a₃ & a₄ = |(b₁,b₂)| );
existence

proof end;

uniqueness ;
commutativity ;

end;

:: deftheorem Def2 defines |( EUCLID_2:def 2 :

theorem Th39: :: EUCLID_2:39

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

proof end;

theorem Th40: :: EUCLID_2:40

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

proof end;

theorem Th41: :: EUCLID_2:41

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

proof end;

theorem Th42: :: EUCLID_2:42

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₃)| by Th41;

theorem Th43: :: EUCLID_2:43

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

proof end;

theorem Th44: :: EUCLID_2:44

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds |(b₂,(- b₃))| = - |(b₂,b₃)| by Th43;

theorem Th45: :: EUCLID_2:45

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

proof end;

theorem Th46: :: EUCLID_2:46

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

proof end;

theorem Th47: :: EUCLID_2:47

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

proof end;

theorem Th48: :: EUCLID_2:48

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

theorem Th49: :: EUCLID_2:49

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds |(b₂,(b₃ - b₄))| = |(b₂,b₃)| - |(b₂,b₄)| by Th46;

theorem Th50: :: EUCLID_2:50

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

proof end;

theorem Th51: :: EUCLID_2:51

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

proof end;

theorem Th52: :: EUCLID_2:52

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

proof end;

theorem Th53: :: EUCLID_2:53

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

proof end;

theorem Th54: :: EUCLID_2:54

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

proof end;

theorem Th55: :: EUCLID_2:55

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds |((0.REAL b₁),b₂)| = 0 by Th54;

theorem Th56: :: EUCLID_2:56

for b₁ being Nat holds |((0.REAL b₁),(0.REAL b₁))| = 0 by Th54;

theorem Th57: :: EUCLID_2:57

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

proof end;

theorem Th58: :: EUCLID_2:58

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds |(b₂,b₂)| = |.b₂.| ^2

proof end;

theorem Th59: :: EUCLID_2:59

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

proof end;

theorem Th60: :: EUCLID_2:60

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

proof end;

theorem Th61: :: EUCLID_2:61

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

proof end;

theorem Th62: :: EUCLID_2:62

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

proof end;

theorem Th63: :: EUCLID_2:63

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

proof end;

theorem Th64: :: EUCLID_2:64

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( |.b₂.| = 0 iff b₂ = 0.REAL b₁ ) by Th61, TOPRNS_1:25;

theorem Th65: :: EUCLID_2:65

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( b₂ <> 0.REAL b₁ iff |(b₂,b₂)| > 0 )

proof end;

theorem Th66: :: EUCLID_2:66

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( b₂ <> 0.REAL b₁ iff |.b₂.| > 0 )

proof end;

theorem Th67: :: EUCLID_2:67

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

proof end;

theorem Th68: :: EUCLID_2:68

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

proof end;

theorem Th69: :: EUCLID_2:69

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

proof end;

theorem Th70: :: EUCLID_2:70

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

proof end;

theorem Th71: :: EUCLID_2:71

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

proof end;

theorem Th72: :: EUCLID_2:72

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

proof end;

theorem Th73: :: EUCLID_2:73

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

proof end;

theorem Th74: :: EUCLID_2:74

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

proof end;

definition

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

end;

:: deftheorem Def3 defines are_orthogonal EUCLID_2:def 3 :

theorem Th75: :: EUCLID_2:75

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

proof end;

theorem Th76: :: EUCLID_2:76

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds 0.REAL b₁,b₂ are_orthogonal by Th75;

theorem Th77: :: EUCLID_2:77

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

proof end;

theorem Th78: :: EUCLID_2:78

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

proof end;

theorem Th79: :: EUCLID_2:79

for b₁ being Nat
for b₂ being real number
for b₃, b₄ being Point of (TOP-REAL b₁) st b₃,b₄ are_orthogonal holds
b₃,b₂ * b₄ are_orthogonal by Th78;

theorem Th80: :: EUCLID_2:80

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

proof end;