avewright/proofwiki-math huggingface dataset:
Theorem: Existence and Uniqueness of Solution for Linear Second Order ODE with two Initial Conditions

Let $\map P x$, $\map Q x$ and $\map R x$ be continuous real functions on a closed real interval $\closedint a b$.
Let $x_0$ be any point in $\closedint a b$.
Let $y_0$ and ${y_0}'$ be real numbers.
Then the linear second order ordinary differential equation:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = \map R x$
has a unique particular solution $\map y x$ on $\closedint a b$ such that:
:$\map y {x_0} = y_0$
and:
:$\map {y'} {x_0} = {y_0}'$

Proof:
Let $z = \dfrac {\d y} {\d x}$.
Then a solution to $(1)$ will yield a particular solution to:
:$(2): \quad \begin{cases}
\dfrac {\d y} {\d x} = z & , \map y {x_0} = y_0 \\
& \\
\dfrac {\d z} {\d x} = -\map P x \dfrac {\d y} {\d x} - \map Q x y + \map R x & , \map z {x_0} = {y_0}'
\end{cases}$
From Lipschitz Condition on Linear ODE of Continuous Functions, $(2)$ satisfies the Lipschitz condition.
Hence Picard's Existence Theorem applies.
Hence the result.
{{qed}}
Theorem: General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution

Consider the nonhomogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = \map R x$
Let $\map {y_g} x$ be the general solution of the homogeneous linear second order ODE:
:$(2): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
Let $\map {y_p} x$ be a particular solution of $(1)$.
Then $\map {y_g} x + \map {y_p} x$ is the general solution of $(1)$.

Proof:
Let $\map {y_g} {x, C_1, C_2}$ be a general solution of $(2)$.
Note that $C_1$ and $C_2$ are the two arbitrary constants that are to be expected of a second order ODE.
Let $\map {y_p} x$ be a certain fixed particular solution of $(1)$.
Let $\map y x$ be an arbitrary particular solution of $(1)$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {y - y_p}' ' + \map P x \paren {y - y_p}' + \map Q x \paren {y - y_p}
      | c = 
}}
{{eqn | r = \paren {y' ' + \map P x y' + \map Q x y} - \paren {y_p' ' + \map P x y_p' + \map Q x y_p}
      | c = 
}}
{{eqn | r = \map R x - \map R x
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
We have that $\map {y_g} {x, C_1, C_2}$ is a general solution of $(2)$.
Thus:
:$\map y x - \map {y_p} x = \map {y_g} {x, C_1, C_2}$
or:
:$\map y x = \map {y_g} {x, C_1, C_2} + \map {y_p} x$
{{qed}}
Theorem: Trivial Solution of Homogeneous Linear 2nd Order ODE

The homogeneous linear second order ODE:
:$\dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
has the particular solution:
:$\map y x = 0$
that is, the zero constant function.
This particular solution is referred to as the '''trivial solution'''.

Proof:
We have:
:$\map {\dfrac {\d} {\d x} } 0 = 0$
and so:
:$\map {\dfrac {\d^2} {\d x^2} } 0 = 0$
from which:
:$\dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
Hence the result.
{{Qed}}
Theorem: Linear Combination of Solutions to Homogeneous Linear 2nd Order ODE

Let $c_1$ and $c_2$ be real numbers.
Let $\map {y_1} x$ and $\map {y_2} x$ be particular solutions to the homogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
Then:
:$c_1 \, \map {y_1} x + c_2 \, \map {y_2} x$
is also a particular solution to $(1)$.
That is, a linear combination of particular solutions to a homogeneous linear second order ODE is also a particular solution to that ODE.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {c_1 \, \map {y_1} x + c_2 \, \map {y_2} x}' ' + \map P x \paren {c_1 \, \map {y_1} x + c_2 \, \map {y_2} x}' + \map Q x \paren {c_1 \, \map {y_1} x + c_2 \, \map {y_2} x}
      | c = 
}}
{{eqn | r = \paren {c_1 \, \map {y_1' '} x + c_2 \, \map {y_2' '} x} + \map P x \paren {c_1 \, \map {y_1'} x + c_2 \, \map {y_2'} x} + \map Q x \paren {c_1 \, \map {y_1} x + c_2 \, \map {y_2} x}
      | c = Linear Combination of Derivatives
}}
{{eqn | r = c_1 \paren {\map {y_1' '} x + \map P x \, \map {y_1'} x + \map Q x \, \map {y_1} x} + c_2 \paren {\map {y_2' '} x + \map P x \, \map {y_2'} x + \map Q x \, \map {y_2} x}
      | c = 
}}
{{eqn | r = c_1 \cdot 0 + c_2 \cdot 0
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Solution of Linear 2nd Order ODE Tangent to X-Axis

Let $\map {y_p} x$ be a particular solution to the homogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
on a closed interval $\closedint a b$.
Let there exist $\xi \in \closedint a b$ such that the curve in the cartesian plane described by $y = \map {y_p} x$ is tangent to the $x$-axis at $\xi$.
Then $\map {y_p} x$ is the zero constant function:
:$\forall x \in \closedint a b: \map {y_p} x = 0$

Proof:
{{AimForCont}} $y_p$ is not the zero constant function.
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another, there exists another particular solution to $(1)$ such that $y_1$ and $y_2$ are linearly independent.
At the point $\xi$:
:$\map {y_p} \xi = 0$
:$\map { {y_p}'} \xi = 0$
Taking the Wronskian of $y_p$ and $y_2$:
:$\map W {y_p, y_2} = y_p {y_2}' - {y_p}' y_2$
But at $\xi$ this works out as zero.
It follows from Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE iff Linearly Dependent that $y_p$ and $y_2$ cannot be linearly independent after all.
From this contradiction, $y_p$ must the zero constant function.
{{qed}}
Theorem: Solutions of Linear 2nd Order ODE have Common Zero iff Linearly Dependent

Let $\map {y_1} x$ and $\map {y_2} x$ be particular solutions to the homogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
on a closed interval $\closedint a b$.
Let $y_1$ and $y_2$ both have a zero for the same value of $x$ in $\closedint a b$.
Then $y_1$ and $y_2$ are constant multiples of each other.
That is, $y_1$ and $y_2$ are linearly dependent.

Proof:
Let $\xi \in \closedint a b$ be such that $\map {y_1} \xi = \map {y_2} \xi = 0$.
Consider the Wronskian $\map W {y_1, y_2}$ at $\xi$:
{{begin-eqn}}
{{eqn | l = \map W {\map {y_1} \xi, \map {y_2} \xi}
      | r = \map {y_1} \xi \map { {y_2}'} \xi - \map {y_2} \xi \map { {y_1}'} \xi
      | c = 
}}
{{eqn | r = 0 \cdot \map { {y_2}'} \xi - 0 \cdot \map { {y_1}'} \xi
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
From Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE:
:$\forall x \in \closedint a b: \map W {\map {y_1} \xi, \map {y_2} \xi} = 0$
and so from Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE iff Linearly Dependent:
:$y_1$ and $y_2$ are linearly dependent.
{{qed}}
Theorem: Real Function is Linearly Dependent with Zero Function

Let $\map f x$ be a real function defined on a closed interval $\closedint a b$.
Let $\map g x$ be the constant zero function on $\closedint a b$:
:$\forall x \in \closedint a b: \map g x = 0$
Then $f$ and $g$ are linearly dependent on $\closedint a b$.

Proof:
We have that:
:$\forall x \in \closedint a b: \map g x = 0 = 0 \times \map f x$
and $0 \in \R$.
Hence the result by definition of linearly dependent real functions.
Theorem: Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution

Let $\map {y_1} x$ and $\map {y_2} x$ be particular solutions to the homogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
on a closed interval $\closedint a b$.
Let $y_1$ and $y_2$ be linearly independent.
Then the general solution to $(1)$ is:
:$y = C_1 \map {y_1} x + C_2 \map {y_2} x$
where $C_1 \in \R$ and $C_2 \in \R$ are arbitrary constants.

Proof:
Let $\map y x$ be any particular solution to $(1)$ on $\closedint a b$.
It is to be shown that constants $C_1$ and $C_2$ can be found such that:
:$\map y x = C_1 \map {y_1} x + C_2 \map {y_2} x$
for all $x \in \closedint a b$.
By Existence and Uniqueness of Solution for Linear Second Order ODE with two Initial Conditions:
:a particular solution to $(1)$ over $\closedint a b$ is completely determined by:
::its value
:and:
::the value of its derivative
at a single point.
From Linear Combination of Solutions to Homogeneous Linear 2nd Order ODE:
:$C_1 \map {y_1} x + C_2 \map {y_2} x$
is a particular solution to $(1)$ over $\closedint a b$
We also have:
:$\map y x$
is a particular solution to $(1)$ over $\closedint a b$
Thus it is sufficient to prove that:
:$\exists x_0 \in \closedint a b: \exists C_1, C_2 \in \R$ such that:
::$ C_1 \map {y_1} {x_0} + C_2 \map {y_2} {x_0} = \map y {x_0}$
:and:
::$ C_1 \map { {y_1}'} {x_0} + C_2 \map { {y_2}'} {x_0} = \map y {x_0}$
For this system to be solvable for $C_1$ and $C_2$ it is necessary that:
:$\begin{vmatrix}
\map {y_1} x & \map {y_2} x \\
\map { {y_1}'} x & \map { {y_2}'} x \\
\end{vmatrix} = \map {y_1} x \map { {y_2}'} x - \map {y_2} x \map { {y_1}'} x \ne 0$
That is, that the Wronskian $\map W {y_1, y_2} \ne 0$ at $x_0$.
From Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE:
:if $\map W {y_1, y_2} \ne 0$ at $x_0$, then $\map W {y_1, y_2} \ne 0$ for all $x \in \closedint a b$.
Hence it does not matter what point is taken for $x_0$; if the Wronskian is non-zero at one such point, it will be non-zero for all such points.
From Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE iff Linearly Dependent:
:$W \left({y_1, y_2}\right) = 0$ for all $x \in \closedint a b$ {{iff}} $y_1$ and $y_2$ are linearly dependent.
But we have that $y_1$ and $y_2$ are linearly independent.
Hence:
:$\forall x \in \closedint a b: \map W {y_1, y_2} \ne 0$
and so:
:$\exists x_0 \in \closedint a b: \exists C_1, C_2 \in \R$ such that:
::$ C_1 \map {y_1} {x_0} + C_2 \map {y_2} {x_0} = \map y {x_0}$
:and:
::$ C_1 \map { {y_1}'} {x_0} + C_2 \map { {y_2}'} {x_0} = \map y {x_0}$
The result follows.
{{qed}}
Theorem: Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE

Let $\map {y_1} x$ and $\map {y_2} x$ be particular solutions to the homogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
on a closed interval $\closedint a b$.
Let $y_1$ and $y_2$ be linearly independent.
Then their Wronskian is either never zero, or zero everywhere on $\closedint a b$.

Proof:
{{begin-eqn}}
{{eqn | l = \map W {y_1, y_2}
      | r = y_1 {y_2}' - y_2 {y_1}'
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {W'} {y_1, y_2}
      | r = \paren {y_1 {y_2}' ' + {y_1}' {y_2}'} - \paren {y_2 {y_1}' ' + {y_2}' {y_1}'}
      | c = Product Rule for Derivatives
}}
{{eqn | r = y_1 {y_2}' ' - y_2 {y_1}' '
      | c = 
}}
{{end-eqn}}
Because $y_1$ and $y_2$ are both particular solutions of $(1)$:
{{begin-eqn}}
{{eqn | n = 2
      | l = {y_1}' ' + \map P x {y_1}' + \map Q x y_1
      | r = 0
      | c = 
}}
{{eqn | n = 3
      | l = {y_2}' ' + \map P x {y_2}' + \map Q x y_2
      | r = 0
      | c = 
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = y_2 {y_1}' ' + \map P x y_2 {y_1}' + \map Q x y_2 y_1
      | r = 0
      | c = $(2)$ multiplied by $y_2$
}}
{{eqn | n = 5
      | l = y_1 {y_2}' ' + \map P x y_1 {y_2}' + \map Q x y_1 y_2
      | r = 0
      | c = $(3)$ multiplied by $y_1$
}}
{{eqn | n = 6
      | ll= \leadsto
      | l = \paren {y_1 {y_2}' ' - y_2 {y_1}' '} + \map P x \paren {y_1 {y_2}' - y_2 {y_1}'}
      | r = 0
      | c = $(5)$ subtracted from $(6)$
}}
{{end-eqn}}
That is:
:$\dfrac {\d P} {\d W} + P W = 0$
This is a linear first order ODE.
From Solution to Linear First Order Ordinary Differential Equation:
:$W = C e^{-\int P \rd x}$
The exponential function is never zero:
Therefore:
:$W = 0 \iff C = 0$
and the result follows.
{{qed}}
Theorem: Real Number Line is Lindelöf

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a Lindelöf Space.

Proof:
From Real Number Line is Second-Countable we have that $\struct {\R, \tau_d}$ is a second-countable space.
The result follows from Second-Countable Space is Lindelöf.
{{qed}}
Theorem: Real Number Line is Lindelöf

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a Lindelöf Space.

Proof:
From Real Number Line is $\sigma$-Compact we have that $\struct {\R, \tau_d}$ is a $\sigma$-compact space.
The result follows from $\sigma$-Compact Space is Lindelöf.
{{qed}}
Theorem: Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE iff Linearly Dependent

Let $\map {y_1} x$ and $\map {y_2} x$ be particular solutions to the homogeneous linear second order ODE:
:$(1): \quad \dfrac {\d^2 y} {\d x^2} + \map P x \dfrac {\d y} {\d x} + \map Q x y = 0$
on a closed interval $\closedint a b$.
Then:
:$y_1$ and $y_2$ are linearly dependent
{{iff}}:
:the Wronskian $\map W {y_1, y_2}$ of $y_1$ and $y_2$ is zero everywhere on $\closedint a b$.

Proof:
=== Sufficient Condition ===
Let $y_1$ and $y_2$ are linearly dependent.
Suppose either $y_1$ or $y_2$ is zero everywhere on $\closedint a b$.
Then either ${y_1}'$ or ${y_2}'$ is also zero everywhere on $\closedint a b$.
Thus:
:$y_1 {y_2}' - y_2 {y_1}' = 0$
and so by definition $\map W {y_1, y_2} = 0$ everywhere on $\closedint a b$.
Suppose that neither $y_1$ nor $y_2$ is zero everywhere on $\closedint a b$.
{{WLOG}}, it follows by definition of linearly dependent that:
:$y_2 = C y_1$
for some $C \in \R$.
Thus by Derivative of Constant Multiple:
:${y_2}' = C {y_1}'$
Hence:
{{begin-eqn}}
{{eqn | l = C
      | r = \frac {y_2} {y_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_2}'
      | r = \frac {y_2} {y_1} {y_1}'
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_1 {y_2}'
      | r = y_2 {y_1}'
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_1 {y_2}' - y_2 {y_1}'
      | r = 0
      | c = 
}}
{{end-eqn}}
Hence by definition $\map W {y_1, y_2} = 0$ everywhere on $\closedint a b$.
{{qed|lemma}}
Theorem: Linear Second Order ODE/y'' + y = 0

The second order ODE:
:$(1): \quad y' ' + y = 0$
has the general solution:
:$y = C_1 \sin x + C_2 \cos x$

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
:$p \dfrac {\d p} {\d y} = -y$
where $p = \dfrac {\d y} {\d x}$.
From:
:First Order ODE: $y \rd y = k x \rd x$
with $k = 1$, this has the solution:
:$p^2 = -y^2 + C$
or: 
:$p^2 + y^2 = C$
As the {{LHS}} is the sum of squares, $C$ has to be positive for this to have any solutions.
Thus, let $C = \alpha^2$.
Then:
{{begin-eqn}}
{{eqn | l = p^2 + y^2
      | r = \alpha^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p = \dfrac {\d y} {\d x}
      | r = \pm \sqrt {\alpha^2 - y^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} {\sqrt {\alpha^2 - y^2} }
      | r = \int \pm 1 \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \arcsin \dfrac y \alpha
      | r = \pm x + \beta
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \alpha \map \sin {\pm x + \beta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = A \map \sin {x + B}
      | c = 
}}
{{end-eqn}}
From Multiple of Sine plus Multiple of Cosine: Sine Form, this can be expressed as:
:$y = C_1 \sin x + C_2 \cos x$
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = 0

The second order ODE:
:$(1): \quad y' ' + y = 0$
has the general solution:
:$y = C_1 \sin x + C_2 \cos x$

Proof:
$(1)$ can be seen to be a special case of:
:$(2): \quad$ Linear Second Order ODE: $y' ' + k^2 y = 0$
with $k = 1$.
$(2)$ has the solution:
:$y = C_1 \sin k x + C_2 \cos k x$
Hence setting $k = 1$:
:$y = C_1 \sin x + C_2 \cos x$
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = 0

The second order ODE:
:$(1): \quad y' ' + y = 0$
has the general solution:
:$y = C_1 \sin x + C_2 \cos x$

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \, \sin x
      | r = \cos x
      | c = Derivative of Sine Function
}}
{{eqn | l = \frac \d {\d x} \, \cos x
      | r = -\sin x
      | c = Derivative of Cosine Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d^2} {\d x^2} \, \cos x
      | r = -\cos x
      | c = 
}}
{{eqn | l = \frac {\d^2} {\d x^2} \, \sin x
      | r = -\sin x
      | c =  
}}
{{end-eqn}}
Hence it can be seen by inspection that:
{{begin-eqn}}
{{eqn | l = \map {y_1} x
      | r = \sin x
}}
{{eqn | l = \map {y_2} x
      | r = \cos x
}}
{{end-eqn}}
are particular solutions to $(1)$.
It is noted that:
:$\dfrac {y_1} {y_2} = \tan x$
which is not a constant function on any closed interval $\closedint a b$.
Calculating the Wronskian of $y_1$ and $y_2$:
{{begin-eqn}}
{{eqn | l = \map W {y_1, y_2}
      | r = \begin{vmatrix} \sin x & \cos x \\ \cos x & -\sin x \end{vmatrix}
      | c = 
}}
{{eqn | r = -\sin^2 x - \cos^2 x
      | c = 
}}
{{eqn | r = -1
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
So the Wronskian of $y_1$ and $y_2$ is never zero.
We have that $(1)$ is a homogeneous linear second order ODE in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where $\map P x = 0$ and $\map Q x$ are constant functions.
So by Constant Real Function is Continuous: $P$ and $Q$ are continuous on $\closedint a b$
Thus from Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$(1)$ has the general solution:
::$y = C_1 \sin x + C_2 \cos x$
:on $\closedint a b$.
Since $\closedint a b$ can be extended indefinitely without introducing points where $P$ or $Q$ are discontinuous, the general solution is valid for all $x$.
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = 0

The second order ODE:
:$(1): \quad y' ' + y = 0$
has the general solution:
:$y = C_1 \sin x + C_2 \cos x$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y'
      | r = \cos x
      | c = Derivative of Sine Function
}}
{{eqn | ll= \leadsto
      | l = y' '
      | r = -\sin x
      | c = Derivative of Cosine Function
}}
{{end-eqn}}
and so:
:$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 = 0$
:$\map Q 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 0 \rd x
      | c = 
}}
{{eqn | r = k
      | c = where $k$ is arbitrary
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{-k}
      | c = 
}}
{{eqn | r = C
      | c =  where $C$ is also arbitrary
}}
{{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 {\sin^2 x} C \rd x
      | c = 
}}
{{eqn | r = \int C \csc^2 x \rd x
      | c = {{Defof|Cosecant}}
}}
{{eqn | r = -C \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 = \sin x \paren {-C \cot x}
      | c = 
}}
{{eqn | r = -C \cos x
      | c = {{Defof|Cotangent}}, and simplifying
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 \sin x + k \paren {-C \cos x}$
where $k$ is arbitrary.
Setting $C_2 = - k C$ yields the result:
:$y = C_1 \sin x + C_2 \cos x$
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = 0

The second order ODE:
:$(1): \quad y' ' + y = 0$
has the general solution:
:$y = C_1 \sin x + C_2 \cos x$

Proof:
Taking Laplace transforms, we have: 
:$\laptrans {y' ' + y} = \laptrans 0$
From Laplace Transform of Constant Mapping, we have: 
:$\laptrans 0 = 0$
We also have: 
{{begin-eqn}}
{{eqn | l = \laptrans {y' ' + y}
      | r = \laptrans {y' '} + \laptrans y
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = s^2 \laptrans y - s \map y 0 - \map {y'} 0 + \laptrans y
      | c = Laplace Transform of Second Derivative
}}
{{end-eqn}}
So: 
:$\paren {s^2 + 1} \laptrans y = s \map y 0 + \map {y'} 0$
Giving: 
:$\laptrans y = \map y 0 \dfrac s {s^2 + 1} + \map {y'} 0 \dfrac 1 {s^2 + 1}$
So: 
{{begin-eqn}}
{{eqn | l = y
      | r = \invlaptrans {\map y 0 \frac s {s^2 + 1} + \map {y'} 0 \frac 1 {s^2 + 1} }
      | c = {{Defof|Inverse Laplace Transform}}
}}
{{eqn | r = \map y 0 \invlaptrans {\frac s {s^2 + 1} } + \map {y'} 0 \invlaptrans {\frac 1 {s^2 + 1} }
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \map y 0 \invlaptrans {\laptrans {\cos x} } + \map {y'} 0 \invlaptrans {\laptrans {\sin x} }
      | c = Laplace Transform of Cosine, Laplace Transform of Sine
}}
{{eqn | r = \map y 0 \cos x + \map {y'} 0 \sin x
      | c = {{Defof|Inverse Laplace Transform}}
}}
{{end-eqn}}
Setting $C_1 = \map {y'} 0$ and $C_2 = \map y 0$ gives the result.
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = 0/y(0) = 2, y'(0) = 3

The second order ODE:
:$(1): \quad y' ' + y = 0$
with initial conditions:
:$\map y 0 = 2$
:$\map {y'} 0 = 3$
has the particular solution:
:$y = 3 \sin x + 2 \cos x$

Proof:
From Linear Second Order ODE: $y' ' + y = 0$, the general solution of $(1)$ is:
:$y = C_1 \sin x + C_2 \cos x$
Differentiating {{WRT|Differentiation}} $x$:
:$y' = C_1 \cos x - C_2 \sin x$
Thus for the initial conditions:
{{begin-eqn}}
{{eqn | l = \map y 0
      | r = C_1 \sin 0 + C_2 \cos 0
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C_1 \times 0 + C_2 \times 1
      | r = 2
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{eqn | ll= \leadsto
      | l = C_2
      | r = 2
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {y'} 0
      | r = C_1 \cos 0 - C_2 \sin 0
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C_1 \times 1 - C_2 \times 0
      | r = 3
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{eqn | ll= \leadsto
      | l = C_1
      | r = 3
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Linearly Independent Solutions of y'' - y = 0

The second order ODE:
:$(1): \quad y' ' - y = 0$
has solutions:
:$y_1 = e^x$
:$y_2 = e^{-x}$
which are linearly independent.

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \, e^x
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{eqn | l = \frac \d {\d x} \, e^{-x}
      | r = -e^{-x}
      | c = Derivative of Exponential Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d^2} {\d x^2} \, e^x
      | r = e^x
      | c = 
}}
{{eqn | l = \frac {\d^2} {\d x^2} \, e^{-x}
      | r = e^{-x}
      | c =  
}}
{{end-eqn}}
Hence it can be seen by inspection that:
{{begin-eqn}}
{{eqn | l = \map {y_1} x
      | r = e^x
}}
{{eqn | l = \map {y_2} x
      | r = e^{-x}
}}
{{end-eqn}}
are solutions to $(1)$.
Calculating the Wronskian of $y_1$ and $y_2$:
{{begin-eqn}}
{{eqn | l = \map W {y_1, y_2}
      | r = \begin{vmatrix} e^x & e^{-x} \\ e^x & -e^{-x} \end{vmatrix}
      | c = 
}}
{{eqn | r = -e^x e^{-x} - e^x e^{-x}
      | c = 
}}
{{eqn | r = -2
      | c = 
}}
{{end-eqn}}
So the Wronskian of $y_1$ and $y_2$ is never zero.
Thus from Zero Wronskian of Solutions of Homogeneous Linear Second Order ODE iff Linearly Dependent:
:$y_1$ and $y_2$ are linearly independent.
{{qed}}