avewright/proofwiki-math huggingface dataset:
Theorem: Definite Integral from 0 to 2 Pi of Logarithm of a plus b Cosine x

:$\ds \int_0^{2 \pi} \map \ln {a + b \cos x} \rd x = 2 \pi \map \ln {\frac {a + \sqrt {a^2 - b^2} } 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^{2 \pi} \map \ln {a + b \cos x} \rd x
      | r = \int_0^\pi \map \ln {a + b \cos x} \rd x + \int_\pi^{2 \pi} \map \ln {a + b \cos x} \rd x
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = \int_0^\pi \map \ln {a + b \cos x} \rd x - \int_\pi^0 \map \ln {a + b \map \cos {2 \pi - x} } \rd x
      | c = substituting $x \mapsto 2 \pi - x$
}}
{{eqn | r = \int_0^\pi \map \ln {a + b \cos x} \rd x + \int_0^\pi \map \ln {a + b \map \cos {2 \pi - x} } \rd x
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = \int_0^\pi \map \ln {a + b \cos x} \rd x + \int_0^\pi \map \ln {a + b \cos x} \rd x
      | c = Cosine of Conjugate Angle
}}
{{eqn | r = 2 \int_0^\pi \map \ln {a + b \cos x} \rd x
}}
{{eqn | r = 2 \pi \map \ln {\frac {a + \sqrt {a^2 - b^2} } 2}
      | c = Definite Integral from 0 to Pi of Logarithm of a plus b Cosine x
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Pi of Sec x by Logarithm of One plus b Cosine x over One plus a Cosine x

:$\ds \int_0^{\pi/2} \sec x \map \ln {\frac {1 + b \cos x} {1 + a \cos x} } \rd x = \frac 1 2 \paren {\paren {\arccos a}^2 - \paren {\arccos b}^2}$

Proof:
Note that by Difference of Logarithms: 
:$\ds \int_0^{\pi/2} \sec x \map \ln {\frac {1 + b \cos x} {1 + a \cos x} } \rd x = \int_0^{\pi/2} \sec x \map \ln {1 + b \cos x} \rd x - \int_0^{\pi/2} \sec \map \ln {1 + a \cos x} \rd x$
For each $\alpha \in \openint {-1} 1$, set: 
:$\ds \map I \alpha = \int_0^{\pi/2} \sec x \map \ln {1 + \alpha \cos x} \rd x$
Then: 
:$\ds \int_0^{\pi/2} \sec x \map \ln {\frac {1 + b \cos x} {1 + a \cos x} } \rd x = \map I b - \map I a$
We have: 
{{begin-eqn}}
{{eqn | l = \map {I'} \alpha
      | r = \frac \d {\d \alpha} \int_0^{\pi/2} \sec x \map \ln {1 + \alpha \cos x} \rd x
}}
{{eqn | r = \int_0^{\pi/2} \frac \partial {\partial \alpha} \paren {\sec x \map \ln {1 + \alpha \cos x} } \rd x
      | c = Definite Integral of Partial Derivative
}}
{{eqn | r = \int_0^{\pi/2} \frac {\cos x \sec x} {1 + \alpha \cos x} \rd x
      | c = Chain Rule for Derivatives, Derivative of Natural Logarithm
}}
{{eqn | r = \int_0^{\pi/2} \frac 1 {1 + \alpha \cos x} \rd x
}}
{{eqn | r = \frac {\arccos \alpha} {\sqrt {1 - \alpha^2} }
      | c = Definite Integral from $0$ to $\dfrac \pi 2$ of $\dfrac 1 {a + b \cos x}$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map I b - \map I a
      | r = \int_a^b \map {I'} \alpha \rd \alpha
      | c = Fundamental Theorem of Calculus: Second Part
}}
{{eqn | r = \int_a^b \frac {\arccos \alpha} {\sqrt {1 - \alpha^2} } \rd \alpha
}}
{{end-eqn}}
From Derivative of Arccosine Function, we have: 
:$\ds \frac \d {\d \alpha} \arccos \alpha = -\frac 1 {\sqrt {1 - \alpha^2} }$
so:
{{begin-eqn}}
{{eqn | l = \int_a^b \frac {\arccos \alpha} {\sqrt {1 - \alpha^2} } \rd \alpha
      | r = \int_{\arccos a}^{\arccos b} x \frac {-\sqrt {1 - \alpha^2} } {\sqrt {1 - \alpha^2} } \rd x
      | c = substituting $x = \arccos \alpha$
}}
{{eqn | r = -\int_{\arccos a}^{\arccos b} x \rd x
}}
{{eqn | r = \intlimits {-\frac {x^2} 2} {\arccos a} {\arccos b}
      | c = Primitive of Power
}}
{{eqn | r = \frac 1 2 \paren {\paren {\arccos a}^2 - \paren {\arccos b}^2}
}}
{{end-eqn}}
so:
:$\ds \int_0^{\pi/2} \sec x \map \ln {\frac {1 + b \cos x} {1 + a \cos x} } \rd x = \frac 1 2 \paren {\paren {\arccos a}^2 - \paren {\arccos b}^2}$
as required.
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x minus Exponential of -b x over x by Secant of p x

:$\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } {x \sec p x} \rd x = \frac 1 2 \map \ln {\frac {b^2 + p^2} {a^2 + p^2} }$

Proof:
Fix $p$ and set: 
:$\ds \map I \alpha = \int_0^\infty \frac {e^{-\alpha x} } {x \sec p x} \rd x$
for all $\alpha \ge 0$.
Then: 
:$\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } {x \sec p x} \rd x = \map I a - \map I b$
We have: 
{{begin-eqn}}
{{eqn	| l = \map {I'} \alpha
	| r = \frac \d {\d \alpha} \int_0^\infty \frac {e^{-\alpha x} } {x \sec p x} \rd x
}}
{{eqn	| r = \int_0^\infty \frac \partial {\partial \alpha} \paren {\frac {e^{-\alpha x} } {x \sec p x} } \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = -\int_0^\infty e^{-\alpha x} \cos p x \rd x
	| c = Derivative of $e^{a x}$, {{Defof|Secant Function}}
}}
{{eqn	| r = -\frac \alpha {\alpha^2 + p^2}
	| c = Definite Integral to Infinity of $e^{-a x} \cos b x$
}}
{{end-eqn}}
so:
{{begin-eqn}}
{{eqn	| l = \map I \alpha
	| r = -\int \frac \alpha {\alpha^2 + p^2} \rd \alpha
}}
{{eqn	| r = -\frac 1 2 \map \ln {\alpha^2 + p^2} + C
	| c = Primitive of $\dfrac x {x^2 + a^2}$
}}
{{end-eqn}}
for all $\alpha \ge 0$, for some constant $C \in \R$.
We then have: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {e^{-a x} - e^{-b x} } {x \sec p x} \rd x
	| r = \map I a - \map I b
}}
{{eqn	| r = \paren {-\frac 1 2 \map \ln {a^2 + p^2} + C} - \paren {-\frac 1 2 \map \ln {b^2 + p^2} + C}
}}
{{eqn	| r = \frac 1 2 \paren {\map \ln {b^2 + p^2} - \map \ln {a^2 + p^2} }
}}
{{eqn	| r = \frac 1 2 \map \ln {\frac {b^2 + p^2} {a^2 + p^2} }
	| c = Difference of Logarithms
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Cosine p x minus Cosine q x over x Squared

:$\ds \int_0^\infty \frac {\cos p x - \cos q x} {x^2} \rd x = \frac {\pi \paren {\size q - \size p} } 2$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\cos p x - \cos q x} {x^2} \rd x
	| r = \int_0^\infty \frac {1 - \cos q x - \paren {1 - \cos p x} } {x^2} \rd x
}}
{{eqn	| r = \int_0^\infty \frac {1 - \cos q x} {x^2} \rd x - \int_0^\infty \frac {1 - \cos p x} {x^2} \rd x
}}
{{eqn	| r = \frac \pi 2 \size q - \frac \pi 2 \size p
	| c = Integral to Infinity of $\dfrac {1 - \cos p x} {x^2}$
}}
{{eqn	| r = \frac {\pi \paren {\size q - \size p} } 2
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x minus Exponential of -b x over x by Cosecant of p x

:$\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } {x \csc p x} \rd x = \arctan \frac b p - \arctan \frac a p$

Proof:
Fix $p$ and set: 
:$\ds \map I \alpha = \int_0^\infty \frac {e^{-\alpha x} } {x \csc p x} \rd x$
for all $\alpha \ge 0$.
Then: 
:$\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } {x \csc p x} \rd x = \map I a - \map I b$
We have: 
{{begin-eqn}}
{{eqn	| l = \map {I'} \alpha
	| r = \frac \d {\d \alpha} \int_0^\infty \frac {e^{-\alpha x} } {x \csc p x} \rd x
}}
{{eqn	| r = \int_0^\infty \frac \partial {\partial \alpha} \paren {\frac {e^{-\alpha x} } {x \csc p x} } \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = -\int_0^\infty e^{-\alpha x} \sin p x \rd x
	| c = Derivative of $e^{a x}$, {{Defof|Cosecant/Real Function|Cosecant}}
}}
{{eqn	| r = -\frac p {\alpha^2 + p^2}
	| c = Definite Integral to Infinity of $e^{-a x} \sin b x$
}}
{{end-eqn}}
so:
{{begin-eqn}}
{{eqn	| l = \map I \alpha
	| r = -p \int \frac 1 {\alpha^2 + p^2} \rd \alpha
}}
{{eqn	| r = -\arctan \frac \alpha p + C
	| c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{end-eqn}}
for all $\alpha \ge 0$ and constant $C \in \R$.
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {e^{-a x} - e^{-b x} } {x \csc p x} \rd x
	| r = \map I a - \map I b
}}
{{eqn	| r = \paren {-\arctan \frac a p + C} - \paren {-\arctan \frac b p + C}
}}
{{eqn	| r = \arctan \frac b p - \arctan \frac a p
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral of Periodic Function

Let $f$ be a Darboux integrable periodic function with period $L$.
Let $\alpha \in \R$ and $n \in \Z$.
Then:
:$\ds \int_\alpha^{\alpha + n L} \map f x \d x = n \int_0^L \map f x \d x$

Proof:
For $n \ge 0$:
{{begin-eqn}}
{{eqn | l = \int_\alpha^{\alpha + n L} \map f x \d x
      | r = \int_\alpha^0 \map f x \d x + \sum_{k \mathop = 0}^{n - 1} \int_{k L}^{\paren {k + 1} L} \map f x \d x + \int_{n L}^{\alpha + n L} \map f x \d x
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions/Corollary
}}
{{eqn | r = \int_\alpha^0 \map f x \d x + \sum_{k \mathop = 0}^{n - 1} \int_{k L}^{\paren {k + 1} L} \map f {x - k L} \d x + \int_{n L}^{\alpha + n L} \map f {x - n L} \d x
      | c = General Periodicity Property
}}
{{eqn | r = \int_\alpha^0 \map f x \d x + \sum_{k \mathop = 0}^{n - 1} \int_0^L \map f x \d x + \int_0^\alpha \map f x \d x
      | c = Integration by Substitution
}}
{{eqn | r = n \int_0^L \map f x \d x
      | c = Reversal of Limits of Definite Integral
}}
{{end-eqn}}
For $n < 0$:
{{begin-eqn}}
{{eqn | l = \int_\alpha^{\alpha + n L} \map f x \d x
      | r = -\int_{\alpha + n L}^\alpha \map f x \d x
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = -\int_{\alpha + n L}^{\alpha + n L + \paren {-n L} } \map f x \d x
}}
{{eqn | r = -\paren {-n \int_0^L \map f x \d x}
      | c = by the above; $-n > 0$
}}
{{eqn | r = n \int_0^L \map f x \d x
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Definite Integrals
Category:Periodic Functions
cyyv9y7clx7fcowj4e2viob94dnqll6
Theorem: Independent Subset is Contained in Maximal Independent Subset

Let $M = \struct{S, \mathscr I}$ be a matroid.
Let $A \subseteq S$.
Let $X \in \mathscr I$ such that $X \subseteq A$.
Then:
:$\exists Y \in \mathscr I : X \subseteq Y \subseteq A : \size Y = \map \rho A$
where $\rho$ is the rank function on $M$.

Proof:
By definition of the rank function on $M$:
:$\size X \le \map \rho A$
Theorem: Automorphic Numbers in Base 10

If leading zeroes are allowed, there are exactly $4$ $n$-digit automorphic numbers in base $10$:
:$00 \dots 00$
:$00 \dots 01$
:$5^{2^{n - 1} } \pmod {10^n}$
:$6^{5^{n - 1} } \pmod {10^n}$

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:There are exactly $4$ $n$-digit automorphic numbers of the forms above.
Theorem: Seventeen Horses/General Problem 2

A man dies, leaving $n$ indivisible and indistinguishable objects to be divided among $m$ heirs.
They are to be distributed in the ratio $\dfrac 1 {a_1} : \dfrac 1 {a_2} : \cdots : \dfrac 1 {a_m}$.
Let $t = \dfrac q r = \ds \sum_{k \mathop = 1}^m \dfrac 1 {a_k}$ expressed in canonical form.
Let $t \ne 1$.
Then it is possible to achieve the required share by adding $s$ objects to the existing $n$ such that:
:$s + q = r$
when $q = n$.
This still works whether $q$ is positive or negative.

Proof:
{{ProofWanted|More clarity of exposition is required. Might not even be correct}}
Theorem: Sum from 1 to n of 1 over r(r+1)(r+2)/Corollary

:$\ds \sum_{r \mathop = 1}^\infty \frac 1 {r \paren {r + 1} \paren {r + 2} } = \frac 1 4$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 1}^\infty \frac 1 {r \paren {r + 1} \paren {r + 2} }
      | r = \lim_{n \mathop \to \infty} \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} \paren {r + 2} }
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {n \paren {n + 3} } {4 \paren {n + 1} \paren {n + 2} }
      | c = Sum from $1$ to $n$ of $\dfrac 1 {r \paren {r + 1} \paren {r + 2} }$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {1 + \frac 3 n} {4 \paren {1 + \frac 1 n} \paren {1 + \frac 2 n} }
      | c = dividing top and bottom by $n^2$
}}
{{eqn | r = \frac 1 4
      | c = Basic Null Sequences
}}
{{end-eqn}}
{{qed}}
Category:Sum from 1 to n of 1 over r(r+1)(r+2)
Category:Limits of Series
nbympv30qdpop38sqiwjrun9diy5ocs
Theorem: Heronian Triangle whose Altitude and Sides are Consecutive Integers

