:: by Akihiro Kubo

::

:: Received August 8, 2003

:: Copyright (c) 2003-2018 Association of Mizar Users

theorem :: EUCLID_4:4

theorem :: EUCLID_4:5

for a being Real

for n being Nat

for x being Element of REAL n holds

( not a * x = 0* n or a = 0 or x = 0* n )

for n being Nat

for x being Element of REAL n holds

( not a * x = 0* n or a = 0 or x = 0* n )

proof end;

theorem :: EUCLID_4:6

theorem :: EUCLID_4:7

theorem :: EUCLID_4:8

for a being Real

for n being Nat

for x1, x2 being Element of REAL n holds

( not a * x1 = a * x2 or a = 0 or x1 = x2 )

for n being Nat

for x1, x2 being Element of REAL n holds

( not a * x1 = a * x2 or a = 0 or x1 = x2 )

proof end;

definition

let n be Nat;

let x1, x2 be Element of REAL n;

{ (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } is Subset of (REAL n)

end;
let x1, x2 be Element of REAL n;

func Line (x1,x2) -> Subset of (REAL n) equals :: EUCLID_4:def 1

{ (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;

coherence { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;

{ (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } is Subset of (REAL n)

proof end;

:: deftheorem defines Line EUCLID_4:def 1 :

for n being Nat

for x1, x2 being Element of REAL n holds Line (x1,x2) = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;

for n being Nat

for x1, x2 being Element of REAL n holds Line (x1,x2) = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;

registration
end;

Lm1: for n being Nat

for x1, x2 being Element of REAL n holds Line (x1,x2) c= Line (x2,x1)

proof end;

definition

let n be Nat;

let x1, x2 be Element of REAL n;

:: original: Line

redefine func Line (x1,x2) -> Subset of (REAL n);

commutativity

for x1, x2 being Element of REAL n holds Line (x1,x2) = Line (x2,x1) by Lm1;

end;
let x1, x2 be Element of REAL n;

:: original: Line

redefine func Line (x1,x2) -> Subset of (REAL n);

commutativity

for x1, x2 being Element of REAL n holds Line (x1,x2) = Line (x2,x1) by Lm1;

theorem Th9: :: EUCLID_4:9

for n being Nat

for x1, x2 being Element of REAL n holds

( x1 in Line (x1,x2) & x2 in Line (x1,x2) )

for x1, x2 being Element of REAL n holds

( x1 in Line (x1,x2) & x2 in Line (x1,x2) )

proof end;

Lm2: for n being Nat

for x1, x2, x3 being Element of REAL n holds x1 + (x2 + x3) = (x1 + x2) + x3

by FINSEQOP:28;

theorem Th10: :: EUCLID_4:10

for n being Nat

for x1, x2, y1, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds

Line (y1,y2) c= Line (x1,x2)

for x1, x2, y1, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds

Line (y1,y2) c= Line (x1,x2)

proof end;

theorem Th11: :: EUCLID_4:11

for n being Nat

for x1, x2, y1, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds

Line (x1,x2) c= Line (y1,y2)

for x1, x2, y1, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds

Line (x1,x2) c= Line (y1,y2)

proof end;

definition

let n be Nat;

let A be Subset of (REAL n);

end;
let A be Subset of (REAL n);

attr A is being_line means :: EUCLID_4:def 2

ex x1, x2 being Element of REAL n st

( x1 <> x2 & A = Line (x1,x2) );

ex x1, x2 being Element of REAL n st

( x1 <> x2 & A = Line (x1,x2) );

:: deftheorem defines being_line EUCLID_4:def 2 :

for n being Nat

for A being Subset of (REAL n) holds

( A is being_line iff ex x1, x2 being Element of REAL n st

( x1 <> x2 & A = Line (x1,x2) ) );

for n being Nat

for A being Subset of (REAL n) holds

( A is being_line iff ex x1, x2 being Element of REAL n st

( x1 <> x2 & A = Line (x1,x2) ) );

Lm3: for n being Nat

for A being Subset of (REAL n)

for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds

A = Line (x1,x2)

by Th10, Th11;

theorem :: EUCLID_4:12

for n being Nat

for A, C being Subset of (REAL n)

for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds

A = C

for A, C being Subset of (REAL n)

for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds

A = C

proof end;

theorem Th13: :: EUCLID_4:13

for n being Nat

for A being Subset of (REAL n) st A is being_line holds

ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 )

for A being Subset of (REAL n) st A is being_line holds

ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 )

proof end;

theorem :: EUCLID_4:14

for n being Nat

for x1 being Element of REAL n

for A being Subset of (REAL n) st A is being_line holds

ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

for x1 being Element of REAL n

for A being Subset of (REAL n) st A is being_line holds

ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

proof end;

theorem :: EUCLID_4:19

theorem Th20: :: EUCLID_4:20

for n being Nat

for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|

for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|

proof end;

theorem Th21: :: EUCLID_4:21

for n being Nat

for x1, x2 being Element of REAL n

for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|

for x1, x2 being Element of REAL n

for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|

proof end;

theorem :: EUCLID_4:22

theorem :: EUCLID_4:24

theorem Th26: :: EUCLID_4:26

for n being Nat

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

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

proof end;

theorem :: EUCLID_4:27

for n being Nat

for a, b being Real

for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)

for a, b being Real

for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)

proof end;

theorem :: EUCLID_4:28

theorem :: EUCLID_4:29

theorem Th30: :: EUCLID_4:30

for n being Nat

for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th31: :: EUCLID_4:31

for n being Nat

for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th32: :: EUCLID_4:32

for n being Nat

for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|

for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|

proof end;

theorem Th33: :: EUCLID_4:33

for n being Nat

for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|

for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|

proof end;

theorem :: EUCLID_4:34

for n being Nat

for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)

