:: EUCLID_6 semantic presentation

Lm1: for p1, p2 being Point of (TOP-REAL 2) holds
( |.(p1 - p2).| = 0 iff p1 = p2 )

proof end;

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

proof end;

theorem Th1: :: EUCLID_6:1

for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) st sin (angle p1,p2,p3) = sin (angle p4,p5,p6) & cos (angle p1,p2,p3) = cos (angle p4,p5,p6) holds
angle p1,p2,p3 = angle p4,p5,p6

proof end;

theorem Th2: :: EUCLID_6:2

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

proof end;

theorem Th3: :: EUCLID_6:3

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

proof end;

Lm3: for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) + (2 * PI )

proof end;

Lm4: for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) + (4 * PI )

proof end;

Lm5: for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) - (4 * PI )

proof end;

Lm6: for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) - (6 * PI )

proof end;

Lm7: for p1, p2, p3 being Point of (TOP-REAL 2)
for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
angle p1,p2,p3 = angle c1,c2

proof end;

Lm8: for c1, c2 being Element of COMPLEX st c2 = 0 holds
Arg (Rotate c2,(- (Arg c1))) = 0

proof end;

Lm9: for c1, c2 being Element of COMPLEX st c2 = 0 & Arg c1 = 0 holds
angle c1,c2 = 0

proof end;

Lm10: for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) >= 0 holds
Arg (Rotate c2,(- (Arg c1))) = (Arg c2) - (Arg c1)

proof end;

Lm11: for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) >= 0 holds
angle c1,c2 = (Arg c2) - (Arg c1)

proof end;

Lm12: for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) < 0 holds
Arg (Rotate c2,(- (Arg c1))) = ((2 * PI ) - (Arg c1)) + (Arg c2)

proof end;

Lm13: for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) < 0 holds
angle c1,c2 = ((2 * PI ) - (Arg c1)) + (Arg c2)

proof end;

Lm14: for c1, c2, c3 being Element of COMPLEX holds
( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

proof end;

theorem Th4: :: EUCLID_6:4

for p1, p4, p2, p3 being Point of (TOP-REAL 2) holds
( (angle p1,p4,p2) + (angle p2,p4,p3) = angle p1,p4,p3 or (angle p1,p4,p2) + (angle p2,p4,p3) = (angle p1,p4,p3) + (2 * PI ) )

proof end;

Lm15: for p1, p2 being Point of (TOP-REAL 2) holds
( (p1 - p2) `1 = (p1 `1 ) - (p2 `1 ) & (p1 - p2) `2 = (p1 `2 ) - (p2 `2 ) )

proof end;

Lm16: for p1, p2, p3 being Point of (TOP-REAL 2)
for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
( Re (c1 .|. c2) = (((p1 `1 ) - (p2 `1 )) * ((p3 `1 ) - (p2 `1 ))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `2 ) - (p2 `2 ))) & Im (c1 .|. c2) = (- (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 ))) & |.c1.| = sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 )) & |.(p1 - p2).| = |.c1.| )

proof end;

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
func the_area_of_polygon3 p1,p2,p3 -> real number equals :: EUCLID_6:def 1
(((((p1 `1 ) * (p2 `2 )) - ((p2 `1 ) * (p1 `2 ))) + (((p2 `1 ) * (p3 `2 )) - ((p3 `1 ) * (p2 `2 )))) + (((p3 `1 ) * (p1 `2 )) - ((p1 `1 ) * (p3 `2 )))) / 2;
correctness ;

end;

:: deftheorem defines the_area_of_polygon3 EUCLID_6:def 1 :

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
func the_perimeter_of_polygon3 p1,p2,p3 -> real number equals :: EUCLID_6:def 2
(|.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).|;
correctness ;

end;

:: deftheorem defines the_perimeter_of_polygon3 EUCLID_6:def 2 :

theorem Th5: :: EUCLID_6:5

for p1, p2, p3 being Point of (TOP-REAL 2) holds the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2

proof end;

theorem Th6: :: EUCLID_6:6

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

proof end;

theorem Th7: :: EUCLID_6:7

