:: Heron's Formula and Ptolemy's Theorem
:: by Marco Riccardi
::
:: Copyright (c) 2008-2021 Association of Mizar Users

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

proof end;

Lm2: for p1, p2 being Point of () holds |.(p1 - p2).| = |.(p2 - p1).|
proof end;

theorem Th1: :: EUCLID_6:1
for p1, p2, p3, p4, p5, p6 being Point of () 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 () 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 () holds cos (angle (p1,p2,p3)) = cos (angle (p3,p2,p1))
proof end;

Lm3: for p1, p2, p3, p4, p5, p6 being Point of () 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 () 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 () 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 () holds not angle (p1,p2,p3) = (2 * (angle (p4,p5,p6))) - (6 * PI)
proof end;

Lm7: for p1, p2, p3 being Point of ()
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 () 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 () 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 ()
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 ();
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 () 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 ();
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 () 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 () 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 () 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 ()
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 () 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 () 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 () 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 ()
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 () st p in (LSeg (p1,p2)) /\ (circle (a,b,r))

proof end;

theorem Th11: :: EUCLID_6:11
for p1, p2, p being Point of () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 ()
for f being Function of (),R^1 st ( for q being Point of () holds f . q = |.(q - q1).| ) holds
f is continuous

proof end;

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

proof end;

theorem Th25: :: EUCLID_6:25
for p1, p2, p3, p being Point of () 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 () 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 () 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 () st p in LSeg (p1,p2) & not p3 in LSeg (p1,p2) holds
ex p4 being Point of () 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 ()
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 () 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 ()
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 ()
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 ()
for a, b, r being Real st p1 in circle (a,b,r) & r > 0 holds
ex p2 being Point of () 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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 () 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 () holds
( |.(p1 - p2).| = 0 iff p1 = p2 ) by Lm1;

theorem :: EUCLID_6:43
for p1, p2 being Point of () holds |.(p1 - p2).| = |.(p2 - p1).| by Lm2;

theorem :: EUCLID_6:44
for p1, p2, p3, p4, p5, p6 being Point of () 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 () 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 () 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 () 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 ()
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 ()
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 ()
for f being Function of (),R^1 st ( for q being Point of () 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 () ex f being Function of (),R^1 st
( ( for q being Point of () holds f . q = |.(q - q1).| ) & f is continuous ) by Lm21;