There exists exactly one Heronian triangle one of whose altitudes and its sides are all consecutive integers.
This is the Heronian triangle whose sides are $\tuple {13, 14, 15}$ and which has an altitude $12$.

Proof:
We note that a Heronian triangle whose sides are all consecutive integers is also known as a Fleenor-Heronian triangle.
From Sequence of Fleenor-Heronian Triangles, we have that the smallest such triangles are as follows:
:$\tuple {1, 2, 3}$, which has an altitude of $0$
This is the degenerate case where the Heronian triangle is a straight line.
While $0, 1, 2, 3$ is a sequence of $4$ consecutive integers, this is not technically a triangle.
:$\tuple {3, 4, 5}$ with area $6$.
It has altitudes $3$, $4$ and $\dfrac {12} 5$.
:$\tuple {13, 14, 15}$
This can be constructed by placing the $2$ Pythagorean triangles $\tuple {5, 12, 13}$ and $\tuple {9, 12, 15}$ together along their common side $12$:
:500px
Thus the altitude and sides are:
:$\tuple {12, 13, 14, 15}$
and this is the Heronian triangle we seek.
It has area $84$.
The next largest Fleenor-Heronian triangle has sides $\tuple {51, 52, 53}$.
Using Heron's Formula, its area is given by:
:$\AA = \sqrt {78 \times 25 \times 26 \times 27} = 1170$
Hence its altitudes are:
:$45 \frac {45} {51}$, $45$, $44 \frac 8 {53}$
For still larger triangles, the altitudes are never within $1$ unit of the sides:
Consider the triangle with sides $\tuple {a - 1, a, a + 1}$.
Using Heron's Formula, its area is given by:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \sqrt {s \paren {s - a + 1} \paren {s - a} \paren {s - a - 1} }
}}
{{eqn | r = \sqrt {\frac 3 2 a \paren {\frac 1 2 a + 1} \paren {\frac 1 2 a} \paren {\frac 1 2 a - 1} }
}}
{{eqn | r = \frac a 4 \sqrt {3 \paren {a + 2} \paren {a - 2} }
}}
{{eqn | r = \frac a 4 \sqrt {3 a^2 - 12}
}}
{{end-eqn}}
Its longest altitude is therefore:
{{begin-eqn}}
{{eqn | l = \frac {2 a} {4 \paren {a - 1} } \sqrt {3 a^2 - 12}
      | o = <
      | r = \frac {a^2 \sqrt 3} {2 \paren {a - 1} }
}}
{{end-eqn}}
and we have:
{{begin-eqn}}
{{eqn | l = \frac {a^2 \sqrt 3} {2 \paren {a - 1} }
      | o = <
      | r = \paren {a - 1} - 1
}}
{{eqn | ll= \leadstoandfrom
      | l = a^2 \sqrt 3
      | o = <
      | r = 2 \paren {a - 1}^2 - 2 \paren {a - 1}
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 a^2 - 4 a + 2 - 2 a + 2 - \sqrt 3 a^2
      | o = >
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {2 - \sqrt 3} a^2 - 6 a + 4
      | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = a
      | o = >
      | r = \frac {6 + \sqrt {6^2 - 4 \times 4 \paren {2 - \sqrt 3} } } {2 \paren {2 - \sqrt 3} }
      | c = Quadratic Formula
}}
{{eqn | o = \approx
      | r = 21.7
}}
{{end-eqn}}
This shows that for $a \ge 22$, all altitudes of the triangle is less than $a - 2$.
Hence there are no more examples.
{{qed}}
Theorem: Integer Heronian Triangle can be Scaled so Area equals Perimeter

