:: EUCLID_3 semantic presentation

definition

let z be Element of COMPLEX ;
func cpx2euc z -> Point of (TOP-REAL 2) equals :: EUCLID_3:def 1
|[(Re z),(Im z)]|;
correctness ;

end;

:: deftheorem defines cpx2euc EUCLID_3:def 1 :

definition

let p be Point of (TOP-REAL 2);
func euc2cpx p -> Element of COMPLEX equals :: EUCLID_3:def 2
[*(p `1 ),(p `2 )*];
correctness ;

end;

:: deftheorem defines euc2cpx EUCLID_3:def 2 :

theorem Th1: :: EUCLID_3:1

for z being Element of COMPLEX holds euc2cpx (cpx2euc z) = z

proof end;

theorem Th2: :: EUCLID_3:2

for p being Point of (TOP-REAL 2) holds cpx2euc (euc2cpx p) = p

proof end;

theorem :: EUCLID_3:3

for p being Point of (TOP-REAL 2) ex z being Element of COMPLEX st p = cpx2euc z

proof end;

theorem :: EUCLID_3:4

for z being Element of COMPLEX ex p being Point of (TOP-REAL 2) st z = euc2cpx p

proof end;

theorem :: EUCLID_3:5

for z1, z2 being Element of COMPLEX st cpx2euc z1 = cpx2euc z2 holds
z1 = z2

proof end;

theorem Th6: :: EUCLID_3:6

for p1, p2 being Point of (TOP-REAL 2) st euc2cpx p1 = euc2cpx p2 holds
p1 = p2

proof end;

theorem Th7: :: EUCLID_3:7

for z being Element of COMPLEX holds
( (cpx2euc z) `1 = Re z & (cpx2euc z) `2 = Im z ) by EUCLID:56;

theorem Th8: :: EUCLID_3:8

for p being Point of (TOP-REAL 2) holds
( Re (euc2cpx p) = p `1 & Im (euc2cpx p) = p `2 )

proof end;

theorem Th9: :: EUCLID_3:9

for x1, x2 being Real holds cpx2euc [*x1,x2*] = |[x1,x2]|

proof end;

theorem Th10: :: EUCLID_3:10

for z1, z2 being Element of COMPLEX holds |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]|

proof end;

theorem Th11: :: EUCLID_3:11

for z1, z2 being Element of COMPLEX holds cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2)

proof end;

theorem Th12: :: EUCLID_3:12

for p1, p2 being Point of (TOP-REAL 2) holds [*((p1 + p2) `1 ),((p1 + p2) `2 )*] = [*((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 ))*]

proof end;

theorem Th13: :: EUCLID_3:13

for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2)

proof end;

theorem Th14: :: EUCLID_3:14

for z being Element of COMPLEX holds |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]|

proof end;

theorem Th15: :: EUCLID_3:15

for z being Element of COMPLEX holds cpx2euc (- z) = - (cpx2euc z)

proof end;

theorem Th16: :: EUCLID_3:16

for p being Point of (TOP-REAL 2) holds [*((- p) `1 ),((- p) `2 )*] = [*(- (p `1 )),(- (p `2 ))*]

proof end;

theorem Th17: :: EUCLID_3:17

for p being Point of (TOP-REAL 2) holds euc2cpx (- p) = - (euc2cpx p)

proof end;

theorem :: EUCLID_3:18

for z1, z2 being Element of COMPLEX holds cpx2euc (z1 - z2) = (cpx2euc z1) - (cpx2euc z2)

proof end;

theorem Th19: :: EUCLID_3:19

for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2)

proof end;

theorem Th20: :: EUCLID_3:20

cpx2euc 0c = 0.REAL 2 by COMPLEX1:12, EUCLID:58;

theorem Th21: :: EUCLID_3:21

euc2cpx (0.REAL 2) = 0c by Th1, Th20;

theorem :: EUCLID_3:22

for p being Point of (TOP-REAL 2) st euc2cpx p = 0c holds
p = 0.REAL 2 by Th2, Th20;

theorem :: EUCLID_3:23

for z being Element of COMPLEX
for r being Real holds cpx2euc ([*r,0*] * z) = r * (cpx2euc z)

proof end;

theorem :: EUCLID_3:24

for r, r1, r2 being Real holds (r + (0 * <i> )) * (r1 + (r2 * <i> )) = (r * r1) + ((r * r2) * <i> ) ;

theorem :: EUCLID_3:25

