avewright/proofwiki-math huggingface dataset:
Theorem: Complex Logarithm of 1

:$\ln 1 = \set {2 k \pi i: k \in \Z}$

Proof:
Denote as $\ln_\R$ the real natural logarithm.
{{begin-eqn}}
{{eqn | l = \map \ln {r e^{i \theta} }
      | r = \set {\map {\ln_\R} r + i \theta + 2 k \pi i: k \in \Z}
      | c = {{Defof|Natural Logarithm/Complex|index = 1|Complex Natural Logarithm}}
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 e^{i \times 0} }
      | r = \set {\map {\ln_\R} 1 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = substituting $r = 1$ and $\theta = 0$
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 e^{i \times \paren {0 + 0 i} } }
      | r = \set {\map {\ln_\R} 1 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = {{Defof|Wholly Real}}
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 e^0}
      | r = \set {\map {\ln_\R} 1 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 \times \paren {1 + 0 i} }
      | r = \set {\map {\ln_\R} 1 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = {{Defof|Exponential Function/Complex|subdef = Differential Equation|Complex Exponential Function}}
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 \times 1}
      | r = \set {\map {\ln_\R} 1 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = {{Defof|Wholly Real}}
}}
{{eqn | ll= \leadsto
      | l = \ln 1
      | r = \set {\map {\ln_\R} 1 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = Real Multiplication Identity is One
}}
{{eqn | ll= \leadsto
      | l = \ln 1
      | r = \set {0 + i \times 0 + 2 k \pi i: k \in \Z}
      | c = Real Logarithm of $1$ is $0$
}}
{{eqn | ll= \leadsto
      | l = \ln 1
      | r = \set {2 k \pi i: k \in \Z}
      | c = Complex Addition Identity is Zero
}}
{{end-eqn}}
{{qed}}
Category:Logarithms
8lijuvzhn33d01fy949u155wwtagk7m
Theorem: Derivative of Constant/Complex

Let $\map {f_c} z$ be the constant function on an open domain $D \in \C$, where $c \in \C$.
Then:
:$\forall z \in D : \map { {f_c}'} z = 0$

Proof:
The function $f_c: D \to \C$ is defined as:
:$\forall z \in D: \map {f_c} z = c$
Thus:
{{begin-eqn}}
{{eqn | l = \map { {f_c}'} z
      | r = \lim_{h \mathop \to 0} \frac {\map {f_c} {z + h} - \map {f_c} z} h
      | c = {{Defof|Derivative of Complex Function}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {c - c} h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac 0 h
      | c =
}}
{{eqn | r = 0
      | c =
}}
{{end-eqn}}
{{qed}}
Category:Complex Differential Calculus
Category:Constant Mappings
5bhpqpihsa829trer9bl30wj985gyvq
Theorem: Derivative of Identity Function/Real

Let $I_\R: \R \to \R$ be the identity mapping on the real numbers $\R$.
Then:
:$\map {I_\R'} x = 1$

Proof:
The identity mapping is defined as:
:$\forall x \in \R: \map {I_\R} x = x$
Thus:
{{begin-eqn}}
{{eqn | l = \map {I_\R'} x
      | r = \lim_{\delta x \mathop \to 0} \frac {\map {I_\R} {x + \delta x} - \map {I_\R} x} {\delta x}
      | c = {{Defof|Derivative of Real Function}}
}}
{{eqn | r = \lim_{\delta x \mathop \to 0} \frac {\paren {x + \delta x} - x} {\delta x}
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \lim_{\delta x \mathop \to 0} \frac {\delta x} {\delta x}
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Derivatives
Category:Identity Mappings
n4p8n98zloc33ds2cfdnpl5nslhgl0j
Theorem: Derivative of Identity Function/Complex

Let $I_\C: \C \to \C$ be the identity function.
Then:
:$\map {I_\C'} z = 1$

Proof:
The identity function is defined as $\forall x \in \C: \map {I_\C} z = z$.
Thus:
{{begin-eqn}}
{{eqn | l = \map {I_\C'} z
      | r = \lim_{h \mathop \to 0} \frac {\map {I_\C} {z + h} - \map {I_\C} z} h
      | c = {{Defof|Derivative of Complex Function}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {z + h} - z} h
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac h h
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Complex Differential Calculus
Category:Identity Mappings
rwwv6z76gpzlj2aty5j2asdl08t1d2t
Theorem: Chain Rule for Real-Valued Functions/Corollary

Let $\Psi$ represent a differentiable function of $x$ and $y$.
Let $y$ represent a differentiable function of $x$.
Then:
{{begin-eqn}}
{{eqn | l = \frac {\d \Psi} {\d x}
      | r = \frac {\partial \Psi} {\partial x} + \frac {\partial \Psi} {\partial y} \frac {\d y} {\d x}
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\d \Psi} {\d x}
      | r = \frac {\partial \Psi} {\partial x} \frac {\d x} {\d x} + \frac {\partial \Psi} {\partial y} \frac {\d y} {\d x}
      | c = Chain Rule for Real-Valued Functions
}}
{{eqn | r = \frac {\partial \Psi} {\partial x} + \frac {\partial \Psi} {\partial y} \frac {\d y} {\d x}
      | c = Derivative of Identity Function
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Periodic Function

Let $f$ be periodic, that is:
:$\exists T \in \R_{\ne 0}: \forall x \in \R: \map f x = \map f {x + T}$
Then:
:$\laptrans {\map f t} = \dfrac 1 {1 - e^{-s T} } \ds \int_0^T e^{-s t} \map f t \rd t$
where $\laptrans {\map f t}$ denotes the Laplace transform.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f t}
      | r = \int_0^{\infty} e^{-s t} \map f t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \sum_{k \mathop = 0}^{\infty} \int_{k T}^{\paren {k + 1} T} e^{-s t} \map f t \rd t
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions: Corollary
}}
{{eqn | r = \sum_{k \mathop = 0}^{\infty} \int_0^T e^{-s \paren {t + k T} } \map f {t + k T} \rd t
      | c = Change of Limits of Integration
}}
{{eqn | r = \sum_{k \mathop = 0}^{\infty} \int_0^T e^{-s \paren {t + k T} } \map f t \rd t
      | c = General Periodicity Property
}}
{{eqn | r = \sum_{k \mathop = 0}^{\infty} \int_0^T e^{-s t - s k T} \map f t \rd t
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = \sum_{k \mathop = 0}^{\infty} \int_0^T e^{-s t} e^{- s k T} \map f t \rd t
      | c = Product of Powers
}}
{{eqn | r = \sum_{k \mathop = 0}^{\infty} e^{- s k T} \int_0^T e^{-s t} \map f t \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \paren {\int_0^T e^{-s t} \map f t \rd t} \sum_{k \mathop = 0}^{\infty} e^{- s k T}
      | c = Scaling of Summations
}}
{{eqn | r = \paren {\int_0^T e^{-s t} \map f t \rd t} \sum_{k \mathop = 0}^{\infty} \paren {e^{- s T} }^k
      | c = Power of Power
}}
{{eqn | r = \paren {\int_0^T e^{-s t} \map f t \rd t} \paren {\frac 1 {1 - e^{-s T} } }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \frac 1 {1 - e^{-s T} } \int_0^T e^{-s t} \map f t \rd t
      | c = Real Multiplication is Commutative
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Periodic Function

Let $f$ be periodic, that is:
:$\exists T \in \R_{\ne 0}: \forall x \in \R: \map f x = \map f {x + T}$
Then:
:$\laptrans {\map f t} = \dfrac 1 {1 - e^{-s T} } \ds \int_0^T e^{-s t} \map f t \rd t$
where $\laptrans {\map f t}$ denotes the Laplace transform.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f t}
      | r = \int_0^{\infty} e^{-s t} \map f t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + \int_T^{\infty} e^{-s t} \map f t \rd t
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + \int_0^{\infty} e^{-s \paren {t + T} } \map f {t + T} \rd t
      | c = Change of Limits of Integration
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + \int_0^{\infty} e^{-s \paren {t + T} } \map f t \rd t
      | c = {{Defof|Real Periodic Function}}
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + \int_0^{\infty} e^{-s t - s T} \map f t \rd t
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + \int_0^{\infty} e^{-s t} e^{-s T} \map f t \rd t
      | c = Product of Powers
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + e^{-s T} \int_0^{\infty} e^{-s t} \map f t \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + e^{-s T} \laptrans {\map f t}
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | ll= \leadsto
      | l = \paren {1 - e^{-s T} } \laptrans {\map f t}
      | r = \int_0^T e^{-s t} \map f t \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = \frac 1 {1 - e^{-s T} } \int_0^T e^{-s t} \map f t \rd t
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Periodic Function

Let $f$ be periodic, that is:
:$\exists T \in \R_{\ne 0}: \forall x \in \R: \map f x = \map f {x + T}$
Then:
:$\laptrans {\map f t} = \dfrac 1 {1 - e^{-s T} } \ds \int_0^T e^{-s t} \map f t \rd t$
where $\laptrans {\map f t}$ denotes the Laplace transform.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f t}
      | r = \int_0^{\infty} e^{-s t} \map f t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^T e^{-s t} \map f t \rd t + \int_T^{2 T} e^{-s t} \map f t \rd t + \int_{2 T}^{3 T} e^{-s t} \map f t \rd t + \dotsb
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = \int_0^T e^{-s u} \map f u \rd t + \int_T^{2 T} e^{-s \paren {u + T} } \map f {u + T} \rd u + \int_{2 T}^{3 T} e^{-s \paren {u + 2 T} } \map f {u + 2 T} \rd u + \dotsb
      | c = Integration by Substitution: $t = u$, $t = u + T$, $t = u + 2 T$, $\ldots$
}}
{{eqn | r = \int_0^T e^{-s u} \map f u \rd t + e^{-s T} \int_0^T e^{-s u} \map f u \rd u + e^{-2 s T} \int_0^T e^{-s u} \map f u \rd u + \dotsb
      | c = Second Translation Property of Laplace Transforms, and adjusting limits of integration
}}
{{eqn | r = \paren {1 + e^{-s T} + e^{-2 s T} + \dotsb} \int_0^T e^{-s u} \map f u \rd u
      | c = simplifying
}}
{{eqn | r = \frac 1 {1 - e^{-s T} } \int_0^T e^{-s t} \map f t \rd t
      | c = Sum of Infinite Geometric Sequence
}}
{{end-eqn}}
{{qed}}
Theorem: Triangle is Medial Triangle of Larger Triangle

Let $\triangle ABC$ be a triangle.
$\triangle ABC$ is the medial triangle of a larger triangle.

Proof:
By {{EuclidPostulateLink|Fifth}}, it is possible to construct exactly one straight line parallel to each of $AC$, $BC$ and $AC$.
:500px
From Parallelism implies Equal Corresponding Angles:
:$\angle ABC = \angle ECB = \angle DAB$
:$\angle ACB = \angle CBE = \angle CAF$
:$\angle CAB = \angle ABD = \angle ACF$
By Triangle Angle-Side-Angle Congruence:
:$\triangle ABC = \triangle ABD$
:$\triangle ABC = \triangle CFA$
:$\triangle ABC = \triangle ECB$
Thus:
:$FC = CE$
:$DB = BE$
:$FA = AD$
The result follows by definition of medial triangle.
{{qed}}
Theorem: Altitudes of Triangle Meet at Point

Let $\triangle ABC$ be a triangle.
The altitudes of $\triangle ABC$ all intersect at the same point.

Proof:
300px
In $\triangle ABC$ construct the altitude from vertex $A$ to side $BC$ at $P$.
Also draw the altitude from vertex $B$ to side $AC$ at $Q$.
By Two Straight Lines make Equal Opposite Angles:
:$\angle AOQ = \angle BOP$
Given:
:$\angle AQO = \angle BPO = $ one right angle.
By Triangles with Two Equal Angles are Similar:
:$\triangle AOQ \sim \triangle BOP$
and:
:$\triangle AOQ \sim \triangle ACP \sim \triangle BOP$
By the definition of similarity:
:$\dfrac {OP} {BP} = \dfrac {CP} {AP}$
Rearrange:
:$OP = \dfrac {BP \cdot CP} {AP}$
Note there is no term related to side $AC$.
If we had used side $AB$ instead of $AC$, we would have the same result.
Therefore, the altitude from vertex $C$ to side $AB$ meets both $AP$ and $BQ$ at $O$.
{{qed}}
Theorem: Perpendicular Bisectors of Triangle Meet at Point

Let $\triangle ABC$ be a triangle.
The perpendicular bisectors of $AB$, $BC$ and $AC$ all intersect at the same point.

Proof:
Let the perpendicular bisectors of $AC$ and $AB$ be constructed through $D$ and $E$ respectively to meet at $F$.
:500px
By definition of perpendicular bisector:
:$AE = EB$
and:
:$\angle AEF = \angle BEF$ are right angles.
From Triangle Side-Angle-Side Congruence:
:$\triangle AEF = \triangle BEF$
and so $AF = BF$.
Similarly, by definition of perpendicular bisector:
:$AD = DC$
and:
:$\angle ADF = \angle CDF$ are right angles.
From Triangle Side-Angle-Side Congruence:
:$\triangle ADF = \triangle CDF$
and so $AF = CF$.
Thus:
:$BF = CF$
Let $FG$ be the angle bisector of $\angle BFC$.
We have:
:$BF = CF$ from above
and:
:$\angle BFG = \angle CFG$ by construction
Thus by Triangle Side-Angle-Side Congruence:
:$\triangle BFG = \triangle CFG$
and so $BG = CG$.
Thus as $\angle BGF = \angle CGF$ it follows that they are both right angles.
Thus $FG$ is the perpendicular bisector of $BC$.
Thus we have all three perpendicular bisectors of the sides of $ABC$ meeting at the same point $G$.
{{qed}}
Theorem: Centroid of Triangle is Centroid of Medial

Let $\triangle ABC$ be a triangle.
Let $\triangle DEF$ be the medial triangle of $\triangle ABC$.
Let $G$ be the centroid of $\triangle ABC$.
Then $G$ is also the centroid of $\triangle DEF$.

Proof:
:500px
By definition of centroid and medial triangle, the lines $AE$, $BF$ and $CD$ intersect at $G$.
It remains to be shown that $AE$, $BF$ and $CD$ bisect the sides of $DF$, $DE$ and $EF$ respectively.
{{WLOG}}, let $AE$ intersect $DF$ at $H$.
From the working of Triangle is Medial Triangle of Larger Triangle, we have that:
:$DE \parallel AF$
:$EF \parallel AD$
and so $\Box ADEF$ is a parallelogram whose diagonals are $DF$ and $AE$.
From Diameters of Parallelogram Bisect each other, $AE$ bisects $DF$ at $H$.
Similarly:
:$BF$ bisects $DE$
:$DC$ bisects $EF$.
Hence the result.
{{qed}}
Category:Medial Triangles
Category:Centroids of Triangles
2c11pj1gjodspx0ze0u3d6irn660nc4
Theorem: Diameters of Parallelogram Bisect each other

Let $\Box ABCD$ be a parallelogram with diameters $AC$ and $BD$.
Let $AC$ and $BD$ intersect at $E$.
Then $E$ is the midpoint of both $AC$ and $BD$.

Proof:
:400px
By definition of parallelogram:
By Opposite Sides and Angles of Parallelogram are Equal:
:$AB = CD$
:$AD = BC$
:$\angle ABC = \angle ADC$
:$\angle BAD = \angle BCD$
Therefore by Triangle Side-Angle-Side Congruence:
:$\triangle ABC = \triangle ADC$
:$\triangle BAD = \triangle BCD$
Thus:
:$\angle ADE = \angle CBE$
:$\angle DAE = \angle BCE$
We have $AD = BC$.
So from Triangle Angle-Side-Angle Congruence:
:$\triangle ADE = \triangle CBE$
and so:
:$DE = BE$
:$AE = CE$
Hence the result.
{{qed}}
Theorem: Diameters of Parallelogram Bisect each other

Let $\Box ABCD$ be a parallelogram with diameters $AC$ and $BD$.
Let $AC$ and $BD$ intersect at $E$.
Then $E$ is the midpoint of both $AC$ and $BD$.

Proof:
:300px
Let $\Box ABCD$ be embedded in the complex plane such that $B$ is identified with the origin $0 + 0 i$.
Let $A$ be identified with the complex number $z_1$.
Let $C$ be identified with the complex number $z_2$.
By Geometrical Interpretation of Complex Subtraction:
:$z_1 - z_2 = AC$
Then:
:$AE = m \paren {z_1 - z_2}$
for some $m$ where $0 \le m \le 1$.
Similarly, by Geometrical Interpretation of Complex Addition:
:$z_1 + z_2 = BD$
Then:
:$BE = n \paren {z_1 + z_2}$
for some $n$ where $0 \le n \le 1$.
Then:
{{begin-eqn}}
{{eqn | l = BA + AE
      | r = BE
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 + m \paren {z_1 - z_2}
      | r = n \paren {z_1 + z_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {1 - m - n} z_1 + \paren {m - n} z_2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1 - m - n
      | r = 0
      | c = Linear Combination of Non-Parallel Complex Numbers is Zero if Factors are Both Zero
}}
{{eqn | l = m - n
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m
      | r = \frac 1 2
      | c = 
}}
{{eqn | l = n
      | r = \frac 1 2
      | c = 
}}
{{end-eqn}}
and so $E$ is at the midpoint of the diameters of $\Box ABCD$.
{{qed}}
Theorem: Circumcenter of Triangle is Orthocenter of Medial

Let $\triangle ABC$ be a triangle.
Let $\triangle DEF$ be the medial triangle of $\triangle ABC$.
Let $K$ be the circumcenter of $\triangle ABC$.
Then $K$ is the orthocenter of $\triangle DEF$.

Proof:
:500px
Let $FG$, $DH$ and $EJ$ be the perpendicular bisectors of the sides of $AC$, $AB$ and $BC$ respectively.
From Circumscribing Circle about Triangle, the point $K$ where they intersect is the circumcenter of $\triangle ABC$.
From Perpendicular Bisector of Triangle is Altitude of Medial Triangle, $FG$, $DH$ and $EJ$ are the altitudes of $\triangle DEF$.
The result follows by definition of orthocenter.
{{qed}}
Category:Circumcircles of Triangles
Category:Orthocenters of Triangles
Category:Medial Triangles
pn6yqwueu426yqsaa9vz0xwgsd1lioq
Theorem: Position of Centroid on Euler Line

Let $\triangle ABC$ be a triangle which is not equilateral.
Let $O$ be the circumcenter of $\triangle ABC$.
Let $G$ be the centroid of $\triangle ABC$.
Let $H$ be the orthocenter of $\triangle ABC$.
Then $G$ lies on the straight line connecting $O$ and $H$ such that:
:$OG : GH = 1 : 2$
The line $OGH$ is the '''Euler line''' of $\triangle ABC$.

Proof:
First it is necessary to dispose of the case where $\triangle ABC$ is equilateral.
From Orthocenter, Centroid and Circumcenter Coincide iff Triangle is Equilateral, in that case $O$, $G$ and $H$ are the same point.
For all other triangles, $O$, $G$ and $H$ are distinct.
:500px
Let $A'$ be the midpoint of $BC$.
Let $B'$ be the midpoint of $AC$.
By definition of centroid, $G$ is the point at which $AA'$ and $BB'$ intersect.
By Circumscribing Circle about Triangle, $O$ is the point at which the perpendicular bisectors of $AC$ and $BC$ intersect.
By construction, the perpendicular bisectors of $BC$ and $AC$ pass through $A'$ and $B'$ respectively.
Let $OG$ be produced to $H$ such that $OG : HG = 1 : 2$.
It will be demonstrated that $H$ is the orthocenter of $\triangle ABC$.
Draw $AH$ and produce it to intersect $BC$ at $P$.
From Medians of Triangle Meet at Centroid:
:$A'G : AG = 1 : 2$
Consider $\triangle A'OG$ and $\triangle AHG$.
From above:
:$OG : HG = A'G : AG$
From Two Straight Lines make Equal Opposite Angles:
:$\angle OGA' = \angle HGA$
From Triangles with One Equal Angle and Two Sides Proportional are Similar:
:$\triangle A'OG$ and $\triangle AHG$ are similar.
Thus:
:$\angle GHA = \angle GOA'$
From Equal Alternate Angles implies Parallel Lines:
:$AH \parallel A'O$
From Parallelism implies Equal Corresponding Angles:
:$\angle APC = \angle OA'C$
As $OA'$ is perpendicular to $BC$, it follows that $AP$ is also perpendicular to $BC$.
Thus $AP$ is a straight line through $A$ perpendicular to $BC$.
So by definition $AP$ is an altitude of $\triangle ABC$ which passes through $H$.
Similarly, draw $BH$ and produce it to intersect $AC$ at $Q$.
By a similar analysis of the triangles $\triangle B'OG$ and $\triangle BHG$:
:$BQ$ is an altitude of $\triangle ABC$ which passes through $H$.
From Altitudes of Triangle Meet at Point, the altitude of $\triangle ABC$ from $C$ to $AB$ likewise will pass through $H$.
Thus $H$ is by definition the orthocenter of $\triangle ABC$.
By construction, $OGH$ is a straight line such that:
:$OG : GH = 1 : 2$
Hence the result.
{{qed}}
Theorem: Perpendicular Bisector of Triangle is Altitude of Medial Triangle

Let $\triangle ABC$ be a triangle.
Let $\triangle DEF$ be the medial triangle of $\triangle ABC$.
Let a perpendicular bisector be constructed on $AC$ at $F$ to intersect $DE$ at $P$.
Then $FP$ is an altitude of $\triangle DEF$.

Proof:
:500px
Consider the triangles $\triangle ABC$ and $\triangle DBE$.
By the Midline Theorem:
:$BA : BD = 2 : 1$
:$BC : BE = 2 : 1$
and:
:$AC \parallel DE$
From Parallelism implies Equal Alternate Angles:
:$\angle AFP = \angle FPE$
By construction, $\angle AFP$ is a right angle.
Thus $\angle FPE$ is also a right angle.
That is, $FP$ is perpendicular to $DE$.
By construction, $FP$ passes through the vertex $F$ of $\triangle DEF$.
The result follows by definition of altitude of triangle.
{{qed}}
Category:Perpendicular Bisectors
Category:Medial Triangles
3s7e7oglzywhd9tn5wy5arc1wrprhip
Theorem: Orthocenter, Centroid and Circumcenter Coincide iff Triangle is Equilateral

Let $\triangle ABC$ be a triangle.
Let $O$ be the circumcenter of $\triangle ABC$.
Let $G$ be the centroid of $\triangle ABC$.
Let $H$ be the orthocenter of $\triangle ABC$.
Then $O$, $G$ and $H$ are the same points {{iff}} $\triangle ABC$ is equilateral.
If $\triangle ABC$ is not equilateral, then $O$, $G$ and $H$ are all distinct.

Proof:
=== Necessary Condition ===
Let $\triangle ABC$ be an equilateral triangle.
By definition, each side of $\triangle ABC$ is the base of an isosceles triangle.
:400px
Let $AE$, $BF$ and $CD$ be the altitudes of $\triangle ABC$ through $A$, $B$ and $C$ respectively.
From Altitudes of Triangle Meet at Point, let them intersect at $G$.
From Altitude, Median and Perpendicular Bisector Coincide iff Triangle is Isosceles:
:$AE$, $BF$ and $CD$ are the medians of $\triangle ABC$
and:
:$AE$, $BF$ and $CD$ are the perpendicular bisectors of $\triangle ABC$.
They all meet at a single point, that is $G$.
Hence by definition, the circumcenter, centroid and orthocenter of $\triangle ABC$ are the same point.
{{qed|lemma}}
Theorem: Altitude, Median and Perpendicular Bisector Coincide iff Triangle is Isosceles

Let $\triangle ABC$ be a triangle.
Then:
::the altitude from $AB$ to $C$
::the median from $AB$ to $C$
::the perpendicular bisector of $AB$
:are all the same straight line
{{iff}}:
:$\triangle ABC$ is isosceles where $AB$ is the base.

Proof:
=== Necessary Condition ===
Let $\triangle ABC$ be an isosceles triangle whose base is $AB$.
Let $D$ be the midpoint of $AB$.
:300px
By definition of isosceles triangle, $AC = BC$.
We have $AD = DB$ by construction, and $CD$ is common.
So by Triangle Side-Side-Side Congruence:
:$\triangle ACD = \triangle BCD$
From Two Angles on Straight Line make Two Right Angles:
:$\angle ADC + \angle BDC$ equals two right angles
and as $\angle ADC = \angle BDC$ they are each both right angles.
Thus $CD$ is the perpendicular bisector of $AB$.
By definition:
:As $D$ is the midpoint of $AB$, $CD$ is the median from $AB$ to $C$.
:As $CD$ is perpendicular to $AB$ and passes through $C$, which is a vertex of $\triangle ABC$, $CD$ is the altitude from $AB$ to $C$.
Thus all three lines coincide.
{{qed|lemma}}
Theorem: Three Regular Tessellations

There exist exactly $3$ regular tessellations of the plane.

Proof:
Let $m$ be the number of sides of each of the regular polygons that form the regular tessellation.
Let $n$ be the number of those regular polygons which meet at each vertex.
From Internal Angles of Regular Polygon, the internal angles of each polygon measure $\dfrac {\paren {m - 2} 180 \degrees} m$.
The sum of the internal angles at a point is equal to $360 \degrees$ by Sum of Angles between Straight Lines at Point form Four Right Angles
So:
{{begin-eqn}}
{{eqn | l = n \paren {\dfrac {\paren {m - 2} 180 \degrees} m}
      | r = 360 \degrees
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {m - 2} m
      | r = \dfrac 2 n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1 - \dfrac 2 m
      | r = \dfrac 2 n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 m + \dfrac 1 n
      | r = \dfrac 1 2
      | c = 
}}
{{end-eqn}}
But $m$ and $n$ are both greater than $2$.
So:
:if $m = 3$, $n = 6$.
:if $m = 4$, $n = 4$.
:if $m = 5$, $n = \dfrac {10} 3$, which is not an integer.
:if $m = 6$, $n = 3$.
Now suppose $m > 6$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac 1 m + \dfrac 1 n
      | r = \dfrac 1 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 6 + \dfrac 1 n
      | o = >
      | r = \dfrac 1 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 n
      | o = >
      | r = \dfrac 1 3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 3
      | o = >
      | r = n
      | c = 
}}
{{end-eqn}}
But there are no integers between $2$ and $3$, so $m \not > 6$.
There are $3$ possibilities in all.
Therefore all regular tessellations have been accounted for.
{{qed}}