Let $T_1$ be an integer Heronian triangle whose sides are $a$, $b$ and $c$.
Then there exists a rational number $k$ such that the Heronian triangle $T_2$ whose sides are $k a$, $k b$ and $k c$ such that the perimeter of $T$ is equal to the area of $T$.

Proof:
For a given triangle $T$:
:let $\map \AA T$ denote the area of $T$
:let $\map P T$ denote the perimeter of $T$.
We are given that $T_1$ is an integer Heronian triangle whose sides are $a$, $b$ and $c$.
Let $\map P {T_1} = k \map \AA {T_1}$.
Let $T_2$ have sides $k a$, $k b$ and $k c$.
Then we have that:
{{begin-eqn}}
{{eqn | l = \map P {T_2}
      | r = k \map P {T_1}
      | c = 
}}
{{eqn | l = \map A {T_2}
      | r = k^2 \map A {T_1}
      | c = 
}}
{{eqn | r = k \map P {T_1}
      | c = 
}}
{{eqn | r = \map P {T_2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Heronian Triangles
hfgq1h2x4tu21n5ln7trqjwr8qpy72w
Theorem: Heronian Triangle is Similar to Integer Heronian Triangle

Let $\triangle {ABC}$ be a Heronian triangle.
Then there exists an integer Heronian triangle $\triangle {A'B'C'}$ such that $\triangle {ABC}$ and $\triangle {A'B'C'}$ are similar.

Proof:
Let $\triangle {ABC}$ have sides whose lengths are $a$, $b$ and $c$.
By definition of Heronian triangle, each of $a$, $b$ and $c$ are rational.
By definition of rational number, we can express:
:$a = \dfrac {p_a} {q_a}$, $b = \dfrac {p_b} {q_b}$ and $c = \dfrac {p_c} {q_c}$
where each of $p_a, q_a, p_b, q_b, p_c, q_c$ are integers.
Now let:
{{begin-eqn}}
{{eqn | l = a'
      | r = a q_a q_b q_c
      | c = 
}}
{{eqn | l = b'
      | r = b q_a q_b q_c
      | c = 
}}
{{eqn | l = c'
      | r = c q_a q_b q_c
      | c = 
}}
{{end-eqn}}
Let $\triangle {A'B'C'}$ be the triangle whose sides have lengths $a'$, $b'$ and $c'$.
By definition, $\triangle {ABC}$ and $\triangle {A'B'C'}$ are similar.
Each of $a'$, $b'$ and $c'$ are integers.
Consider the area of triangle $\triangle {A'B'C'}$
Let the area of $\triangle {ABC}$ be $A$.
Then the area $\triangle {A'B'C'}$ is $q_a q_b q_c A$, which is rational.
Hence $\triangle {A'B'C'}$ is an integer Heronian triangle.
{{Qed}}
Theorem: Triple with Sum and Product Equal

For $a, b, c \in \Z$, $a \le b \le c$, the solutions to the equation:
:$a + b + c = a b c$
are:
:$\tuple {1, 2, 3}$
:$\tuple {-3, -2, -1}$
and the trivial solution set:
:$\set {\tuple {-z, 0, z}: z \in \N}$

Proof:
Suppose one of $a, b, c$ is zero.
Then $a b c = 0 = a + b + c$.
The remaining two numbers sum to $0$, giving the solution set:
:$\set {\tuple {-z, 0, z}: z \in \N}$
{{qed|lemma}}
Suppose $a < 0$ and $0 < b \le c$.
Then $a b c \le a < a + b + c$.
Hence equality never happens.
Similarly, for $a \le b < 0$ and $c > 0$:
:$a b c \ge c > a + b + c$
Hence equality never happens.
{{qed|lemma}}
Now it remains the case $0 < a \le b \le c$.
Suppose $a \ge 2$.
Then:
{{begin-eqn}}
{{eqn | l = a b c
      | o = \ge
      | r = 4 c
}}
{{eqn | o = \ge
      | r = a + b + c + c
}}
{{eqn | o = >
      | r = a + b + c
}}
{{end-eqn}}
hence $a = 1$.
Suppose $b \ge 3$.
Then:
{{begin-eqn}}
{{eqn | l = b c
      | o = \ge
      | r = c + c + c
}}
{{eqn | o = \ge
      | r = b + c + c
}}
{{eqn | o = >
      | r = b + c
}}
{{end-eqn}}
hence $b = 1$ or $b = 2$.
For $b = 1$:
:$c = 1 + 1 + c$
which is a contradiction.
For $b = 2$:
:$2 c = 1 + 2 + c$
giving $c = 3$.
Therefore $\tuple {1, 2, 3}$ is the only solution for strictly positive integer values of $a, b, c$.
Similarly, for $a \le b \le c < 0$, we have $0 < -c \le -b \le -a$.
Also:
{{begin-eqn}}
{{eqn | l = \paren {-c} + \paren {-b} + \paren {-a}
      | r = -\paren {a + b + c}
}}
{{eqn | r = -a b c
}}
{{eqn | r = \paren {-c} \paren {-b} \paren {-a}
}}
{{end-eqn}}
and we have already show that $-c = 1, -b = 2, -a = 3$.
Therefore we have $\tuple {a, b, c} = \tuple {-3, -2, -1}$.
{{qed|lemma}}
We have considered all possible signs of $a, b, c$.
Hence the result.
{{qed}}
Category:6
9mdcgt479nqmb80i7kkm6nbs95jprdm
Theorem: Triple with Product Quadruple the Sum

Let $a, b, c \in \N$ such that $a \le b \le c$.
Then the solutions to:
:$a b c = 4 \paren {a + b + c}$
are:
:$\tuple {0, 0, 0}, \tuple {1, 5, 24}, \tuple {1, 6, 14}, \tuple {1, 8, 9}, \tuple {2, 3, 10}, \tuple {2, 4, 6}$

Proof:
Suppose $a \ge 4$.
Then:
{{begin-eqn}}
{{eqn | l = a b c
      | o = \ge
      | r = 16 c
      | c = as $4 \le a \le b$
}}
{{eqn | o = \ge
      | r = 4 \paren {a + b + c + c}
      | c = as $a \le b \le c$
}}
{{eqn | o = >
      | r = 4 \paren {a + b + c}
      | c = as $c > 0$
}}
{{end-eqn}}
hence $0 \le a \le 3$.
For $a = 0$, we have $4 \paren {b + c} = 0$.
This forces $b = c = 0$, giving the trivial solution:
:$\tuple {0, 0, 0}$
{{qed|lemma}}
For $a \ge 1$, note that:
{{begin-eqn}}
{{eqn | l = 4 \paren {a + b + c}
      | r = a b c
}}
{{eqn | ll= \leadstoandfrom
      | l = 4 \paren {a + b}
      | r = \paren {a b - 4} c
}}
{{eqn | ll= \leadstoandfrom
      | l = c
      | r = \frac {4 \paren {a + b} } {a b - 4}
}}
{{end-eqn}}
In the second step, {{LHS}} is strictly positive.
Hence $a b > 4$ and the final step is justified.
For $a = 1$, we have $b c = 4 \paren {1 + b + c}$.
Since $a b > 4$, $b > 4$.
Suppose $b \ge 9$.
Then:
{{begin-eqn}}
{{eqn | l = b c
      | o = \ge
      | r = 9 c
}}
{{eqn | o = \ge
      | r = 4 \paren {b + c} + c
      | c = as $b \le c$
}}
{{eqn | o = >
      | r = 4 \paren {1 + b + c}
      | c = as $c \ge b > 4$
}}
{{end-eqn}}
hence $b \le 8$.
We find the value of $c$ by substituting $a$ and $b$:
:$b = 5: c = \dfrac {4 \paren {1 + 5} } {5 - 4} = 24$
:$b = 6: c = \dfrac {4 \paren {1 + 6} } {6 - 4} = 14$
:$b = 7: c = \dfrac {4 \paren {1 + 7} } {7 - 4} = \dfrac {32} 3$
:$b = 8: c = \dfrac {4 \paren {1 + 8} } {8 - 4} = 9$
and we see that $\tuple {1, 5, 24}, \tuple {1, 6, 14}, \tuple {1, 8, 9}$ are valid solutions.
{{qed|lemma}}
For $a = 2$, we have $2 b c = 4 \paren {2 + b + c}$.
Since $a b > 4$, $b > 2$.
Suppose $b \ge 5$.
Then:
{{begin-eqn}}
{{eqn | l = 2 b c
      | o = \ge
      | r = 10 c
}}
{{eqn | o = \ge
      | r = 4 \paren {b + c} + 2 c
      | c = as $b \le c$
}}
{{eqn | o = >
      | r = 4 \paren {2 + b + c}
      | c = as $c \ge b > 4$
}}
{{end-eqn}}
hence $b \le 4$.
We find the value of $c$ by substituting $a$ and $b$:
:$b = 3: c = \dfrac {4 \paren {2 + 3} } {2 \times 3 - 4} = 10$
:$b = 4: c = \dfrac {4 \paren {2 + 4} } {2 \times 4 - 4} = 6$
and we see that $\tuple {2, 3, 10}, \tuple {2, 4, 6}$ are valid solutions.
{{qed|lemma}}
For $a = 3$, we have $3 b c = 4 \paren {3 + b + c}$.
Suppose $b \ge 4$.
Then:
{{begin-eqn}}
{{eqn | l = 3 b c
      | o = \ge
      | r = 12 c
}}
{{eqn | o = \ge
      | r = 4 \paren {b + c} + 4 c
      | c = as $b \le c$
}}
{{eqn | o = >
      | r = 4 \paren {3 + b + c}
      | c = as $c \ge b > 1$
}}
{{end-eqn}}
hence $b \le 3$.
Since $3 = a \le b$, this forces $b = 3$
We find the value of $c$ by substituting $a$ and $b$:
:$c = \dfrac {4 \paren {3 + 3} } {3 \times 3 - 4} = \dfrac {24} 5$
and we see that it is not a valid solution.
{{qed|lemma}}
We have considered all possible values of $a$.
Hence the result.
{{qed}}
mgja9o3yt8d0kuze46853enzwrydbf2
Theorem: Area of Integer Heronian Triangle is Multiple of 6

Let $\triangle {ABC}$ be an integer Heronian triangle.
Then the area of $\triangle {ABC}$ is a multiple of $6$.

Proof:
Heron's Formula gives us that:
:$\AA = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
where:
:$\AA$ denotes the area of the triangle
:$a$, $b$ and $c$ denote the lengths of the sides of the triangle
:$s = \dfrac {a + b + c} 2$ denotes the semiperimeter of the triangle.
We set out to eliminate $s$ and simplify as best possible:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }
      | c = 
}}
{{eqn | l = \AA^2
      | r = \dfrac {a + b + c} 2 \paren {\dfrac {a + b + c} 2 - a} \paren {\dfrac {a + b + c} 2 - b} \paren {\dfrac {a + b + c} 2 - c}
      | c = substituting for $s$ and squaring
}}
{{eqn | ll= \leadsto
      | l = 16 \AA^2
      | r = \paren {a + b + c} \paren {-a + b + c} \paren {a - b + c} \paren {a + b - c}
      | c = multiplying through by $16$ and simplifying
}}
{{eqn | r = 2 a^2 b^2 + 2 b^2 c^2 + 2 c^2 a^2 - a^4 - b^4 - c^4
      | c = multiplying out and simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {4 \AA}^2 + \paren {b^2 + c^2 - a^2}^2
      | r = \paren {2 b c}^2
      | c = factorising
}}
{{end-eqn}}
This is now in the form $p^2 + q^2 = r^2$.
From Solutions of Pythagorean Equation, $\tuple {p, q, r}$ has the parametric solution:
:$\tuple {m^2 - n^2, 2 m n, m^2 + n^2}$
There are two steps to showing $6 \divides \AA$: