:: Heron's Formula and Ptolemy's Theorem :: by Marco Riccardi :: :: Received January 10, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin Lm1: for p1, p2 being Point of (TOP-REAL 2) holds ( |.(p1 - p2).| = 0 iff p1 = p2 ) proofend; Lm2: for p1, p2 being Point of (TOP-REAL 2) holds |.(p1 - p2).| = |.(p2 - p1).| proofend; 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) proofend; 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))) proofend; 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)) proofend; 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) proofend; 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) proofend; 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) proofend; 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) proofend; 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) proofend; Lm8: for c1, c2 being Element of COMPLEX st c2 = 0 holds Arg (Rotate (c2,(- (Arg c1)))) = 0 proofend; Lm9: for c1, c2 being Element of COMPLEX st c2 = 0 & Arg c1 = 0 holds angle (c1,c2) = 0 proofend; 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) proofend; Lm11: for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) >= 0 holds angle (c1,c2) = (Arg c2) - (Arg c1) proofend; 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) proofend; 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) proofend; 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) ) proofend; 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) ) proofend; 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) ) proofend; 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.| ) proofend; :: Meister-Gauss formula 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).|; :: 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 proofend; 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))) proofend; :: Law of Cosines :: [WP: ] Law_of_Cosines 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)))) proofend; begin 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 proofend; 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) proofend; 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) proofend; 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)) proofend; 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) proofend; 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) proofend; 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 proofend; 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) proofend; :: Vertical angles 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) proofend; :: The Isosceles Triangle Theorem A 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) proofend; 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 ) proofend; 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) proofend; :: The Isosceles Triangle Theorem B :: [WP: ] 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) ) ) proofend; definition let p1, p2, p3 be Point of (TOP-REAL 2); predp1,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 ) ) proofend; 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).| proofend; 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).| ) proofend; 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).| proofend; 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).| ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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) proofend; 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) proofend; 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) ) proofend; 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 proofend; 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) proofend; :: opposite point on circle 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) ) proofend; :: 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 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) proofend; :: 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 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 proofend; 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 proofend; 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).| proofend; 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).| proofend; 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) proofend; 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 proofend; :: Intersecting Chords Theorem or :: Product of Segments of Chords :: [WP: ] 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 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).| proofend; begin :: Heron's formula :: [WP: ] Heron's_Formula 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)) proofend; :: Ptolemy's Theorem :: [WP: ] 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 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).|) proofend; begin 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;