:: EUCLIDLP semantic presentation

theorem Th1: :: EUCLIDLP:1

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

proof end;

theorem Th2: :: EUCLIDLP:2

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

proof end;

theorem Th3: :: EUCLIDLP:3

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

proof end;

theorem Th4: :: EUCLIDLP:4

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

proof end;

theorem Th5: :: EUCLIDLP:5

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

proof end;

theorem Th6: :: EUCLIDLP:6

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

proof end;

theorem Th7: :: EUCLIDLP:7

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

proof end;

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

proof end;

theorem Th8: :: EUCLIDLP:8

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;

theorem Th9: :: EUCLIDLP:9

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

proof end;

theorem Th10: :: EUCLIDLP:10

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

proof end;

theorem Th11: :: EUCLIDLP:11

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

proof end;

theorem Th12: :: EUCLIDLP:12

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

proof end;

theorem Th13: :: EUCLIDLP:13

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

proof end;

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

proof end;

theorem Th14: :: EUCLIDLP:14

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

proof end;

theorem Th15: :: EUCLIDLP:15

for b₁ being Real
for b₂ being Nat
for b₃, b₄, b₅ being Element of REAL b₂ st b₃ - b₄ = b₁ * b₅ & b₃ <> b₄ holds
b₁ <> 0

proof end;

theorem Th16: :: EUCLIDLP:16

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

proof end;

theorem Th17: :: EUCLIDLP:17

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

proof end;

theorem Th18: :: EUCLIDLP:18

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

proof end;

theorem Th19: :: EUCLIDLP:19

for b₁, b₂, b₃ being Real
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₇)) + ((- b₃) * b₈))

proof end;

theorem Th20: :: EUCLIDLP:20

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

proof end;

theorem Th21: :: EUCLIDLP:21

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

proof end;

theorem Th22: :: EUCLIDLP:22

for b₁ being Nat
for b₂, b₃, 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 Th23: :: EUCLIDLP:23

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

proof end;

theorem Th24: :: EUCLIDLP:24

for b₁ being Nat
for b₂, b₃, 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 Th25: :: EUCLIDLP:25

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

proof end;

theorem Th26: :: EUCLIDLP:26

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

proof end;

theorem Th27: :: EUCLIDLP:27

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

proof end;

theorem Th28: :: EUCLIDLP:28

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

proof end;

theorem Th29: :: EUCLIDLP:29

for b₁, b₂, b₃, b₄, b₅, b₆ being Real
for b₇ being Nat
for b₈, b₉, b₁₀ being Element of REAL b₇ holds (((b₁ * b₈) + (b₂ * b₉)) + (b₃ * b₁₀)) + (((b₄ * b₈) + (b₅ * b₉)) + (b₆ * b₁₀)) = (((b₁ + b₄) * b₈) + ((b₂ + b₅) * b₉)) + ((b₃ + b₆) * b₁₀)

proof end;

theorem Th30: :: EUCLIDLP:30

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

proof end;

theorem Th31: :: EUCLIDLP:31

for b₁, b₂, b₃, b₄, b₅, b₆ being Real
for b₇ being Nat
for b₈, b₉, b₁₀ being Element of REAL b₇ holds (((b₁ * b₈) + (b₂ * b₉)) + (b₃ * b₁₀)) - (((b₄ * b₈) + (b₅ * b₉)) + (b₆ * b₁₀)) = (((b₁ - b₄) * b₈) + ((b₂ - b₅) * b₉)) + ((b₃ - b₆) * b₁₀)

proof end;

theorem Th32: :: EUCLIDLP:32

for b₁, b₂, b₃ being Real
for b₄ being Nat
for b₅, b₆, b₇ being Element of REAL b₄ st (b₁ + b₂) + b₃ = 1 holds
((b₁ * b₅) + (b₂ * b₆)) + (b₃ * b₇) = (b₅ + (b₂ * (b₆ - b₅))) + (b₃ * (b₇ - b₅))

proof end;

theorem Th33: :: EUCLIDLP:33

for b₁, b₂ being Real
for b₃ being Nat
for b₄, b₅, b₆, b₇ being Element of REAL b₃ st b₄ = (b₅ + (b₁ * (b₆ - b₅))) + (b₂ * (b₇ - b₅)) holds
ex b₈ being Real st
( b₄ = ((b₈ * b₅) + (b₁ * b₆)) + (b₂ * b₇) & (b₈ + b₁) + b₂ = 1 )

