:: by Roland Coghetto

::

:: Received November 29, 2014

:: Copyright (c) 2014-2018 Association of Mizar Users

Lm1: angle (|[0,0]|,|[0,1]|,|[((sqrt 3) / 2),(1 / 2)]|) < PI

proof end;

Lm2: |.|[((sqrt 3) / 2),(1 / 2)]|.| = 1

proof end;

Lm3: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| holds

( |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1 )

proof end;

Lm4: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| holds

( O <> A & A <> B & O <> B & A <> O & B <> A & B <> O )

proof end;

Lm5: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| holds

( angle (B,O,A) = angle (O,A,B) & angle (O,A,B) = angle (A,B,O) )

proof end;

Lm6: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| & angle (O,A,B) < PI holds

angle (B,O,A) = PI / 3

proof end;

theorem :: EUCLID10:20

theorem Thm17: :: EUCLID10:25

for x, y, z being Real st (x + y) + z = PI holds

(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem :: EUCLID10:26

for x, y, z being Real st (x - y) + z = PI holds

(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem :: EUCLID10:27

for x, y, z being Real st (x - ((- (2 * PI)) + y)) + z = PI holds

(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem :: EUCLID10:28

for x, y, z being Real st ((PI - x) - (PI - y)) + z = PI holds

(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

Lm7: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

angle (A,B,C) <> 0

proof end;

theorem Thm19: :: EUCLID10:30

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

( not angle (A,B,C) is zero & not angle (B,C,A) is zero & not angle (C,A,B) is zero & not angle (A,C,B) is zero & not angle (C,B,A) is zero & not angle (B,A,C) is zero )

( not angle (A,B,C) is zero & not angle (B,C,A) is zero & not angle (C,A,B) is zero & not angle (A,C,B) is zero & not angle (C,B,A) is zero & not angle (B,A,C) is zero )

proof end;

Lm9: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) )

proof end;

theorem Thm20: :: EUCLID10:31

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) & angle (C,A,B) = (2 * PI) - (angle (B,A,C)) & angle (B,A,C) = (2 * PI) - (angle (C,A,B)) & angle (A,C,B) = (2 * PI) - (angle (B,C,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) )

( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) & angle (C,A,B) = (2 * PI) - (angle (B,A,C)) & angle (B,A,C) = (2 * PI) - (angle (C,A,B)) & angle (A,C,B) = (2 * PI) - (angle (B,C,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) )

proof end;

theorem :: EUCLID10:32

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((B - A),(C - A))| = 0 & not |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| holds

|.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).|

|.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).|

proof end;

theorem :: EUCLID10:33

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds

(angle (C,B,A)) + (angle (A,C,B)) = PI / 2

(angle (C,B,A)) + (angle (A,C,B)) = PI / 2

proof end;

theorem Thm21: :: EUCLID10:34

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds

( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| & |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| )

( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| & |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| )

proof end;

theorem :: EUCLID10:35

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds

( tan (angle (A,C,B)) = |.(A - B).| / |.(A - C).| & tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).| )

( tan (angle (A,C,B)) = |.(A - B).| / |.(A - C).| & tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).| )

proof end;

registration
end;

theorem Thm24: :: EUCLID10:37

for A, B, C being Point of (TOP-REAL 2)

for a, b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) holds

r is positive

for a, b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) holds

r is positive

proof end;

theorem Thm25: :: EUCLID10:38

for A being Point of (TOP-REAL 2)

for a, b being Real

for r being positive Real st A in circle (a,b,r) holds

A <> |[a,b]|

for a, b being Real

for r being positive Real st A in circle (a,b,r) holds

A <> |[a,b]|

proof end;

theorem :: EUCLID10:39

for A, B, C being Point of (TOP-REAL 2)

for a, b, r being Real st A,B,C is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & |[a,b]| in LSeg (A,C) holds

angle (C,B,A) = PI / 2

for a, b, r being Real st A,B,C is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & |[a,b]| in LSeg (A,C) holds

angle (C,B,A) = PI / 2

proof end;

theorem Thm26: :: EUCLID10:40

for A, B, C being Point of (TOP-REAL 2)

for r being positive Real st not angle (A,B,C) is zero holds

sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C)))))

for r being positive Real st not angle (A,B,C) is zero holds

sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C)))))

proof end;

theorem :: EUCLID10:41

for A, B, C being Point of (TOP-REAL 2) st not angle (A,B,C) is zero holds

sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))

sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))

proof end;

theorem Thm27: :: EUCLID10:42

for A, B, C being Point of (TOP-REAL 2) holds

( the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (B,C,A) & the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (C,A,B) )

( the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (B,C,A) & the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (C,A,B) )

proof end;

theorem Thm28: :: EUCLID10:43

for A, B, C being Point of (TOP-REAL 2) holds the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 (B,A,C))

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);

coherence

(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C)) is Real;

;

end;
::: assume A,B,C is_a_triangle;

func the_diameter_of_the_circumcircle (A,B,C) -> Real equals :: EUCLID10:def 1

(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));

correctness (((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));

coherence

(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C)) is Real;

;

:: deftheorem defines the_diameter_of_the_circumcircle EUCLID10:def 1 :

for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = (((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));

for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = (((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));

theorem Thm29: :: EUCLID10:44

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A)))

the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A)))

proof end;

theorem :: EUCLID10:45

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_diameter_of_the_circumcircle (A,B,C) = - (|.(C - A).| / (sin (angle (A,B,C))))

the_diameter_of_the_circumcircle (A,B,C) = - (|.(C - A).| / (sin (angle (A,B,C))))

proof end;

theorem :: EUCLID10:46

for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,C,A) by Thm27;

theorem Thm31: :: EUCLID10:47

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C))

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C))

proof end;

theorem Thm32: :: EUCLID10:48

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (A,C,B))

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (A,C,B))

proof end;

theorem Thm33: :: EUCLID10:49

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (C,B,A))

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (C,B,A))

proof end;

Lm10: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

|.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B)))

proof end;

theorem Thm34: :: EUCLID10:50

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

( |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) & |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) & |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) )

( |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) & |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) & |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) )

proof end;

theorem :: EUCLID10:51

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

|.(A - B).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3)))

|.(A - B).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3)))

proof end;

theorem :: EUCLID10:52

for A, B, C, P being Point of (TOP-REAL 2) st A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI holds

|.(A - P).| * (sin (PI - (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

|.(A - P).| * (sin (PI - (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

proof end;

Lm11: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,A) < PI holds

( ((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = PI & ((angle (C,A,B)) + (angle (A,B,C))) + (angle (B,C,A)) = 5 * PI )

proof end;

Lm12: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,A) < PI holds

(((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3

proof end;

theorem Thm35: :: EUCLID10:53

for A, B, C, P being Point of (TOP-REAL 2) st A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI & (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 holds

|.(A - P).| * (sin (((2 * PI) / 3) + ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

|.(A - P).| * (sin (((2 * PI) / 3) + ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

proof end;

theorem :: EUCLID10:54

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,A,B) < PI holds

( ((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = 5 * PI & ((angle (C,A,B)) + (angle (A,B,C))) + (angle (B,C,A)) = PI )

( ((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = 5 * PI & ((angle (C,A,B)) + (angle (A,B,C))) + (angle (B,C,A)) = PI )

proof end;

theorem :: EUCLID10:55

for A, B, C, P being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,A) < PI & A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI holds

|.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

|.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

proof end;

theorem :: EUCLID10:56

for A, B, C, P being Point of (TOP-REAL 2) st A,B,C is_a_triangle & A,B,P is_a_triangle & angle (C,B,A) < PI & angle (A,P,B) < PI & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 holds

|.(A - P).| = - (((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3)))

|.(A - P).| = - (((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3)))

proof end;

theorem Thm37: :: EUCLID10:57

for A, B, C being Point of (TOP-REAL 2) st A,B,C are_mutually_distinct & C in LSeg (A,B) holds

|.(A - B).| = |.(A - C).| + |.(C - B).|

|.(A - B).| = |.(A - C).| + |.(C - B).|

proof end;

theorem Thm38: :: EUCLID10:58

for A, B being Point of (TOP-REAL 2)

for a, b being Real

for r being positive Real st A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) holds

|.(A - B).| = 2 * r

for a, b being Real

for r being positive Real st A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) holds

|.(A - B).| = 2 * r

proof end;

theorem :: EUCLID10:59

for a, b being Real

for r being positive Real

for C being Subset of (Euclid 2) st C = circle (a,b,r) holds

diameter C = 2 * r

for r being positive Real

for C being Subset of (Euclid 2) st C = circle (a,b,r) holds

diameter C = 2 * r

proof end;