for r being Real
for p being Point of (TOP-REAL 2) holds euc2cpx (r * p) = [*r,0*] * (euc2cpx p)

proof end;

theorem Th26: :: EUCLID_3:26

for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))

proof end;

theorem Th27: :: EUCLID_3:27

for f being FinSequence of REAL st len f = 2 holds
|.f.| = sqrt (((f . 1) ^2 ) + ((f . 2) ^2 ))

proof end;

theorem :: EUCLID_3:28

for f being FinSequence of REAL
for p being Point of (TOP-REAL 2) st len f = 2 & p = f holds
|.p.| = |.f.|

proof end;

theorem Th29: :: EUCLID_3:29

for z being Element of COMPLEX holds |.(cpx2euc z).| = sqrt (((Re z) ^2 ) + ((Im z) ^2 ))

proof end;

theorem :: EUCLID_3:30

for z being Element of COMPLEX holds |.(cpx2euc z).| = |.z.|

proof end;

theorem Th31: :: EUCLID_3:31

for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = |.p.|

proof end;

definition

let p be Point of (TOP-REAL 2);
func Arg p -> Real equals :: EUCLID_3:def 3
Arg (euc2cpx p);
correctness ;

end;

:: deftheorem defines Arg EUCLID_3:def 3 :

theorem :: EUCLID_3:32

for z being Element of COMPLEX
for p being Point of (TOP-REAL 2) st ( z = euc2cpx p or p = cpx2euc z ) holds
Arg z = Arg p

proof end;

theorem :: EUCLID_3:33

for p being Point of (TOP-REAL 2) holds
( 0 <= Arg p & Arg p < 2 * PI ) by COMPTRIG:52;

theorem :: EUCLID_3:34

for x1, x2 being Real
for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds
p = |[x1,x2]|

proof end;

theorem :: EUCLID_3:35

Arg (0.REAL 2) = 0 by Th21, COMPLEX2:20;

theorem :: EUCLID_3:36

for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) )

proof end;

theorem :: EUCLID_3:37

for p being Point of (TOP-REAL 2) st Arg p = 0 holds
( p = |[|.p.|,0]| & p `2 = 0 )

proof end;

theorem Th38: :: EUCLID_3:38

for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
( Arg p < PI iff Arg (- p) >= PI )

proof end;

theorem :: EUCLID_3:39

for p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 or p1 - p2 <> 0.REAL 2 ) holds
( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI )

proof end;

theorem :: EUCLID_3:40

for p being Point of (TOP-REAL 2) holds
( Arg p in ].0,PI .[ iff p `2 > 0 )

proof end;

theorem :: EUCLID_3:41

for p being Point of (TOP-REAL 2) st Arg p <> 0 holds
( Arg p < PI iff sin (Arg p) > 0 ) by COMPLEX2:28;

theorem :: EUCLID_3:42

for p1, p2 being Point of (TOP-REAL 2) st Arg p1 < PI & Arg p2 < PI holds
Arg (p1 + p2) < PI

proof end;

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
func angle p1,p2,p3 -> Real equals :: EUCLID_3:def 4
angle (euc2cpx p1),(euc2cpx p2),(euc2cpx p3);
correctness by XREAL_0:def 1;

end;

:: deftheorem defines angle EUCLID_3:def 4 :

theorem :: EUCLID_3:43

for p1, p2, p3 being Point of (TOP-REAL 2) holds
( 0 <= angle p1,p2,p3 & angle p1,p2,p3 < 2 * PI ) by COMPLEX2:84;

theorem :: EUCLID_3:44

for p1, p2, p3 being Point of (TOP-REAL 2) holds angle p1,p2,p3 = angle (p1 - p2),(0.REAL 2),(p3 - p2)

proof end;

theorem :: EUCLID_3:45

for p1, p2, p3 being Point of (TOP-REAL 2) st angle p1,p2,p3 = 0 holds
( Arg (p1 - p2) = Arg (p3 - p2) & angle p3,p2,p1 = 0 )

proof end;

theorem :: EUCLID_3:46

for p1, p2, p3 being Point of (TOP-REAL 2) st angle p1,p2,p3 <> 0 holds
angle p3,p2,p1 = (2 * PI ) - (angle p1,p2,p3)

proof end;

theorem :: EUCLID_3:47

for p1, p2, p3 being Point of (TOP-REAL 2) st angle p3,p2,p1 <> 0 holds
angle p3,p2,p1 = (2 * PI ) - (angle p1,p2,p3)

proof end;

theorem Th48: :: EUCLID_3:48

for x, y being Element of COMPLEX holds Re (x .|. y) = ((Re x) * (Re y)) + ((Im x) * (Im y))

proof end;

theorem Th49: :: EUCLID_3:49

for x, y being Element of COMPLEX holds Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y))

proof end;

theorem Th50: :: EUCLID_3:50

for p, q being Point of (TOP-REAL 2) holds |(p,q)| = ((p `1 ) * (q `1 )) + ((p `2 ) * (q `2 ))

proof end;

theorem Th51: :: EUCLID_3:51

for p1, p2 being Point of (TOP-REAL 2) holds |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2))

proof end;

theorem :: EUCLID_3:52

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> 0.REAL 2 & p2 <> 0.REAL 2 holds
( |(p1,p2)| = 0 iff ( angle p1,(0.REAL 2),p2 = PI / 2 or angle p1,(0.REAL 2),p2 = (3 / 2) * PI ) )

proof end;

theorem :: EUCLID_3:53

for p1, p2 being Point of (TOP-REAL 2) st p1 <> 0.REAL 2 & p2 <> 0.REAL 2 holds
( ( ( not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| & not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) or angle p1,(0.REAL 2),p2 = PI / 2 or angle p1,(0.REAL 2),p2 = (3 / 2) * PI ) & ( ( not angle p1,(0.REAL 2),p2 = PI / 2 & not angle p1,(0.REAL 2),p2 = (3 / 2) * PI ) or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) )

proof end;

theorem :: EUCLID_3:54

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 & p3 <> p2 holds
( |((p1 - p2),(p3 - p2))| = 0 iff ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) )

proof end;

theorem :: EUCLID_3:55

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 & p3 <> p2 & ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) holds
(|.(p1 - p2).| ^2 ) + (|.(p3 - p2).| ^2 ) = |.(p1 - p3).| ^2

proof end;

theorem :: EUCLID_3:56

for p1, p2, p3 being Point of (TOP-REAL 2) st p2 <> p1 & p1 <> p3 & p3 <> p2 & angle p2,p1,p3 < PI & angle p1,p3,p2 < PI & angle p3,p2,p1 < PI holds
((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI

proof end;

definition

let n be Nat;
let p1, p2, p3 be Point of (TOP-REAL n);
func Triangle p1,p2,p3 -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 5
((LSeg p1,p2) \/ (LSeg p2,p3)) \/ (LSeg p3,p1);
correctness ;

end;

:: deftheorem defines Triangle EUCLID_3:def 5 :

definition

let n be Nat;
let p1, p2, p3 be Point of (TOP-REAL n);
func closed_inside_of_triangle p1,p2,p3 -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 6
{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;
correctness

proof end;

end;

:: deftheorem defines closed_inside_of_triangle EUCLID_3:def 6 :

definition

let n be Nat;
let p1, p2, p3 be Point of (TOP-REAL n);
func inside_of_triangle p1,p2,p3 -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 7
(closed_inside_of_triangle p1,p2,p3) \ (Triangle p1,p2,p3);
correctness ;

end;

:: deftheorem defines inside_of_triangle EUCLID_3:def 7 :

definition

let n be Nat;
let p1, p2, p3 be Point of (TOP-REAL n);
func outside_of_triangle p1,p2,p3 -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 8
{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;
correctness

proof end;

end;

:: deftheorem defines outside_of_triangle EUCLID_3:def 8 :

definition

let n be Nat;
let p1, p2, p3 be Point of (TOP-REAL n);
func plane p1,p2,p3 -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 9
(outside_of_triangle p1,p2,p3) \/ (closed_inside_of_triangle p1,p2,p3);
correctness ;

end;

:: deftheorem defines plane EUCLID_3:def 9 :

theorem Th57: :: EUCLID_3:57

for n being Nat
for p1, p2, p3, p being Point of (TOP-REAL n) st p in plane p1,p2,p3 holds
ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

proof end;

theorem :: EUCLID_3:58

for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle p1,p2,p3 c= closed_inside_of_triangle p1,p2,p3

proof end;

definition

let n be Nat;
let q1, q2 be Point of (TOP-REAL n);
pred q1,q2 are_lindependent2 means :Def10: :: EUCLID_3:def 10
for a1, a2 being Real st (a1 * q1) + (a2 * q2) = 0.REAL n holds
( a1 = 0 & a2 = 0 );

end;

:: deftheorem Def10 defines are_lindependent2 EUCLID_3:def 10 :

notation

let n be Nat;
let q1, q2 be Point of (TOP-REAL n);
antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2 ;

end;

theorem Th59: :: EUCLID_3:59

for n being Nat
for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds
( q1 <> q2 & q1 <> 0.REAL n & q2 <> 0.REAL n )

proof end;

theorem Th60: :: EUCLID_3:60

for n being Nat
for p1, p2, p3, p0 being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p0 in plane p1,p2,p3 holds
ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )

proof end;

theorem Th61: :: EUCLID_3:61

for n being Nat
for p1, p2, p3, p0 being Point of (TOP-REAL n) st ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 ) holds
p0 in plane p1,p2,p3

proof end;

theorem :: EUCLID_3:62

for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds plane p1,p2,p3 = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }

proof end;

theorem Th63: :: EUCLID_3:63

for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
plane p1,p2,p3 = REAL 2

proof end;

definition

let n be Nat;
let p1, p2, p3, p be Point of (TOP-REAL n);
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 & p in plane p1,p2,p3 ) ;
func tricord1 p1,p2,p3,p -> Real means :Def11: :: EUCLID_3:def 11
ex a2, a3 being Real st
( (it + a2) + a3 = 1 & p = ((it * p1) + (a2 * p2)) + (a3 * p3) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines tricord1 EUCLID_3:def 11 :

definition

let n be Nat;
let p1, p2, p3, p be Point of (TOP-REAL n);
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 & p in plane p1,p2,p3 ) ;
func tricord2 p1,p2,p3,p -> Real means :Def12: :: EUCLID_3:def 12
ex a1, a3 being Real st
( (a1 + it) + a3 = 1 & p = ((a1 * p1) + (it * p2)) + (a3 * p3) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines tricord2 EUCLID_3:def 12 :

definition

let n be Nat;
let p1, p2, p3, p be Point of (TOP-REAL n);
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 & p in plane p1,p2,p3 ) ;
func tricord3 p1,p2,p3,p -> Real means :Def13: :: EUCLID_3:def 13
ex a1, a2 being Real st
( (a1 + a2) + it = 1 & p = ((a1 * p1) + (a2 * p2)) + (it * p3) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines tricord3 EUCLID_3:def 13 :

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
func trcmap1 p1,p2,p3 -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 14
for p being Point of (TOP-REAL 2) holds it . p = tricord1 p1,p2,p3,p;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines trcmap1 EUCLID_3:def 14 :

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
func trcmap2 p1,p2,p3 -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 15
for p being Point of (TOP-REAL 2) holds it . p = tricord2 p1,p2,p3,p;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines trcmap2 EUCLID_3:def 15 :

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
func trcmap3 p1,p2,p3 -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 16
for p being Point of (TOP-REAL 2) holds it . p = tricord3 p1,p2,p3,p;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines trcmap3 EUCLID_3:def 16 :

theorem :: EUCLID_3:64

for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in outside_of_triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 ) )

proof end;

theorem Th65: :: EUCLID_3:65

for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in Triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p >= 0 & tricord2 p1,p2,p3,p >= 0 & tricord3 p1,p2,p3,p >= 0 & ( tricord1 p1,p2,p3,p = 0 or tricord2 p1,p2,p3,p = 0 or tricord3 p1,p2,p3,p = 0 ) ) )

proof end;

theorem :: EUCLID_3:66

for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in Triangle p1,p2,p3 iff ( ( tricord1 p1,p2,p3,p = 0 & tricord2 p1,p2,p3,p >= 0 & tricord3 p1,p2,p3,p >= 0 ) or ( tricord1 p1,p2,p3,p >= 0 & tricord2 p1,p2,p3,p = 0 & tricord3 p1,p2,p3,p >= 0 ) or ( tricord1 p1,p2,p3,p >= 0 & tricord2 p1,p2,p3,p >= 0 & tricord3 p1,p2,p3,p = 0 ) ) ) by Th65;

theorem Th67: :: EUCLID_3:67

for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in inside_of_triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p > 0 & tricord2 p1,p2,p3,p > 0 & tricord3 p1,p2,p3,p > 0 ) )

proof end;

theorem :: EUCLID_3:68

for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
not inside_of_triangle p1,p2,p3 is empty

proof end;