:: Heron's Formula and Ptolemy's Theorem
:: by Marco Riccardi
::
:: Received January 10, 2008
:: Copyright (c) 2008 Association of Mizar Users

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
coherence
(((((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 is real number ;
;

end;

:: deftheorem defines the_area_of_polygon3 EUCLID_6:def 1 :

for p1, p2, p3 being Point of (TOP-REAL 2) holds the_area_of_polygon3 p1,p2,p3 = (((((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;

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
coherence
(|.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).| is real number ;
;

end;

:: deftheorem defines the_perimeter_of_polygon3 EUCLID_6:def 2 :

for p1, p2, p3 being Point of (TOP-REAL 2) holds the_perimeter_of_polygon3 p1,p2,p3 = (|.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).|;

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 :

for p1, p2, p3 being Point of (TOP-REAL 2) holds
( p1,p2,p3 is_collinear iff ( p1 in LSeg p2,p3 or p2 in LSeg p3,p1 or p3 in LSeg p1,p2 ) );

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 are_mutually_different & angle p1,p2,p3 <= PI holds
( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI )

proof end;

theorem Th24: :: EUCLID_6:24

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

proof end;

Lm20: for n being Element of NAT
for q1 being Point of (TOP-REAL n)
for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) holds
f is continuous

proof end;

Lm21: for n being Element of NAT
for q1 being Point of (TOP-REAL n) ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous )

proof end;

theorem Th25: :: EUCLID_6:25

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

proof end;

theorem Th26: :: EUCLID_6:26

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

proof end;

theorem Th27: :: EUCLID_6:27

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

proof end;

theorem Th28: :: EUCLID_6:28

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

proof end;

theorem :: EUCLID_6:29

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) by Lm17;

theorem Th30: :: EUCLID_6:30

for p1, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p1,p4 & p3 <> p4 holds
p = p1

proof end;

theorem Th31: :: EUCLID_6:31

for p1, p2, p, pc being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p in circle a,b,r & pc = |[a,b]| & pc in LSeg p,p2 & p1 <> p & not 2 * (angle p1,p,p2) = angle p1,pc,p2 holds
2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2

proof end;

theorem Th32: :: EUCLID_6:32

for p1 being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & r > 0 holds
ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle a,b,r & |[a,b]| in LSeg p1,p2 )

proof end;

theorem Th33: :: EUCLID_6:33

for p1, p2, p, pc being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p in circle a,b,r & pc = |[a,b]| & p1 <> p & p2 <> p & not 2 * (angle p1,p,p2) = angle p1,pc,p2 holds
2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2

proof end;

theorem Th34: :: EUCLID_6:34

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & not angle p1,p3,p2 = angle p1,p4,p2 & not angle p1,p3,p2 = (angle p1,p4,p2) - PI holds
angle p1,p3,p2 = (angle p1,p4,p2) + PI

proof end;

theorem Th35: :: EUCLID_6:35

for p1, p2, p3 being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p1 <> p2 & p2 <> p3 holds
angle p1,p2,p3 <> PI

proof end;

Lm22: for p1, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p1,p4 holds
|.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).|

proof end;

Lm23: for p1, p2, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p1 & p in LSeg p2,p4 holds
|.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|

proof end;

theorem Th36: :: EUCLID_6:36

for p1, p2, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p2,p4 & p1,p2,p3,p4 are_mutually_different holds
angle p1,p4,p2 = angle p1,p3,p2

proof end;

theorem Th37: :: EUCLID_6:37

for p1, p2, p3 being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & angle p1,p2,p3 = 0 & p1 <> p2 & p2 <> p3 holds
p1 = p3

proof end;

theorem :: EUCLID_6:38

for p1, p2, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p2,p4 holds
|.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|

proof end;

theorem :: EUCLID_6:39

for p2, p1, p3 being Point of (TOP-REAL 2)
for a, b, c, s being real number st a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| & s = (the_perimeter_of_polygon3 p1,p2,p3) / 2 holds
abs (the_area_of_polygon3 p1,p2,p3) = sqrt (((s * (s - a)) * (s - b)) * (s - c))

proof end;

theorem :: EUCLID_6:40

for p1, p2, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p2,p4 holds
|.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

proof end;

theorem :: EUCLID_6:41

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

theorem :: EUCLID_6:42

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

theorem :: EUCLID_6:43

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

theorem :: EUCLID_6:44

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 ) by Lm3;

theorem :: EUCLID_6:45

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 ) by Lm4;

theorem :: EUCLID_6:46

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 ) by Lm5;

theorem :: EUCLID_6:47

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 ) by Lm6;

theorem :: EUCLID_6:48

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 by Lm7;

theorem :: EUCLID_6:49

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 ) ) by Lm14;

theorem :: EUCLID_6:50

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.| ) by Lm16;

theorem :: EUCLID_6:51

for n being Element of NAT
for q1 being Point of (TOP-REAL n)
for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) holds
f is continuous by Lm20;

theorem :: EUCLID_6:52

for n being Element of NAT
for q1 being Point of (TOP-REAL n) ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous ) by Lm21;