avewright/proofwiki-math huggingface dataset:
Theorem: Linear Second Order ODE/x^2 y'' + x y' - 4 y = 0

The second order ODE:
:$(1): \quad x^2 y'' + x y' - 4 y = 0$
has the general solution:
:$y = C_1 x^2 + \dfrac {C_2} {x^2}$

Proof:
It can be seen that $(1)$ is an instance of the Cauchy-Euler Equation:
:$x^2 y'' + p x y' + q y = 0$
where:
:$p = 1$
:$q = -4$
By Conversion of Cauchy-Euler Equation to Constant Coefficient Linear ODE, this can be expressed as:
:$\dfrac {\d^2 y} {\d t^2} + \paren {p - 1} \dfrac {\d y} {\d t^2} + q y = 0$
by making the substitution:
:$x = e^t$
Hence it can be expressed as:
:$(2): \quad \dfrac {\d^2 y} {\d t^2} - 4 y = 0$
From Linear Second Order ODE: $y'' - 4 y = 0$, this has the general solution:
{{begin-eqn}}
{{eqn | l = y
      | r = C_1 e^{2 t} + C_2 e^{-2 t}
      | c = 
}}
{{eqn | r = C_1 x^2 + C_2 x^{-2}
      | c = substituting $x = e^t$
}}
{{eqn | r = C_1 x^2 + \frac {C_2} {x^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Legendre's Differential Equation/(1 - x^2) y'' - 2 x y' + 2 y = 0

The special case of Legendre's differential equation:
:$(1): \quad \paren {1 - x^2} y' ' - 2 x y' + 2 y = 0$
has the general solution:
:$y = C_1 x + C_2 \paren {\dfrac x 2 \, \map \ln {\dfrac {1 + x} {1 - x} } - 1}$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = 1
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = 0
      | c = Derivative of Constant
}}
{{end-eqn}}
and so by inspection:
:$y_1 = x$
is a particular solution of $(1)$.
$(1)$ can be expressed as:
:$(2): \quad y' ' - \dfrac {2 x} {1 - x^2} y' + \dfrac 2 {1 - x^2} y = 0$
which is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = - \dfrac {2 x} {1 - x^2}$
:$\map Q x = \dfrac 2 {1 - x^2}$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \paren {-\dfrac {2 x} {1 - x^2} } \rd x
      | c = 
}}
{{eqn | r = \map \ln {1 - x^2}
      | c = Primitive of Function under its Derivative
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-\map \ln {1 - x^2} }
      | c = 
}}
{{eqn | r = \frac 1 {1 - x^2}
      | c =  
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {x^2} \frac 1 {1 - x^2} \rd x
      | c = 
}}
{{eqn | r = \int \dfrac 1 {x^2 \paren {1 - x^2} } \rd x
      | c = 
}}
{{eqn | r = -\frac 1 x + \frac 1 2 \map \ln {\frac {1 + x} {1 - x} }
      | c = Primitive of $\dfrac 1 {x^2 \paren {a^2 - x^2} }$
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = \paren {-\frac 1 x + \frac 1 2 \map \ln {\frac {1 + x} {1 - x} } } x
      | c = 
}}
{{eqn | r = -1 + \frac x 2 \map \ln {\frac {1 + x} {1 - x} }
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 x + C_2 \paren {\dfrac x 2 \, \map \ln {\dfrac {1 + x} {1 - x} } - 1}$
{{qed}}
Theorem: Bessel's Equation/x^2 y'' + x y' + (x^2 - (1 over 4)) y = 0

The special case of Bessel's equation:
:$(1): \quad x^2 y' ' + x y' + \paren {x^2 - \dfrac 1 4} y = 0$
has the general solution:
:$y = C_1 \dfrac {\sin x} {\sqrt x} + C_2 \dfrac {\cos x} {\sqrt x}$

Proof:
=== Particular Solution ===
{{:Bessel's Equation/x^2 y'' + x y' + (x^2 - (1 over 4)) y = 0/Particular Solution}}{{qed|lemma}}
$(1)$ can be expressed as:
:$(2): \quad y' ' + \dfrac 1 x y' + \paren {1 - \dfrac 1 {4 x^2} } y = 0$
which is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = \dfrac 1 x$
:$\map Q x = 1 - \dfrac 1 {4 x^2}$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \dfrac 1 x \rd x
      | c = 
}}
{{eqn | r = \ln x
      | c = Primitive of Reciprocal
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-\ln x}
      | c = 
}}
{{eqn | r = \frac 1 x
      | c =  
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac x {\sin^2 x} \frac 1 x \rd x
      | c = 
}}
{{eqn | r = \int \csc^2 x \rd x
      | c = 
}}
{{eqn | r = \cot x 
      | c = Primitive of $\csc^2 x$
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = \paren {-\cot x} \dfrac {\sin x} {\sqrt x}
      | c = 
}}
{{eqn | r = -\dfrac {\cos x} {\sqrt x}
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 \dfrac {\sin x} {\sqrt x} + C_2 \dfrac {\cos x} {\sqrt x}$
{{qed}}
Theorem: Bessel's Equation/x^2 y'' + x y' + (x^2 - (1 over 4)) y = 0/Particular Solution

The special case of Bessel's equation:
:$(1): \quad x^2 y' ' + x y' + \paren {x^2 - \dfrac 1 4} y = 0$
has a particular solution:
:$y = \dfrac {\sin x} {\sqrt x}$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = \frac {\sin x} {\sqrt x}
      | c = 
}}
{{eqn | r = x^{-1/2} \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = x^{-1/2} \cos x - \frac 1 2 x^{-3/2} \sin x 
      | c = Product Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = -x^{-1/2} \sin x - \frac 1 2 x^{-3/2} \cos x - \frac 1 2 x^{-3/2} \cos x + \frac 3 4 x^{-5/2} \sin x 
      | c = Product Rule for Derivatives
}}
{{eqn | r = \paren {\frac 3 4 x^{-5/2} - x^{-1/2} } \sin x - x^{-3/2} \cos x 
      | c = 
}}
{{eqn | r = \paren {\frac 3 {4 x^2} - 1} x^{-1/2} \sin x - x^{-3/2} \cos x 
      | c = 
}}
{{end-eqn}}
Inserting into $(1)$, and gradually simplifying:
{{begin-eqn}}
{{eqn | o = 
      | r = x^2 \paren {\paren {\frac 3 {4 x^2} - 1} x^{-1/2} \sin x - x^{-3/2} \cos x} + x \paren {x^{-1/2} \cos x - \frac 1 2 x^{-3/2} \sin x} + \paren {x^2 - \dfrac 1 4} x^{-1/2} \sin x
      | c = 
}}
{{eqn | r = \paren {\frac 3 4 - x^2} x^{-1/2} \sin x - x^{1/2} \cos x + x^{1/2} \cos x - \frac 1 2 x^{-1/2} \sin x + x^{3/2} \sin x - \dfrac 1 4 x^{-1/2} \sin x
      | c = 
}}
{{eqn | r = \frac 3 4 x^{-1/2} \sin x - x^{3/2} \sin x - \frac 1 2 x^{-1/2} \sin x + x^{3/2} \sin x - \dfrac 1 4 x^{-1/2} \sin x
      | c = 
}}
{{eqn | r = \frac 3 4 x^{-1/2} \sin x - \frac 1 2 x^{-1/2} \sin x - \dfrac 1 4 x^{-1/2} \sin x
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
hence demonstrating that:
:$y_1 = \dfrac {\sin x} {\sqrt x}$
is a particular solution of $(1)$.
Theorem: Linear Second Order ODE/(x - 1) y'' - y' + y = 0

The second order ODE:
:$(1): \quad \paren {x - 1} y' ' - x y' + y = 0$
has the general solution:
:$y = C_1 x + C_2 e^x$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = 1
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = 0
      | c = Derivative of Constant
}}
{{end-eqn}}
and so by inspection:
:$y_1 = x$
is a particular solution of $(1)$.
$(1)$ can be expressed as:
:$(2): \quad y' ' - \dfrac x {x - 1} y' + \dfrac 1 {x - 1} y = 0$
which is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = -\dfrac x {x - 1}$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \paren {-\dfrac x {x - 1} } \rd x
      | c = 
}}
{{eqn | r = -x - \map \ln {x - 1}
      | c = Primitive of $\dfrac x {a x + b}$
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{x + \map \ln {x - 1} }
      | c = 
}}
{{eqn | r = e^x \paren {x - 1}
      | c =  
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{- \int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {x^2} e^x \paren {x - 1} \rd x
      | c = 
}}
{{eqn | r = \int \paren {\dfrac {e^x} x - \dfrac {e^x} {x^2} } \rd x
      | c = 
}}
{{eqn | r = \int \dfrac {e^x} x \rd x - \int \dfrac {e^x} {x^2} \rd x
      | c = 
}}
{{eqn | r = \int \dfrac {e^x} x \rd x + \frac {e^x} x - \int \frac {e^x} x \rd x
      | c = Primitive of $\dfrac {e^{a x} } {x^n}$
}}
{{eqn | r = \frac {e^x} x
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = \paren {\frac {e^x} x} x
      | c = 
}}
{{eqn | r = e^x
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 x + C_2 e^x$
{{qed}}
</onlyinclude>
Theorem: Linear Second Order ODE/x^2 y'' + 2 x y' - 2 y = 0

The second order ODE:
:$(1): \quad x^2 y'' + 2 x y' - 2 y = 0$
has the general solution:
:$y = C_1 x + \dfrac {C_2} {x^2}$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = 1
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_1}''
      | r = 0
      | c = Derivative of Constant
}}
{{end-eqn}}
and so by inspection:
:$y_1 = x$
is a particular solution of $(1)$.
$(1)$ can be expressed as:
:$(2): \quad y'' + \dfrac 2 x y' - \dfrac 2 {x^2} y = 0$
which is in the form:
:$y'' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = \dfrac 2 x$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \dfrac 2 x \rd x
      | c = 
}}
{{eqn | r = 2 \ln x
      | c = Primitive of Reciprocal
}}
{{eqn | r = \ln {x^2}
      | c = Logarithm of Power
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-\ln {x^2} }
      | c = 
}}
{{eqn | r = \frac 1 {x^2}
      | c =  
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{- \int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {x^2} \frac 1 {x^2} \rd x
      | c = 
}}
{{eqn | r = \int \dfrac 1 {x^4} \rd x
      | c = 
}}
{{eqn | r = -\frac 1 {3 x^3}
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = \paren {-\frac 1 {3 x^3} } x
      | c = 
}}
{{eqn | r = -\frac 1 {3 x^2}
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 x + k \paren {-\dfrac 1 {3 x^2} }$
where $k$ is arbitrary.
Setting $C_2 = -\dfrac k 3$:
:$y = C_1 x + \dfrac {C_2} {x^2}$
{{qed}}
Theorem: Linear Second Order ODE/x^2 y'' + 2 x y' - 2 y = 0

The second order ODE:
:$(1): \quad x^2 y'' + 2 x y' - 2 y = 0$
has the general solution:
:$y = C_1 x + \dfrac {C_2} {x^2}$

Proof:
It can be seen that $(1)$ is an instance of the Cauchy-Euler Equation:
:$x^2 y'' + p x y' + q y = 0$
where:
:$p = 2$
:$q = -2$
By Conversion of Cauchy-Euler Equation to Constant Coefficient Linear ODE, this can be expressed as:
:$\dfrac {\d^2 y} {\d t^2} + \paren {p - 1} \dfrac {\d y} {\d t} + q y = 0$
by making the substitution:
:$x = e^t$
Hence it can be expressed as:
:$(2): \quad \dfrac {\d^2 y} {\d t^2} + \dfrac {\d y} {\d t} - 2 y = 0$
From Linear Second Order ODE: $y'' + y' - 2 y = 0$, this has the general solution:
{{begin-eqn}}
{{eqn | l = y
      | r = C_1 e^t + C_2 e^{-2 t}
      | c = 
}}
{{eqn | r = C_1 x + C_2 x^{-2}
      | c = substituting $x = e^t$
}}
{{eqn | r = C_1 x + \frac {C_2} {x^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/y'' - x f(x) y' + f(x) y = 0

The second order ODE:
:$(1): \quad y' ' - x \, \map f x y' + \map f x y = 0$
has the general solution:
:$\ds y = C_1 x + C_2 x \int x^{-2} e^{\int x \, \map f x \rd x} \rd x$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = 1
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = 0
      | c = Derivative of Constant
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = y' ' - x \map f x y' + \map f x y
      | r = 0 - x \map f x 1 + \map f x x
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
and so it has been demonstrated that:
:$y_1 = x$
is a particular solution of $(1)$.
$(1)$ is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = -x \map f x$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \paren {-x \map f x} \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-\int \paren {-x \map f x} \rd x}
      | c = 
}}
{{eqn | r = e^{\int x \map f x \rd x}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {x^2} e^{\int x \map f x \rd x} \rd x
      | c = as $y_1 = x$
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = x \int x^{-2} e^{\int x \map f x \rd x} \rd x
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$\ds y = C_1 x + C_2 x \int x^{-2} e^{\int x \map f x \rd x} \rd x$
{{qed}}
Theorem: Second Order ODE/x y'' - (2 x + 1) y' + (x + 1) y = 0

The second order ODE:
:$(1): \quad x y' ' - \paren {2 x + 1} y' + \paren {x + 1} y = 0$
has the general solution:
:$y = C_1 e^x + C_2 x^2 e^x$

Proof:
Note that:
:$x - \paren {2 x + 1} + \paren {x + 1} = 0$
so if $y' ' = y' = y$ we find that $(1)$ is satisfied.
So:
{{begin-eqn}}
{{eqn | l = y_1
      | r = e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{end-eqn}}
and so:
:$y_1 = e^x$
is a particular solution of $(1)$.
$(1)$ can be expressed as:
:$(2): \quad y' ' - \dfrac {2 x + 1} x y' + \dfrac {x + 1} x y = 0$
which is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = -\dfrac {2 x + 1} x$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \paren {-\dfrac {2 x + 1} x} \rd x
      | c = 
}}
{{eqn | r = \int \paren {-2 - \dfrac 1 x} \rd x
      | c = 
}}
{{eqn | r = -2 x - \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-\paren {-2 x - \ln x} }
      | c = 
}}
{{eqn | r = e^{2 x + \ln x}
      | c = 
}}
{{eqn | r = e^{2 x} e^{\ln x}
      | c = 
}}
{{eqn | r = x e^{2 x}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {e^{2 x} } x e^{2 x} \rd x
      | c = as $y_1 = e^x$
}}
{{eqn | r = \int x \rd x
      | c = 
}}
{{eqn | r = \frac {x^2} 2
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = \frac {x^2} 2 e^x
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 e^x + k \dfrac {x^2} 2 e^x$
and so setting $C_2 = \dfrac k 2$:
:$y = C_1 e^x + C_2 x^2 e^x$
{{qed}}
Theorem: Second Order ODE/y'' - f(x) y' + (f(x) - 1) y = 0

The second order ODE:
:$(1): \quad y' ' - \map f x y' + \paren {\map f x - 1} y = 0$
has the general solution:
:$\ds y = C_1 e^x + C_2 e^x \int e^{-2 x + \int \map f x \rd x} \rd x$

Proof:
Note that:
:$1 - \map f x + \paren {\map f x - 1} = 0$
so if $y' ' = y' = y$ we find that $(1)$ is satisfied.
So:
{{begin-eqn}}
{{eqn | l = y_1
      | r = e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{end-eqn}}
and so:
:$y_1 = e^x$
is a particular solution of $(1)$.
$(1)$ is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = -\map f x$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \paren {-\map f x} \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-\int \paren {-\map f x} \rd x}
      | c = 
}}
{{eqn | r = e^{\int \map f x \rd x}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {e^{2 x} } e^{\int \map f x \rd x} \rd x
      | c = as $y_1 = e^x$
}}
{{eqn | r = \int e^{-2 x + \int \map f x \rd x} \rd x
      | c = as $y_1 = e^x$
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = e^x \int e^{-2 x + \int \map f x \rd x} \rd x
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$\ds y = C_1 e^x + C_2 e^x \int e^{-2 x + \int \map f x \rd x} \rd x$
{{qed}}
Theorem: Exponential Function is Solution of Constant Coefficient Homogeneous LSOODE iff Index is Root of Auxiliary Equation

Let:
:$(1): \quad y' ' + p y' + q y = 0$
be a constant coefficient homogeneous linear second order ODE.
Then:
:$y = e^{m_1 x}$ is a solution to $(1)$
{{iff}}
:$m_1$ is a root of the auxiliary equation $m^2 + p m + q = 0$

Proof:
Consider the equation:
:$y = e^{m_1 x}$
Differentiating {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = y
      | r = e^{m_1 x}
      | c = 
}}
{{eqn | l = y'
      | r = m_1 e^{m_1 x}
      | c = 
}}
{{eqn | l = y' '
      | r = {m_1}^2 e^{m_1 x}
      | c = 
}}
{{end-eqn}}
Theorem: Solution of Constant Coefficient Homogeneous LSOODE

Let:
:$(1): \quad y' ' + p y' + q y = 0$
be a constant coefficient homogeneous linear second order ODE.
Let $m_1$ and $m_2$ be the roots of the auxiliary equation $m^2 + p m + q = 0$.

Proof:
=== Real Roots of Auxiliary Equation ===
{{:Solution of Constant Coefficient Homogeneous LSOODE/Real Roots of Auxiliary Equation}}{{qed|lemma}}
Theorem: Solution of Constant Coefficient Homogeneous LSOODE/Real Roots of Auxiliary Equation

{{:Solution of Constant Coefficient Homogeneous LSOODE}}
Let $p^2 > 4 q$.
Then $(1)$ has the general solution:
:$y = C_1 e^{m_1 x} + C_2 e^{m_2 x}$

Proof:
Consider the auxiliary equation of $(1)$:
:$(2): \quad m^2 + p m + q$
Let $p^2 > 4 q$.
From Solution to Quadratic Equation with Real Coefficients, $(2)$ has two real roots:
{{begin-eqn}}
{{eqn | l = m_1
      | r = -\frac p 2 + \sqrt {\frac {p^2} 4 - q}
}}
{{eqn | l = m_2
      | r = -\frac p 2 - \sqrt {\frac {p^2} 4 - q}
}}
{{end-eqn}}
As $p^2 > 4 q$ we have that:
:$\sqrt {\dfrac {p^2} 4 - q} \ne 0$
and so:
:$m_1 \ne m_2$
From Exponential Function is Solution of Constant Coefficient Homogeneous LSOODE iff Index is Root of Auxiliary Equation:
{{begin-eqn}}
{{eqn | l = y_1
      | r = e^{m_1 x}
}}
{{eqn | l = y_2
      | r = e^{m_2 x}
}}
{{end-eqn}}
are both particular solutions to $(1)$.
We also have that:
{{begin-eqn}}
{{eqn | l = \frac {y_1} {y_2}
      | r = \frac {e^{m_1 x} } {e^{m_2 x} }
}}
{{eqn | r = e^{\paren {m_1 - m_2} x}
}}
{{eqn | o = \ne
      | r = 0
      | c = as $m_1 \ne m_2$
}}
{{end-eqn}}
Thus $y_1$ and $y_2$ are linearly independent.
It follows from Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution that:
:$y = C_1 e^{m_1 x} + C_2 e^{m_2 x}$
is the general solution to $(1)$.
Theorem: Solution of Constant Coefficient Homogeneous LSOODE/Equal Real Roots of Auxiliary Equation

{{:Solution of Constant Coefficient Homogeneous LSOODE}}
Let $p^2 = 4 q$.
Then $(1)$ has the general solution:
:$y = C_1 e^{m_1 x} + C_2 x e^{m_1 x}$

Proof:
Consider the auxiliary equation of $(1)$:
:$(2): \quad m^2 + p m + q$
Let $p^2 = 4 q$.
From Solution to Quadratic Equation with Real Coefficients, $(2)$ has one (repeated) root, that is:
:$m_1 = m_2 = -\dfrac p 2$
From Exponential Function is Solution of Constant Coefficient Homogeneous LSOODE iff Index is Root of Auxiliary Equation:
:$y_1 = e^{m_1 x}$
is a particular solution to $(1)$.
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int p \rd x
      | c = 
}}
{{eqn | r = p x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-p x}
      | c = 
}}
{{eqn | r = e^{2 m_1 x}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {e^{2 m_1 x} } e^{2 m_1 x} \rd x
      | c = as $y_1 = e^{m_1 x}$
}}
{{eqn | r = \int \rd x
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = x e^{m_1 x}
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 e^{m_1 x} + C_2 x e^{m_1 x}$
Theorem: Linear Second Order ODE/y'' + y' - 6 y = 0

The second order ODE:
:$(1): \quad y' ' + y' - 6 y = 0$
has the general solution:
:$y = C_1 e^{2 x} + C_2 e^{-3 x}$

Proof:
It can be seen that $(1)$ is a constant coefficient homogeneous linear second order ODE.
Its auxiliary equation is:
:$(2): \quad: m^2 + m - 6 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = -3$
:$m_2 = 2$
These are real and unequal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 e^{2 x} + C_2 e^{-3 x}$
{{qed}}
Theorem: Linear Second Order ODE/y'' + 2 y' + y = 0

The second order ODE:
:$(1): \quad y' ' + 2 y' + y = 0$
has the general solution:
:$y = C_1 e^{-x} + C_2 x e^{-x}$

Proof:
It can be seen that $(1)$ is a constant coefficient homogeneous linear second order ODE.
Its auxiliary equation is:
:$(2): \quad m^2 + 2 m + 1 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = m_2 = -1$
These are real and equal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 e^{-x} + C_2 x e^{-x}$
{{qed}}