for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)

proof end;

theorem :: EUCLID_4:35

for n being Nat

for x, y being Element of REAL n holds |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2)

for x, y being Element of REAL n holds |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2)

proof end;

theorem :: EUCLID_4:36

for n being Nat

for x, y being Element of REAL n holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))

for x, y being Element of REAL n holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))

proof end;

theorem :: EUCLID_4:37

for n being Nat

for x, y being Element of REAL n holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|

for x, y being Element of REAL n holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|

proof end;

Lm4: for a being Real

for n being Nat

for x being Element of REAL n holds

( - (a * x) = (- a) * x & - (a * x) = a * (- x) )

proof end;

Lm5: for n being Nat

for x1, x2 being Element of REAL n st x1 <> x2 holds

|.(x1 - x2).| <> 0

proof end;

Lm6: for n being Nat

for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds

ex a being Real st y1 - y2 = a * (x1 - x2)

proof end;

Lm7: for n being Nat

for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line (x1,x2) holds

|.(y1 - y2).| <= |.(y1 - x).| ) )

proof end;

::$CT

theorem :: EUCLID_4:40

for n being Nat

for R being Subset of REAL

for x1, x2, y1 being Element of REAL n st R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } holds

ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )

for R being Subset of REAL

for x1, x2, y1 being Element of REAL n st R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } holds

ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )

proof end;

definition
end;

Lm8: for n being Nat

for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st

( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )

proof end;

theorem :: EUCLID_4:41

theorem :: EUCLID_4:42

theorem :: EUCLID_4:43

definition

let n be Nat;

let A be Subset of (TOP-REAL n);

end;
let A be Subset of (TOP-REAL n);

attr A is being_line means :: EUCLID_4:def 4

ex p1, p2 being Point of (TOP-REAL n) st

( p1 <> p2 & A = Line (p1,p2) );

ex p1, p2 being Point of (TOP-REAL n) st

( p1 <> p2 & A = Line (p1,p2) );

:: deftheorem defines being_line EUCLID_4:def 4 :

for n being Nat

for A being Subset of (TOP-REAL n) holds

( A is being_line iff ex p1, p2 being Point of (TOP-REAL n) st

( p1 <> p2 & A = Line (p1,p2) ) );

for n being Nat

for A being Subset of (TOP-REAL n) holds

( A is being_line iff ex p1, p2 being Point of (TOP-REAL n) st

( p1 <> p2 & A = Line (p1,p2) ) );

Lm9: for n being Nat

for A being Subset of (TOP-REAL n)

for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds

A = Line (p1,p2)

by RLTOPSP1:75;

theorem :: EUCLID_4:44

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds

A = C

for p1, p2 being Point of (TOP-REAL n)

for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds

A = C

proof end;

theorem Th44: :: EUCLID_4:45

for n being Nat

for A being Subset of (TOP-REAL n) st A is being_line holds

ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 )

for A being Subset of (TOP-REAL n) st A is being_line holds

ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 )

proof end;

theorem :: EUCLID_4:46

for n being Nat

for p1 being Point of (TOP-REAL n)

for A being Subset of (TOP-REAL n) st A is being_line holds

ex p2 being Point of (TOP-REAL n) st

( p1 <> p2 & p2 in A )

for p1 being Point of (TOP-REAL n)

for A being Subset of (TOP-REAL n) st A is being_line holds

ex p2 being Point of (TOP-REAL n) st

( p1 <> p2 & p2 in A )

proof end;

theorem :: EUCLID_4:47

for n being Nat

for R being Subset of REAL

for p1, p2, q1 being Point of (TOP-REAL n) st R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) } holds

ex q2 being Point of (TOP-REAL n) st

( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )

for R being Subset of REAL

for p1, p2, q1 being Point of (TOP-REAL n) st R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) } holds

ex q2 being Point of (TOP-REAL n) st

( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )

proof end;