<abstract xmlns="http://www.w3.org/1999/xhtml"> We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius of the Morley’s trisector triangle are formalized [3]. Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the centroid (the common point of the medians [4]) of a triangle.</abstract>

We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius of the Morley’s trisector triangle are formalized [3]. Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the centroid (the common point of the medians [4]) of a triangle.

Circumcenter, Circumcircle and Centroid of a Triangle

Rue de la Brasserie 5 7100 La Louvière, Belgium

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Circumcenter, Circumcircle and Centroid of a Triangle"}

We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector...

Circumcenter, Circumcircle and Centroid of a Triangle

Publié en ligne: 31 août 2016

Pages: 17 - 26

Reçu: 30 déc. 2015

DOI: https://doi.org/10.1515/forma-2016-0002

Mots clés
Euclidean geometry, perpendicular bisector, circumcenter, circumcircle, centroid, extended law of sines

© by Roland Coghetto

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Circumcenter, Circumcircle and Centroid of a Triangle

Publié en ligne: 31 août 2016

Pages: 17 - 26

Reçu: 30 déc. 2015

DOI: https://doi.org/10.1515/forma-2016-0002

Mots clésEuclidean geometry, perpendicular bisector, circumcenter, circumcircle, centroid, extended law of sines

© by Roland Coghetto

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Mots clés
Euclidean geometry, perpendicular bisector, circumcenter, circumcircle, centroid, extended law of sines