:: Heron's Formula and Ptolemy's Theorem
:: by Marco Riccardi
::
:: Received January 10, 2008
:: Copyright (c) 2008-2021 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 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 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, p2, p3, p4 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;

:: Meister-Gauss formula

definition

let p1, p2, p3 be Point of (TOP-REAL 2);

:: Meister-Gauss formula (for triangles

func the_area_of_polygon3 (p1,p2,p3) -> Real 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;
;

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 equals :: EUCLID_6:def 2
(|.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).|;

correctness
coherence
(|.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).| is Real;
;

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

:: Area

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 p1, p2, 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;

:: Law of Cosines
:: Law of Cosines

theorem Th7: :: EUCLID_6:7

for p1, p2, p3 being Point of (TOP-REAL 2)
for a, b, c being Real 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 p1, p2, p 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 p1, p2, p3, p 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 p1, p2, p3, p 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 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, p2, p 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 p1, p3, p4, p 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 p1, p2, p3, p 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 p1, p2, p3, p 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;

:: Vertical angles

theorem Th15: :: EUCLID_6:15

for p1, p2, p3, p4, p 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;

:: The Isosceles Triangle Theorem A

theorem Th16: :: EUCLID_6:16

for p1, p2, p3 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, p2, p3, 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;

:: The Isosceles Triangle Theorem B
:: Isosceles Triangle Theorem

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 V be RealLinearSpace;

end;

:: deftheorem EUCLID_6:def 3 :
canceled;

notation

let V be RealLinearSpace;
let p1, p2, p3 be Element of V;
antonym p1,p2,p3 is_a_triangle for p1,p2,p3 are_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_distinct & angle (p1,p2,p3) <> PI & angle (p2,p3,p1) <> PI & angle (p3,p1,p2) <> PI ) )

proof end;

Lm18: for p1, p2, p3, p4, p5, p6 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 p1, p2, p3, 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_distinct & 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_distinct & 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 p1, p2, p3, p 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 p1, p2, p3, p 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 p1, p2, p3, p 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 p1, p2, p3, p 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 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 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 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;

:: opposite point on circle

theorem Th32: :: EUCLID_6:32

for p1 being Point of (TOP-REAL 2)
for a, b, r being Real 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;

:: The centre angle and the inscribed angle

theorem Th33: :: EUCLID_6:33

for p1, p2, p, pc being Point of (TOP-REAL 2)
for a, b, r being Real 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;

:: Angles subtended by the same chord

theorem Th34: :: EUCLID_6:34

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, r being Real 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 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 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 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 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_distinct 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 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;

:: Intersecting Chords Theorem or
:: Product of Segments of Chords
:: Intersecting chords theorem

theorem :: EUCLID_6:38

for p1, p2, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being Real 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;

:: Heron's formula
:: Heron's Formula

theorem :: EUCLID_6:39

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

proof end;

:: Ptolemy's Theorem
:: Ptolemy's Theorem

theorem :: EUCLID_6:40

for p1, p2, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being Real 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;