for p1, p2, p3 being Point of (TOP-REAL 2)
for a, b, c being real number st a = |.(p1 - p2).| & b = |.(p3 - p2).| & c = |.(p3 - p1).| holds
c ^2 = ((a ^2 ) + (b ^2 )) - (((2 * a) * b) * (cos (angle p1,p2,p3)))

proof end;

theorem Th8: :: EUCLID_6:8

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

proof end;

theorem Th9: :: EUCLID_6:9

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

proof end;

theorem Th10: :: EUCLID_6:10

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

proof end;

Lm17: for p1, p2 being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in inside_of_circle a,b,r & p2 in outside_of_circle a,b,r holds
ex p being Point of (TOP-REAL 2) st p in (LSeg p1,p2) /\ (circle a,b,r)

proof end;

theorem Th11: :: EUCLID_6:11

for p1, p, p2 being Point of (TOP-REAL 2) st angle p1,p,p2 = PI holds
p in LSeg p1,p2

proof end;

theorem Th12: :: EUCLID_6:12

for p, p1, p3, p4 being Point of (TOP-REAL 2) st p in LSeg p1,p3 & p in LSeg p1,p4 & p3 <> p4 & p <> p1 & not p3 in LSeg p1,p4 holds
p4 in LSeg p1,p3

proof end;

theorem Th13: :: EUCLID_6:13

for p, p1, p3, p2 being Point of (TOP-REAL 2) st p in LSeg p1,p3 & p <> p1 & p <> p3 & not (angle p1,p,p2) + (angle p2,p,p3) = PI holds
(angle p1,p,p2) + (angle p2,p,p3) = 3 * PI

proof end;

theorem Th14: :: EUCLID_6:14

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

proof end;

theorem Th15: :: EUCLID_6:15

for p, p1, p3, p2, p4 being Point of (TOP-REAL 2) st p in LSeg p1,p3 & p in LSeg p2,p4 & p <> p1 & p <> p2 & p <> p3 & p <> p4 holds
angle p1,p,p2 = angle p3,p,p4

proof end;

theorem Th16: :: EUCLID_6:16

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

proof end;

theorem Th17: :: EUCLID_6:17

for p1, p2, p3, p being Point of (TOP-REAL 2) st p in LSeg p1,p2 & p <> p2 holds
( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 )

proof end;

theorem Th18: :: EUCLID_6:18

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

proof end;

theorem :: EUCLID_6:19

for p1, p2, p3, p being Point of (TOP-REAL 2) st |.(p1 - p3).| = |.(p2 - p3).| & p in LSeg p1,p2 & p <> p3 holds
( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) )

proof end;

definition

let p1, p2, p3 be Point of (TOP-REAL 2);
pred p1,p2,p3 is_collinear means :Def3: :: EUCLID_6:def 3
( p1 in LSeg p2,p3 or p2 in LSeg p3,p1 or p3 in LSeg p1,p2 );

end;

:: deftheorem Def3 defines is_collinear EUCLID_6:def 3 :

notation

let p1, p2, p3 be Point of (TOP-REAL 2);
antonym p1,p2,p3 is_a_triangle for p1,p2,p3 is_collinear ;

end;

theorem Th20: :: EUCLID_6:20

for p1, p2, p3 being Point of (TOP-REAL 2) holds
( p1,p2,p3 is_a_triangle iff ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI ) )

proof end;

Lm18: for p3, p2, p1, p5, p6, p4 being Point of (TOP-REAL 2) st p3 <> p2 & p3 <> p1 & p2 <> p1 & p5 <> p6 & p5 <> p4 & p6 <> p4 & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI & angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p6,p4,p5 holds
|.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|

proof end;

theorem Th21: :: EUCLID_6:21

for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) st p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p6,p4,p5 holds
( |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| & |.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| & |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| )

proof end;

Lm19: for p3, p2, p1, p4, p5, p6 being Point of (TOP-REAL 2) st p3 <> p2 & p3 <> p1 & p2 <> p1 & p4 <> p5 & p4 <> p6 & p5 <> p6 & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI & angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p5,p6,p4 holds
|.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).|

proof end;

theorem Th22: :: EUCLID_6:22

for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) st p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p5,p6,p4 holds
( |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| & |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| )

proof end;

theorem Th23: :: EUCLID_6:23

for p1, p2, p3 being Point of (TOP-REAL 2) st p1,p2,p3