proof end;

theorem Th34: :: EUCLIDLP:34

for b₁ being Nat st b₁ >= 1 holds
1* b₁ <> 0* b₁

proof end;

theorem Th35: :: EUCLIDLP:35

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 Th36: :: EUCLIDLP:36

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;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
pred c₂ // c₃ means :Def1: :: EUCLIDLP:def 1
( a₂ <> 0* a₁ & a₃ <> 0* a₁ & ex b₁ being Real st a₂ = b₁ * a₃ );

end;

:: deftheorem Def1 defines // EUCLIDLP:def 1 :

theorem Th37: :: EUCLIDLP:37

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ // b₃ holds
ex b₄ being Real st
( b₄ <> 0 & b₂ = b₄ * b₃ )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
redefine pred // as c₂ // c₃;
symmetry

proof end;

end;

theorem Th38: :: EUCLIDLP:38

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ st b₂ // b₃ & b₃ // b₄ holds
b₂ // b₄

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
pred c₂,c₃ are_lindependent2 means :Def2: :: EUCLIDLP:def 2
for b₁, b₂ being Real st (b₁ * a₂) + (b₂ * a₃) = 0* a₁ holds
( b₁ = 0 & b₂ = 0 );
symmetry ;

end;

:: deftheorem Def2 defines are_lindependent2 EUCLIDLP:def 2 :

notation

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
antonym c₂,c₃ are_ldependent2 for c₂,c₃ are_lindependent2 ;

end;

Lemma40: for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂,b₃ are_lindependent2 holds
b₂ <> 0* b₁

proof end;

theorem Th39: :: EUCLIDLP:39

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂,b₃ are_lindependent2 holds
( b₂ <> 0* b₁ & b₃ <> 0* b₁ ) by Lemma40;

theorem Th40: :: EUCLIDLP:40

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat
for b₆, b₇ being Element of REAL b₅ st b₆,b₇ are_lindependent2 & (b₁ * b₆) + (b₂ * b₇) = (b₃ * b₆) + (b₄ * b₇) holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th41: :: EUCLIDLP:41

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat
for b₆, b₇, b₈, b₉, b₁₀ being Element of REAL b₅ st b₁₀,b₆ are_lindependent2 & b₁₀ = (b₁ * b₇) + (b₂ * b₈) & b₆ = (b₃ * b₇) + (b₄ * b₈) holds
ex b₁₁, b₁₂, b₁₃, b₁₄ being Real st
( b₇ = (b₁₁ * b₁₀) + (b₁₂ * b₆) & b₈ = (b₁₃ * b₁₀) + (b₁₄ * b₆) )

proof end;

theorem Th42: :: EUCLIDLP:42

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂,b₃ are_lindependent2 holds
b₂ <> b₃

proof end;

theorem Th43: :: EUCLIDLP:43

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ st b₂ - b₃,b₄ - b₃ are_lindependent2 holds
b₂ <> b₄ by Th42;

theorem Th44: :: EUCLIDLP:44

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

proof end;

theorem Th45: :: EUCLIDLP:45

for b₁ being Nat
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of REAL b₁ st b₂ - b₃,b₄ - b₅ are_lindependent2 & b₆ in Line b₃,b₂ & b₇ in Line b₃,b₂ & b₆ <> b₇ & b₈ in Line b₅,b₄ & b₉ in Line b₅,b₄ & b₈ <> b₉ holds
b₇ - b₆,b₉ - b₈ are_lindependent2

proof end;

Lemma45: for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ // b₃ holds
b₂,b₃ are_ldependent2

proof end;

theorem Th46: :: EUCLIDLP:46

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ // b₃ holds
( b₂,b₃ are_ldependent2 & b₂ <> 0* b₁ & b₃ <> 0* b₁ ) by Def1, Lemma45;

Lemma46: for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂,b₃ are_ldependent2 & b₂ <> 0* b₁ & b₃ <> 0* b₁ holds
b₂ // b₃

proof end;

theorem Th47: :: EUCLIDLP:47

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds
( not b₂,b₃ are_ldependent2 or b₂ = 0* b₁ or b₃ = 0* b₁ or b₂ // b₃ ) by Lemma46;

theorem Th48: :: EUCLIDLP:48

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 )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of REAL c₁;
pred c₂ _|_ c₃ means :Def3: :: EUCLIDLP:def 3
( a₂ <> 0* a₁ & a₃ <> 0* a₁ & a₂,a₃ are_orthogonal );
symmetry ;

end;

:: deftheorem Def3 defines _|_ EUCLIDLP:def 3 :

theorem Th49: :: EUCLIDLP:49

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ st b₂ _|_ b₃ & b₃ // b₄ holds
b₂ _|_ b₄

proof end;

theorem Th50: :: EUCLIDLP:50

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ _|_ b₃ holds
b₂,b₃ are_lindependent2

proof end;

theorem Th51: :: EUCLIDLP:51

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ // b₃ holds
not b₂ _|_ b₃

proof end;

theorem Th52: :: EUCLIDLP:52

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ st b₂ _|_ b₃ holds
not b₂ // b₃ by Th51;

definition

let c₁ be Nat;
func line_of_REAL c₁ -> Subset-Family of (REAL a₁) equals :: EUCLIDLP:def 4
{ b₁ where B is Subset of (REAL a₁) : ex b₁, b₂ being Element of REAL a₁ st b₁ = Line b₂,b₃ } ;
correctness

proof end;

end;

:: deftheorem Def4 defines line_of_REAL EUCLIDLP:def 4 :

registration

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

proof end;

end;

theorem Th53: :: EUCLIDLP:53

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁ holds Line b₂,b₃ in line_of_REAL b₁ ;

theorem Th54: :: EUCLIDLP:54

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

proof end;

theorem Th55: :: EUCLIDLP:55

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ holds
( b₂ meets b₃ iff ex b₄ being Element of REAL b₁ st
( b₄ in b₂ & b₄ in b₃ ) )

proof end;

theorem Th56: :: EUCLIDLP:56

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃, b₄ being Element of line_of_REAL b₁ st b₃ misses b₄ & b₂ in b₃ holds
not b₂ in b₄ by Th55;

theorem Th57: :: EUCLIDLP:57

for b₁ being Nat
for b₂ being Element of line_of_REAL b₁ ex b₃, b₄ being Element of REAL b₁ st b₂ = Line b₃,b₄

proof end;

theorem Th58: :: EUCLIDLP:58

for b₁ being Nat
for b₂ being Element of line_of_REAL b₁ ex b₃ being Element of REAL b₁ st b₃ in b₂

proof end;

theorem Th59: :: EUCLIDLP:59

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

proof end;

theorem Th60: :: EUCLIDLP:60

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ st not b₂ in b₃ & b₃ is_line holds
ex b₄, b₅ being Element of REAL b₁ st
( b₃ = Line b₄,b₅ & b₂ - b₄ _|_ b₅ - b₄ )

proof end;

theorem Th61: :: EUCLIDLP:61

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ st not b₂ in b₃ & b₃ is_line holds
ex b₄, b₅ being Element of REAL b₁ st
( b₃ = Line b₄,b₅ & b₂ - b₄,b₅ - b₄ are_lindependent2 )

proof end;

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
let c₃ be Element of line_of_REAL c₁;
func dist_v c₂,c₃ -> Subset of REAL equals :: EUCLIDLP:def 5
{ |.(a₂ - b₁).| where B is Element of REAL a₁ : b₁ in a₃ } ;
correctness

proof end;

end;

:: deftheorem Def5 defines dist_v EUCLIDLP:def 5 :

definition

let c₁ be Nat;
let c₂ be Element of REAL c₁;
let c₃ be Element of line_of_REAL c₁;
func dist c₂,c₃ -> Real equals :: EUCLIDLP:def 6
lower_bound (dist_v a₂,a₃);
correctness ;

end;

:: deftheorem Def6 defines dist EUCLIDLP:def 6 :

theorem Th62: :: EUCLIDLP:62

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁
for b₅ being Element of line_of_REAL b₁ st b₅ = Line b₂,b₃ holds
{ |.(b₄ - b₆).| where B is Element of REAL b₁ : b₆ in Line b₂,b₃ } = dist_v b₄,b₅ ;

theorem Th63: :: EUCLIDLP:63

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ ex b₄ being Element of REAL b₁ st
( b₄ in b₃ & |.(b₂ - b₄).| = dist b₂,b₃ )

proof end;

theorem Th64: :: EUCLIDLP:64

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ holds dist b₂,b₃ >= 0

proof end;

theorem Th65: :: EUCLIDLP:65

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ holds
( b₂ in b₃ iff dist b₂,b₃ = 0 )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of line_of_REAL c₁;
pred c₂ // c₃ means :Def7: :: EUCLIDLP:def 7
ex b₁, b₂, b₃, b₄ being Element of REAL a₁ st
( a₂ = Line b₁,b₂ & a₃ = Line b₃,b₄ & b₂ - b₁ // b₄ - b₃ );
symmetry ;

end;

:: deftheorem Def7 defines // EUCLIDLP:def 7 :

theorem Th66: :: EUCLIDLP:66

for b₁ being Nat
for b₂, b₃, b₄ being Element of line_of_REAL b₁ st b₂ // b₃ & b₃ // b₄ holds
b₂ // b₄

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of line_of_REAL c₁;
pred c₂ _|_ c₃ means :Def8: :: EUCLIDLP:def 8
ex b₁, b₂, b₃, b₄ being Element of REAL a₁ st
( a₂ = Line b₁,b₂ & a₃ = Line b₃,b₄ & b₂ - b₁ _|_ b₄ - b₃ );
symmetry ;

end;

:: deftheorem Def8 defines _|_ EUCLIDLP:def 8 :

theorem Th67: :: EUCLIDLP:67

for b₁ being Nat
for b₂, b₃, b₄ being Element of line_of_REAL b₁ st b₂ _|_ b₃ & b₃ // b₄ holds
b₂ _|_ b₄

proof end;

theorem Th68: :: EUCLIDLP:68

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ st not b₂ in b₃ & b₃ is_line holds
ex b₄ being Element of line_of_REAL b₁ st
( b₂ in b₄ & b₄ _|_ b₃ & b₄ meets b₃ )

proof end;

theorem Th69: :: EUCLIDLP:69

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ misses b₃ holds
ex b₄ being Element of REAL b₁ st
( b₄ in b₂ & not b₄ in b₃ )

proof end;

theorem Th70: :: EUCLIDLP:70

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

proof end;

theorem Th71: :: EUCLIDLP:71

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ is_line & b₃ is_line & b₂ = b₃ holds
b₂ // b₃

proof end;

theorem Th72: :: EUCLIDLP:72

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ // b₃ holds
( b₂ is_line & b₃ is_line )

proof end;

theorem Th73: :: EUCLIDLP:73

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ _|_ b₃ holds
( b₂ is_line & b₃ is_line )

proof end;

theorem Th74: :: EUCLIDLP:74

for b₁ being Real
for b₂ being Nat
for b₃ being Element of REAL b₂
for b₄ being Element of line_of_REAL b₂ st b₃ in b₄ & b₁ <> 1 & b₁ * b₃ in b₄ holds
0* b₂ in b₄

proof end;

theorem Th75: :: EUCLIDLP:75

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

proof end;

theorem Th76: :: EUCLIDLP:76

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

proof end;

theorem Th77: :: EUCLIDLP:77

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ // b₃ & b₂ <> b₃ holds
b₂ misses b₃

proof end;

theorem Th78: :: EUCLIDLP:78

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ holds
( not b₂ // b₃ or b₂ = b₃ or b₂ misses b₃ ) by Th77;

theorem Th79: :: EUCLIDLP:79

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ // b₃ & b₂ meets b₃ holds
b₂ = b₃ by Th77;

theorem Th80: :: EUCLIDLP:80

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ st b₃ is_line holds
ex b₄ being Element of line_of_REAL b₁ st
( b₂ in b₄ & b₄ // b₃ )

proof end;

theorem Th81: :: EUCLIDLP:81

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

proof end;

theorem Th82: :: EUCLIDLP:82

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁
for b₆, b₇ being Element of line_of_REAL b₁ st b₂ in b₆ & b₃ in b₆ & b₂ <> b₃ & b₄ in b₇ & b₅ in b₇ & b₄ <> b₅ & b₆ _|_ b₇ holds
b₃ - b₂ _|_ b₅ - b₄

proof end;

theorem Th83: :: EUCLIDLP:83

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ _|_ b₃ holds
b₂ <> b₃

proof end;

theorem Th84: :: EUCLIDLP:84

for b₁ being Nat
for b₂, b₃ being Element of REAL b₁
for b₄ being Element of line_of_REAL b₁ st b₄ is_line & b₄ = Line b₂,b₃ holds
b₂ <> b₃

proof end;

theorem Th85: :: EUCLIDLP:85

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁
for b₆, b₇ being Element of line_of_REAL b₁ st b₂ in b₆ & b₃ in b₆ & b₂ <> b₃ & b₄ in b₇ & b₅ in b₇ & b₄ <> b₅ & b₆ // b₇ holds
b₃ - b₂ // b₅ - b₄

proof end;

theorem Th86: :: EUCLIDLP:86

for b₁ being Nat
for b₂, b₃, b₄, b₅, b₆ being Element of REAL b₁
for b₇, b₈ being Element of line_of_REAL b₁ st b₂ - b₃,b₄ - b₃ are_lindependent2 & b₅ in Line b₃,b₂ & b₆ in Line b₃,b₄ & b₇ = Line b₂,b₄ & b₈ = Line b₅,b₆ holds
( b₇ // b₈ iff ex b₉ being Real st
( b₉ <> 0 & b₅ - b₃ = b₉ * (b₂ - b₃) & b₆ - b₃ = b₉ * (b₄ - b₃) ) )

proof end;

theorem Th87: :: EUCLIDLP:87

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

proof end;

theorem Th88: :: EUCLIDLP:88

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃, b₄ being Element of line_of_REAL b₁ st b₃ _|_ b₄ & b₂ in b₄ holds
ex b₅ being Element of line_of_REAL b₁ st
( b₂ in b₅ & b₅ _|_ b₄ & b₅ // b₃ )

proof end;

theorem Th89: :: EUCLIDLP:89

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃, b₄ being Element of line_of_REAL b₁ st b₂ in b₃ & b₂ in b₄ & b₃ _|_ b₄ holds
ex b₅ being Element of REAL b₁ st
( b₂ <> b₅ & b₅ in b₃ & not b₅ in b₄ )

proof end;

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Element of REAL c₁;
func plane c₂,c₃,c₄ -> Subset of (REAL a₁) equals :: EUCLIDLP:def 9
{ b₁ where B is Element of REAL a₁ : ex b₁, b₂, b₃ being Real st
( (b₂ + b₃) + b₄ = 1 & b₁ = ((b₂ * a₂) + (b₃ * a₃)) + (b₄ * a₄) ) } ;
correctness

proof end;

end;

:: deftheorem Def9 defines plane EUCLIDLP:def 9 :

registration

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

proof end;

end;

definition

let c₁ be Nat;
let c₂ be Subset of (REAL c₁);
attr a₂ is being_plane means :Def10: :: EUCLIDLP:def 10
ex b₁, b₂, b₃ being Element of REAL a₁ st
( b₂ - b₁,b₃ - b₁ are_lindependent2 & a₂ = plane b₁,b₂,b₃ );

end;

:: deftheorem Def10 defines being_plane EUCLIDLP:def 10 :

theorem Th90: :: EUCLIDLP:90

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

proof end;

theorem Th91: :: EUCLIDLP:91

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

proof end;

theorem Th92: :: EUCLIDLP:92

for b₁ being Nat
for b₂ being Subset of (REAL b₁)
for b₃, b₄, b₅, b₆ being Element of REAL b₁ st b₃ in plane b₄,b₅,b₆ & ex b₇, b₈, b₉ being Real st
( (b₇ + b₈) + b₉ = 0 & b₃ = ((b₇ * b₄) + (b₈ * b₅)) + (b₉ * b₆) ) holds
0* b₁ in plane b₄,b₅,b₆

proof end;

theorem Th93: :: EUCLIDLP:93

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

proof end;

theorem Th94: :: EUCLIDLP:94

for b₁ being Nat
for b₂ being Subset of (REAL b₁)
for b₃ being Element of REAL b₁ st b₂ is being_plane & b₃ in b₂ & ex b₄ being Real st
( b₄ <> 1 & b₄ * b₃ in b₂ ) holds
0* b₁ in b₂

proof end;

theorem Th95: :: EUCLIDLP:95

for b₁, b₂, b₃ being Real
for b₄ being Nat
for b₅, b₆, b₇, b₈ being Element of REAL b₄ st b₅ - b₅,b₆ - b₅ are_lindependent2 & b₇ in plane b₅,b₈,b₆ & b₇ = ((b₁ * b₅) + (b₂ * b₈)) + (b₃ * b₆) & not (b₁ + b₂) + b₃ = 1 holds
0* b₄ in plane b₅,b₈,b₆

proof end;

theorem Th96: :: EUCLIDLP:96

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁ holds
( b₂ in plane b₃,b₄,b₅ iff ex b₆, b₇, b₈ being Real st
( (b₆ + b₇) + b₈ = 1 & b₂ = ((b₆ * b₃) + (b₇ * b₄)) + (b₈ * b₅) ) )

proof end;

theorem Th97: :: EUCLIDLP:97

for b₁, b₂, b₃, b₄, b₅, b₆ being Real
for b₇ being Nat
for b₈, b₉, b₁₀, b₁₁ being Element of REAL b₇ st b₈ - b₉,b₁₀ - b₉ are_lindependent2 & b₁₁ in plane b₉,b₈,b₁₀ & (b₁ + b₂) + b₃ = 1 & b₁₁ = ((b₁ * b₉) + (b₂ * b₈)) + (b₃ * b₁₀) & (b₄ + b₅) + b₆ = 1 & b₁₁ = ((b₄ * b₉) + (b₅ * b₈)) + (b₆ * b₁₀) holds
( b₁ = b₄ & b₂ = b₅ & b₃ = b₆ )

proof end;

definition

let c₁ be Nat;
func plane_of_REAL c₁ -> Subset-Family of (REAL a₁) equals :: EUCLIDLP:def 11
{ b₁ where B is Subset of (REAL a₁) : ex b₁, b₂, b₃ being Element of REAL a₁ st b₁ = plane b₂,b₃,b₄ } ;
correctness

proof end;

end;

:: deftheorem Def11 defines plane_of_REAL EUCLIDLP:def 11 :

registration

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

proof end;

end;

theorem Th98: :: EUCLIDLP:98

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds plane b₂,b₃,b₄ in plane_of_REAL b₁ ;

theorem Th99: :: EUCLIDLP:99

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

proof end;

theorem Th100: :: EUCLIDLP:100

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁
for b₅ being Element of plane_of_REAL b₁ st b₂ in b₅ & b₃ in b₅ & b₄ in b₅ & b₃ - b₂,b₄ - b₂ are_lindependent2 holds
b₅ = plane b₂,b₃,b₄

proof end;

theorem Th101: :: EUCLIDLP:101

for b₁ being Nat
for b₂, b₃ being Element of plane_of_REAL b₁ st b₂ is being_plane & b₂ c= b₃ holds
b₂ = b₃

proof end;

theorem Th102: :: EUCLIDLP:102

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds
( Line b₂,b₃ c= plane b₂,b₃,b₄ & Line b₃,b₄ c= plane b₂,b₃,b₄ & Line b₄,b₂ c= plane b₂,b₃,b₄ )

proof end;

theorem Th103: :: EUCLIDLP:103

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

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of line_of_REAL c₁;
pred c₂,c₃ are_coplane means :Def12: :: EUCLIDLP:def 12
ex b₁, b₂, b₃ being Element of REAL a₁ st
( a₂ c= plane b₁,b₂,b₃ & a₃ c= plane b₁,b₂,b₃ );

end;

:: deftheorem Def12 defines are_coplane EUCLIDLP:def 12 :

theorem Th104: :: EUCLIDLP:104

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ holds
( b₂,b₃ are_coplane iff ex b₄ being Element of plane_of_REAL b₁ st
( b₂ c= b₄ & b₃ c= b₄ ) )

proof end;

theorem Th105: :: EUCLIDLP:105

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ // b₃ holds
b₂,b₃ are_coplane

proof end;

theorem Th106: :: EUCLIDLP:106

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ is_line & b₃ is_line & b₂,b₃ are_coplane & b₂ misses b₃ holds
ex b₄ being Element of plane_of_REAL b₁ st
( b₂ c= b₄ & b₃ c= b₄ & b₄ is being_plane )

proof end;

theorem Th107: :: EUCLIDLP:107

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ ex b₄ being Element of plane_of_REAL b₁ st
( b₂ in b₄ & b₃ c= b₄ )

proof end;

theorem Th108: :: EUCLIDLP:108

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁ st not b₂ in b₃ & b₃ is_line holds
ex b₄ being Element of plane_of_REAL b₁ st
( b₂ in b₄ & b₃ c= b₄ & b₄ is being_plane )

proof end;

theorem Th109: :: EUCLIDLP:109

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁
for b₄ being Element of plane_of_REAL b₁ st b₂ in b₄ & b₃ c= b₄ & not b₂ in b₃ & b₃ is_line holds
b₄ is being_plane

proof end;

theorem Th110: :: EUCLIDLP:110

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being Element of line_of_REAL b₁
for b₄, b₅ being Element of plane_of_REAL b₁ st not b₂ in b₃ & b₃ is_line & b₂ in b₄ & b₃ c= b₄ & b₂ in b₅ & b₃ c= b₅ holds
b₄ = b₅

proof end;

theorem Th111: :: EUCLIDLP:111

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ is_line & b₃ is_line & b₂,b₃ are_coplane & b₂ <> b₃ holds
ex b₄ being Element of plane_of_REAL b₁ st
( b₂ c= b₄ & b₃ c= b₄ & b₄ is being_plane )

proof end;

theorem Th112: :: EUCLIDLP:112

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ is_line & b₃ is_line & b₂ <> b₃ & b₂ meets b₃ holds
ex b₄ being Element of plane_of_REAL b₁ st
( b₂ c= b₄ & b₃ c= b₄ & b₄ is being_plane )

proof end;

theorem Th113: :: EUCLIDLP:113

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁
for b₄, b₅ being Element of plane_of_REAL b₁ st b₂ is_line & b₃ is_line & b₂ <> b₃ & b₂ meets b₃ & b₂ c= b₄ & b₃ c= b₄ & b₂ c= b₅ & b₃ c= b₅ holds
b₄ = b₅

proof end;

theorem Th114: :: EUCLIDLP:114

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ // b₃ & b₂ <> b₃ holds
ex b₄ being Element of plane_of_REAL b₁ st
( b₂ c= b₄ & b₃ c= b₄ & b₄ is being_plane )

proof end;

theorem Th115: :: EUCLIDLP:115

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂ _|_ b₃ & b₂ meets b₃ holds
ex b₄ being Element of plane_of_REAL b₁ st
( b₄ is being_plane & b₂ c= b₄ & b₃ c= b₄ )

proof end;

theorem Th116: :: EUCLIDLP:116

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃, b₄, b₅ being Element of line_of_REAL b₁
for b₆ being Element of plane_of_REAL b₁ st b₃ c= b₆ & b₄ c= b₆ & b₅ c= b₆ & b₂ in b₃ & b₂ in b₄ & b₂ in b₅ & b₃ _|_ b₅ & b₄ _|_ b₅ holds
b₃ = b₄

proof end;

theorem Th117: :: EUCLIDLP:117

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂,b₃ are_coplane & b₂ _|_ b₃ holds
b₂ meets b₃

proof end;

theorem Th118: :: EUCLIDLP:118

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃, b₄, b₅ being Element of line_of_REAL b₁
for b₆ being Element of plane_of_REAL b₁ st b₃ c= b₆ & b₄ c= b₆ & b₃ _|_ b₄ & b₂ in b₆ & b₅ // b₄ & b₂ in b₅ holds
( b₅ c= b₆ & b₅ _|_ b₃ )

proof end;

theorem Th119: :: EUCLIDLP:119

for b₁ being Nat
for b₂, b₃, b₄ being Element of line_of_REAL b₁
for b₅ being Element of plane_of_REAL b₁ st b₂ c= b₅ & b₃ c= b₅ & b₄ c= b₅ & b₂ _|_ b₃ & b₂ _|_ b₄ holds
b₃ // b₄

proof end;

theorem Th120: :: EUCLIDLP:120

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of line_of_REAL b₁
for b₆ being Element of plane_of_REAL b₁ st b₂ c= b₆ & b₃ c= b₆ & b₄ c= b₆ & b₂ // b₃ & b₃ // b₄ & b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ & b₅ meets b₂ & b₅ meets b₃ holds
b₅ meets b₄

proof end;

theorem Th121: :: EUCLIDLP:121

for b₁ being Nat
for b₂, b₃ being Element of line_of_REAL b₁ st b₂,b₃ are_coplane & b₂ is_line & b₃ is_line & b₂ misses b₃ holds
b₂ // b₃

proof end;

theorem Th122: :: EUCLIDLP:122

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Element of REAL b₁
for b₆ being Element of plane_of_REAL b₁ st b₂ in b₆ & b₃ in b₆ & b₄ in b₆ & b₅ in b₆ & b₃ - b₂,b₅ - b₄ are_lindependent2 holds
Line b₂,b₃ meets Line b₄,b₅

proof end;