avewright/proofwiki-math huggingface dataset:
Theorem: Differential Equation defining Confocal Conics

Consider the equation:
:$(1): \quad \dfrac {x^2} {a^2 + \lambda} + \dfrac {y^2} {b^2 + \lambda} = 1$
where $a^2 > b^2$ and $-\lambda < a^2$.
defining the set of confocal conics whose foci are at $\tuple {\pm \sqrt {a^2 - b^2}, 0}$.
The differential equation defining these confocal conics is:
:$x y \paren {\paren {y'}^2 - 1} + \paren {x^2 - y^2 - a^2 + b^2} y' = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {x^2} {a^2 + \lambda}
      | r = 1 - \dfrac {y^2} {b^2 + \lambda}
      | c = from $(1)$
}}
{{eqn | r = \dfrac {b^2 + \lambda - y^2} {b^2 + \lambda}
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = a^2 + \lambda
      | r = \dfrac {x^2 \paren {b^2 + \lambda} } {b^2 + \lambda - y^2}
      | c = 
}}
{{eqn | l = \dfrac {y^2} {b^2 + \lambda}
      | r = 1 - \dfrac {x^2} {a^2 + \lambda}
      | c = from $(1)$
}}
{{eqn | r = \dfrac {a^2 + \lambda - x^2} {a^2 + \lambda}
      | c = 
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = b^2 + \lambda
      | r = \dfrac {y^2 \paren {a^2 + \lambda} } {a^2 + \lambda - x^2}
      | c = 
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\dfrac {x^2} {a^2 + \lambda} + \dfrac {y^2} {b^2 + \lambda} }
      | r = \map {\dfrac \d {\d x} } 1
      | c = Differentiating $(1)$ {{WRT|Differentiation}} $x$
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = \dfrac {2 x} {a^2 + \lambda} + \dfrac {2 y} {b^2 + \lambda} \dfrac {\d y} {\d x}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {a^2 + \lambda} y'
      | r = -\dfrac {2 x} {2 y} \paren {b^2 + \lambda}
      | c = putting $y' = \dfrac {\d y} {\d x}$
}}
{{eqn | r = -\dfrac x y \dfrac {y^2 \paren {a^2 + \lambda} } {a^2 + \lambda - x^2}
      | c = from $(3)$
}}
{{eqn | ll= \leadsto
      | l = y'
      | r = -\dfrac {x y} {a^2 + \lambda - x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y' \paren {a^2 + \lambda}
      | r = x^2 y' - x y
      | c = 
}}
{{eqn | n = 5
      | ll= \leadsto
      | l = a^2 + \lambda
      | r = \dfrac {x^2 y' - x y} {y'}
      | c = 
}}
{{end-eqn}}
and similarly:
{{begin-eqn}}
{{eqn | l = \paren {b^2 + \lambda}
      | r = -\dfrac {2 y} {2 x} \paren {a^2 + \lambda} y'
      | c = from $(4)$, putting $y' = \dfrac {\d y} {\d x}$
}}
{{eqn | r = -\dfrac {y y'} x \dfrac {x^2 \paren {b^2 + \lambda} } {b^2 + \lambda - y^2}
      | c = from $(2)$
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = -\dfrac {x y y'} {b^2 + \lambda - y^2}
      | c = 
}}
{{eqn | n = 6
      | ll= \leadsto
      | l = b^2 + \lambda
      | r = y^2 - x y y'
      | c = 
}}
{{end-eqn}}
Eliminating $\lambda$:
{{begin-eqn}}
{{eqn | l = b^2 + \paren {\dfrac {x^2 y' - x y} {y'} - a^2}
      | r = y^2 - x y y'
      | c = from $(5)$ and $(6)$
}}
{{eqn | ll= \leadsto
      | l = y' \paren {b^2 - a^2} + x^2 y' - x y - y^2 y + x y \paren {y'}^2
      | r = 0
      | c = multiplying through by $y'$ and rearranging
}}
{{eqn | ll= \leadsto
      | l = x y \paren {\paren {y'}^2 - 1} + \paren {x^2 - y^2 - a^2 + b^2} y'
      | r = 0
      | c = multiplying through by $y'$ and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: P-adic Integer has Unique Coherent Sequence Representative/Lemma 3

:$\sequence {\alpha_n}$ and $\sequence {\beta_n}$ are representatives of the same $p$-adic number in $\Q_p$.

Proof:
From Representatives of same P-adic Number iff Difference is Null Sequence, it needs only to be shown that $\sequence {\alpha_j - \beta_j}$ is a null sequence.
Let $\epsilon \in \R_{> 0}$.
From Sequence of Powers of Number less than One, the sequence $\sequence {p^n}$ is a null sequence.
Then there exists $j \in \N$ such that $p^{-j} < \epsilon$.
Then for all $i \ge \map N j$:
{{begin-eqn}}
{{eqn | l = \norm {\alpha_i - \beta_i}_p 
      | r = \norm {\alpha_i - \beta_{\map N i} + \beta_{\map N i} - \beta_i}_p
}}
{{eqn | o = \le 
      | r = \max \set {\norm {\alpha_i - \beta_{\map N i} }_p, \norm {\beta_{\map N i} - \beta_i}_p}
}}
{{eqn | o = \le 
      | r = \max \set {\norm {p^{-\paren{i + 1} } }_p, \norm {\beta_{\map N i} - \beta_i}_p}
      | c =
}}
{{eqn | o = \le 
      | r = \max \set {\norm {p^{-\paren{i + 1} } }_p, \norm {p^{-\paren {i + 1} } }_p}
      | c =
}}
{{eqn | r = \norm {p^{-\paren {i + 1} } }_p
      | c =
}}
{{eqn | o = \le 
      | r = \norm {p^{-j } }_p
      | c =
}}
{{eqn | o = < 
      | r = \epsilon
      | c =
}}
{{end-eqn}}
It follows that $\sequence {\alpha_n - \beta_n}$ is a null sequence by definition.
{{qed}}
Category:P-adic Integer has Unique Coherent Sequence Representative
ogpt6tsx87z0sudzm6yl4n9tlgz9bml
Theorem: P-adic Integer has Unique Coherent Sequence Representative/Lemma 4

:$\sequence {\alpha_j}$ is the only coherent sequence that represents $a$.

Proof:
Let $\sequence {\alpha'_j}$ be a coherent sequence not equal to $\sequence {\alpha_j}$.
From Representatives of same P-adic Number iff Difference is Null Sequence, it needs only to be shown that $\sequence {\alpha_j - \alpha'_j}$ is not a null sequence.
Since $\sequence {\alpha'_j} \ne \sequence{\alpha_j}$ then:
:$\exists i_0 \in \N : \alpha'_{i_0} \ne \alpha_{i_0}$
By definition of coherent sequences:
:$0 \le \alpha_{i_0}, \alpha'_{i_0} < p^{i_0 + 1}$
From Reduced Residue System Modulo Prime:
:$\alpha_{i_0} \not \equiv \alpha'_{i_0} \pmod {p^{i_0 + 1} }$
By definition of a coherent sequence, for all $i > i_0$:
:$\alpha_i \equiv \alpha_{i_0} \pmod {p^{i_0 + 1} }$
:$\alpha'_i \equiv \alpha'_{i_0} \pmod {p^{i_0 + 1} }$
Then:
:$\forall i > i_0: \alpha_i \equiv \alpha_{i_0} \not \equiv \alpha'_{i_0}  \equiv \alpha'_i \pmod {p^{i_0 + 1} }$
That is:
:$\forall i > i_0: p^{i_0 + 1} \nmid \alpha_i - \alpha'_i$
By definition of the $p$-adic norm on integers:
:$\forall i > i_0: \norm {\alpha_i - \alpha'_i} > \dfrac 1 {p^{i_0 + 1} }$
By definition of convergence, $\sequence {\alpha_j - \alpha'_j}$ is not a null sequence.
The result follows.
{{qed}}
Category:P-adic Integer has Unique Coherent Sequence Representative
kcyqcjy5cxrpge477ylblljohdfgahg
Theorem: Elimination of Constants by Partial Differentiation

Let $x_1, x_2, \dotsc, x_m$ be independent variables.
Let $c_1, c_2, \dotsc, c_n$ be arbitrary constants.
Let this equation:
:$(1): \quad \map f {x_1, x_2, \dotsc, x_m, z, c_1, c_2, \dotsc, c_n} = 0$
define a dependent variable $z$ via the implicit function $f$.
Then it may be possible to eliminate the constants by successive partial differentiation of $(1)$.

Proof:
We differentiate $(1)$ partially {{WRT|Differentiation}} each of $x_j$ for $1 \le j \le m$:
:$(2): \quad \dfrac {\partial f} {\partial x_j} + \dfrac {\partial f} {\partial z} \cdot \dfrac {\partial z} {\partial x_j} = 0$
Suppose $m \ge n$.
Then there exist sufficient equations of the form of $2$ for the constants $c_1, c_2, \dotsc, c_n$ to be eliminated.
Otherwise suppose $m > n$.
Then we differentiate $(2)$ partially for each $j$ {{WRT|Differentiation}} each of $x_j$ for $1 \le j \le m$, to obtain:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial^2 f} {\partial {x_j}^2} + 2 \dfrac {\partial^2 f} {\partial x_j \partial z} + \dfrac {\partial^2 f} {\partial z^2} \cdot \paren {\dfrac {\partial z} {\partial x_j} }^2 + \dfrac {\partial f} {\partial z} \cdot \dfrac {\partial^2 z} {\partial {x_j}^2}
      | r = 0
      | c = for $1 \le j \le m$
}}
{{eqn | l = \dfrac {\partial^2 f} {\partial x_j \partial x_k} + \dfrac {\partial^2 f} {\partial x_j \partial z} \cdot \dfrac {\partial z} {\partial x_k} + \dfrac {\partial^2 f} {\partial x_k \partial z} \cdot \dfrac {\partial z} {\partial x_j} + \dfrac {\partial^2 f} {\partial z^2} \cdot \dfrac {\partial z} {\partial x_j} \cdot \dfrac {\partial z} {\partial x_k} + \dfrac {\partial f} {\partial z} \cdot \dfrac {\partial^2 f} {\partial x_j \partial x_k}
      | r = 0
      | c = for $1 \le j \le m$, $1 \le k \le m$, $j \ne k$
}}
{{end-eqn}}
and continue the operation until enough equations have been obtained so that the remaining constants can be eliminated.
{{qed}}
Theorem: Representatives of same P-adic Number iff Difference is Null Sequence

Let $p$ be a prime number.
Let $\norm {\,\cdot\,}_p$ be the $p$-adic norm on the rational numbers $\Q$.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\sequence{\alpha_n}$ and $\sequence{\beta_n}$ be Cauchy sequences in $\struct {Q, \norm {\,\cdot\,}_p}$.
Then: 
:$\sequence {\alpha_n}$ and $\sequence {\beta_n}$ are representatives of the same $p$-adic number in $\Q_p$
{{iff}}:
:the sequence $\sequence {\alpha_n - \beta_n}$ is a null sequence.

Proof:
Let $\CC$ be the commutative ring of Cauchy sequences over $\struct {\Q, \norm {\,\cdot\,}_p}$.
Let $\NN$ be the set of null sequences in $\struct {\Q, \norm {\,\cdot\,}_p}$.
Then $\Q_p$ is the quotient ring $\CC \, \big / \NN$ by definition of the $p$-adic numbers.
Hence:
:$\sequence {\alpha_n}$ and $\sequence {\beta_n}$ are representatives of the same $p$-adic number in $\Q_p$ 
{{iff}}:
:$\sequence {\alpha_n}$ and $\sequence {\beta_n}$ are elements of the same left coset of $\NN$ in $\CC$.
From Element in Left Coset iff Product with Inverse in Subgroup:
:$\sequence {\alpha_n}$ and $\sequence {\beta_n}$ are elements of the same left coset of $\NN$ in $\CC$ 
{{iff}}: 
:$\sequence {\alpha_n} - \sequence {\beta_n} = \sequence {\alpha_n - \beta_n} \in \NN$.
The result follows.
{{qed}}
Category:P-adic Number Theory
8nos1wnnj5qdh6sye3vse0zl77hshxa
Theorem: Partial Differential Equation of Planes in 3-Space

The set of planes in real Cartesian $3$-dimensional space can be described by the system of partial differential equations:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial^2 z} {\partial x^2}
      | r = 0
}}
{{eqn | l = \dfrac {\partial^2 z} {\partial x \partial y}
      | r = 0
}}
{{eqn | l = \dfrac {\partial^2 z} {\partial y^2}
      | r = 0
}}
{{end-eqn}}

Proof:
From Equation of Plane, we have that the equation defining a general plane $P$ is:
:$\alpha_1 x + \alpha_2 y + \alpha_3 z = \gamma$
which can be written as:
:$z = a x + b y + c$
by setting:
{{begin-eqn}}
{{eqn | l = a
      | r = \dfrac {-\alpha_1} {\alpha_3}
}}
{{eqn | l = b
      | r = \dfrac {-\alpha_2} {\alpha_3}
}}
{{eqn | l = c
      | r = \dfrac {-\gamma} {\alpha_3}
}}
{{end-eqn}}
We use the technique of Elimination of Constants by Partial Differentiation.
We see we have:
:$1$ dependent variable, that is: $z$
:$2$ independent variables, that is: $x$ and $y$
:$3$ constants, that is: $a$, $b$ and $c$.
Taking the partial first derivatives {{WRT|Differentiation}} $x$ and $y$, we get:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial z} {\partial x}
      | r = a
}}
{{eqn | l = \dfrac {\partial z} {\partial y}
      | r = b
}}
{{end-eqn}}
$2$ equations are insufficient to dispose of $3$ constants, so the process continues by taking the partial second derivatives {{WRT|Differentiation}} $x$ and $y$:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial^2 z} {\partial x^2}
      | r = 0
}}
{{eqn | l = \dfrac {\partial^2 z} {\partial x \partial y}
      | r = 0
}}
{{eqn | l = \dfrac {\partial^2 z} {\partial y^2}
      | r = 0
}}
{{end-eqn}}
and the system of partial differential equations has been established.
{{qed}}
Theorem: Inverse of Vandermonde Matrix/Eisinberg Formula

Let:
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop = 1}^n \paren {x - x_k}
      | r = a_n x^n + \sum_{m \mathop = 0}^{n - 1} a_m x^m
      | c = Polynomial expansion in powers of $x$
}}
{{eqn | r = x^n + \sum_{m \mathop = 0}^{n - 1} \paren {-1}^{n - m} \map {e_{n - m} } {x_1, \ldots, x_n} \, x^m
      | c = Viète's Formulas and {{Defof|Elementary Symmetric Function}}
}}
{{eqn | l = W_n 
      | r = 
<nowiki>\begin{bmatrix}
  1     & x_1    & \cdots & {x_1}^{n - 1} \\
  1     & x_2    & \cdots & {x_2}^{n - 1} \\
\vdots  & \vdots & \ddots & \vdots        \\
  1     & x_n    & \cdots & {x_n}^{n - 1} \\
\end{bmatrix}</nowiki>
      | c = {{Defof|Vandermonde Matrix|subdef = Formulation 1}} of Order $n$
}}
{{end-eqn}}
Let $W_n$ have a matrix inverse $W_n^{-1} = \begin {bmatrix} d_{ij} \end {bmatrix}$. 
Let $a_n = \map {e_0} {x_1, \ldots, x_n} = 1$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = d_{ij}
      | r = \frac {\ds \sum_{k \mathop = 0}^{n - i} a_{i + k} \, {x_j}^k} {\ds \prod_{\substack {m \mathop = 1 \\ m \mathop \ne j} }^n \paren {x_j - x_m} }
      | c = for $i, j = 1, \ldots, n$
}}
{{eqn | r = \frac {\ds \sum_{k \mathop = 0}^{n - i} \paren {-1}^{n - i - k} \map {e_{n - i - k} } {x_1, \ldots, x_n} \, {x_j}^k} {\ds \prod_{\substack {m \mathop = 1 \\ m \mathop \ne j} }^n \paren {x_j - x_m} }
      | c = for $i, j = 1, \ldots, n$
}}
{{end-eqn}}

Proof:
=== Lemma 1 ===
Given values $z_1, \ldots, z_{p + 1}$ and $1 \le m \le p$, then:
{{begin-eqn}}
{{eqn | n = 2
      | l = \ds \map {e_m} {z_1, \ldots, z_p, z_{p + 1} }
      | r = z_{p + 1} \map {e_{m - 1} } {z_1, \ldots, z_p} + \map {e_m} {z_1, \ldots, z_p}
      | c = Recursion Property of Elementary Symmetric Function
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Linear First Order ODE/dy = f(x) dx

Let $f: \R \to \R$ be an integrable real function.
The linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} = \map f x$
has the general solution:
:$y = \ds \int \map f x \rd x + C$
where $\ds \int \map f x \rd x$ denotes the primitive of $f$.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x}
      | r = \map f x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \d y
      | r = \int \map f x \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \int \map f x \rd x
      | c = Primitive of Constant
}}
{{end-eqn}}
{{qed}}
Theorem: Linear First Order ODE/dy = f(x) dx/Initial Condition

Consider the linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} = \map f x$
subject to the initial condition:
:$y = y_0$ when $x = x_0$
$(1)$ has the particular solution:
:$y = y_0 + \ds \int_{x_0}^x \map f \xi \rd \xi$
where $\ds \int \map f x \rd x$ denotes the primitive of $f$.

Proof:
It is seen that $(1)$ is an instance of the first order ordinary differential equation:
:$\dfrac {\d y} {\d x} = \map f {x, y}$
which is:
:subject to an initial condition: $\tuple {x_0, y_0}$
where:
:$\map f {x, y}$ is actually $\map f x$
From Solution to First Order Initial Value Problem, this problem is equivalent to the integral equation:
:$\ds y = y_0 + \int_{x_0}^x \map f {\xi, \map y \xi} \rd \xi$
As $\map y \xi$ does not contribute towards $\map f x$, it can be ignored.
Hence we have:
:$\ds y = y_0 + \int_{x_0}^x \map f \xi \rd \xi$
{{qed}}
Theorem: Solution by Integrating Factor/Examples/y' - 3y = sin x

The linear first order ODE:
:$\dfrac {\d y} {\d x} - 3 y = \sin x$
has the general solution:
:$y = \dfrac 1 {10} \paren {3 \sin x - \cos x} + C e^{3 x}$

Proof:
This is a linear first order ODE in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x$
where:
:$\map P x y = -3 y$
:$\map Q x = \sin x$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = \int -3 \rd x
      | c = 
}}
{{eqn | r = -3 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{-3 x}
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor:
{{begin-eqn}}
{{eqn | l = \dfrac {\d} {\d x} \paren {e^{-3 x} y}
      | r = e^{-3 x} \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{-3 x} y
      | r = \int e^{-3 x} \sin x \rd x + C
      | c = 
}}
{{eqn | r = \frac {e^{3 x} \paren {3 \sin x - \cos x} } {3^2 + 1^2} + C
      | c = Primitive of $e^{a x} \sin b x$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \dfrac 1 {10} \paren {3 \sin x - \cos x} + C e^{3 x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Solution by Integrating Factor/Examples/y' - 3y = sin x

The linear first order ODE:
:$\dfrac {\d y} {\d x} - 3 y = \sin x$
has the general solution:
:$y = \dfrac 1 {10} \paren {3 \sin x - \cos x} + C e^{3 x}$

Proof:
This is a linear first order ODE with constant coefficents in the form:
:$\dfrac {\d y} {\d x} + a y = \map Q x$
where:
:$a = -3$
:$\map Q x = \sin x$
Thus from Solution to Linear First Order ODE with Constant Coefficients:
{{begin-eqn}}
{{eqn | l = y
      | r = e^{-3 x} \int e^{3 x} \sin x \rd x + C e^{-3 x}
      | c = 
}}
{{eqn | r = e^{-3 x} \cdot \frac {e^{3 x} \paren {3 \sin x - \cos x} } {3^2 + 1^2} + C
      | c = Primitive of $e^{a x} \sin b x$
}}
{{eqn | r = \dfrac 1 {10} \paren {3 \sin x - \cos x} + C e^{3 x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Solution to Linear First Order ODE with Constant Coefficients

A linear first order ODE with constant coefficients in the form:
:$(1): \quad \dfrac {\d y} {\d x} + a y = \map Q x$
has the general solution:
:$\ds y = e^{-a x} \paren {\int e^{a x} \map Q x \rd x + C}$

Proof:
From the Product Rule for Derivatives:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {e^{a x} y}
      | r = e^{a x} \cdot \dfrac {\d y} {\d x} + y \cdot a e^{a x}
      | c = 
}}
{{eqn | r = e^{a x} \paren {\dfrac {\d y} {\d x} + a y}
      | c = 
}}
{{end-eqn}}
Hence, multiplying $(1)$ all through by $e^{\int a \rd x}$:
:$\map {\dfrac \d {\d x} } {e^{a x} y} = e^{a x} \map Q x$
Integrating {{WRT|Integration}} $x$ now gives:
:$\ds e^{a x} y = \int e^{a x} \map Q x \rd x + C$
whence we get the result by dividing by $e^{a x}$.
{{qed}}
Theorem: Solution to Linear First Order ODE with Constant Coefficients

A linear first order ODE with constant coefficients in the form:
:$(1): \quad \dfrac {\d y} {\d x} + a y = \map Q x$
has the general solution:
:$\ds y = e^{-a x} \paren {\int e^{a x} \map Q x \rd x + C}$

Proof:
This is a specific instance of Solution to Linear First Order Ordinary Differential Equation:
{{:Solution to Linear First Order Ordinary Differential Equation}}
In this instance, we have:
:$\map P x = a$
Hence:
:$\ds \int \map P x = a x$
and the result follows.
{{qed}}
Theorem: Solution to Linear First Order ODE with Constant Coefficients/With Initial Condition

Consider the linear first order ODE with constant coefficients in the form:
:$(1): \quad \dfrac {\d y} {\d x} + a y = \map Q x$
with initial condition $\tuple {x_0, y_0}$
Then $(1)$ has the particular solution:
:$\ds y = e^{-a x} \int_{x_0}^x e^{a \xi} \map Q \xi \rd \xi + y_0 e^{a \paren {x - x_0} }$

Proof:
From Solution to Linear First Order ODE with Constant Coefficients, the general solution to $(1)$ is:
:$(2): \quad \ds y = e^{-a x} \int e^{a x} \map Q x \rd x + C e^{-a x}$
Let $y = y_0$ when $x = x_0$.
We have:
:$(3): \ds \quad y_0 = e^{-a x_0} \int e^{a x_0} \map Q {x_0} \rd x_0 + C e^{-a x_0}$
Thus:
{{begin-eqn}}
{{eqn | l = y e^{a x}
      | r = \int e^{a x} \map Q x \rd x + C
      | c = multiplying $(2)$ by $e^{a x}$
}}
{{eqn | l = y_0 e^{a x_0}
      | r = \int e^{a x_0} \map Q {x_0} \rd x + C
      | c = multiplying $(3)$ by $e^{a x}$
}}
{{eqn | ll= \leadsto
      | l = y e^{a x}
      | r = y_0 e^{a x_0} + \int e^{a x} \map Q x \rd x - \int e^{a x_0} \map Q {x_0} \rd x
      | c = substituting for $C$ and rearranging
}}
{{eqn | r = y_0 e^{a x_0} + \int_{x_0}^x e^{a \xi} \map Q \xi \rd \xi
      | c = Fundamental Theorem of Calculus
}}
{{eqn | ll= \leadsto
      | l = y
      | r = e^{a x} \int_{x_0}^x e^{a \xi} \map Q \xi \rd \xi + y_0 e^{-a \paren {x - x_0} }
      | c = dividing by $e^{a x}$ and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Solution by Integrating Factor/Examples/y' + y = x^-1

Consider the linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} + y = \dfrac 1 x$
with the initial condition $\tuple {1, 0}$.
This has the particular solution:
:$y = \ds e^{-x} \int_1^x \dfrac {e^\xi \rd \xi} \xi$

Proof:
This is a linear first order ODE with constant coefficents in the form:
:$\dfrac {\d y} {\d x} + a y = \map Q x$
where:
:$a = 1$
:$\map Q x = \dfrac 1 x$
with the initial condition $y = 0$ when $x = 1$.
Thus from Solution to Linear First Order ODE with Constant Coefficients with Initial Condition:
{{begin-eqn}}
{{eqn | l = y
      | r = e^{-x} \int_1^x \dfrac {e^\xi \rd \xi} \xi + 0 \cdot e^{x - 1}
      | c = 
}}
{{eqn | r = e^{-x} \int_1^x \dfrac {e^\xi \rd \xi} \xi
      | c = 
}}
{{end-eqn}}
From Primitive of $\dfrac {e^x} x$ has no Solution in Elementary Functions, further work on this is not trivial.
{{qed}}
Theorem: General Solution equals Particular Solution plus Complementary Function

Consider the linear first order ODE with constant coefficients:
:$(1): \quad \dfrac {\d y} {\d x} + a y = \map Q x$
The general solution to $(1)$ consists of:
:the particular solution to $(1)$ for which the constant of integration is $0$
plus:
:the complementary function to $(1)$.

Proof:
From Solution to Linear First Order ODE with Constant Coefficients, $(1)$ has the general solution:
:$\ds y = e^{-a x} \int e^{a x} \map Q x \rd x + C e^{-a x}$
Setting $C = 0$ we get:
:$\ds y = e^{-a x} \int e^{a x} \map Q x \rd x$
which is a particular solution to $(1)$
By definition, the complementary function to $(1)$ is the general solution to the reduced equation:
:$\dfrac {\d y} {\d x} + a y = 0$
From First Order ODE: $\dfrac {\d y} {\d x} = k y$, that general solution of $(1)$ is:
:$y = C e^{-a x}$
Hence the result.
{{qed}}
Theorem: Linear Second Order ODE/y'' + 2 y' + 2 y = 0

The second order ODE:
:$(1): \quad y' ' + 2 y' + 2 y = 0$
has the general solution:
:$y = e^{-x} \paren {A \cos x + B \sin 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 + 2 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = -1 + i$
:$m_2 = -1 - i$
These are complex conjugates.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = e^{-x} \paren {A \cos x + B \sin x}$
{{qed}}
Theorem: Linear Second Order ODE/y'' + 2 y' + 2 y = 0/Verification

The equation:
:$(1): \quad y = e^{-x} \paren {A \cos x + B \sin x}$
is a set of solutions to the second order ODE:
:$y' ' + 2 y' + 2 y = 0$

Proof:
Differentiating $(1)$ twice {{WRT|Differentiation}} $x$ gives:
{{begin-eqn}}
{{eqn | l = y'
      | r = -e^{-x} \paren {A \cos x + B \sin x} + e^{-x} \paren {-A \sin x + B \cos x}
      | c = 
}}
{{eqn | r = e^{-x} \paren {\paren {B - A} \cos x - \paren {A + B} \sin x}
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = y' '
      | r = -e^{-x} \paren {\paren {B - A} \cos x - \paren {A + B} \sin x} + e^{-x} \paren {-\paren {B - A} \sin x - \paren {A + B} \cos x}
      | c = 
}}
{{eqn | r = e^{-x} \paren {-2 B \cos x + 2 A \sin x}
      | c = rearranging
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = y' ' + 2 y' + 2 y
      | r = e^{-x} \paren {-2 B \cos x + 2 A \sin x} + 2 \paren {e^{-x} \paren {\paren {B - A} \cos x - \paren {A + B} \sin x} } + 2 e^{-x} \paren {A \cos x + B \sin x}
      | c = 
}}
{{eqn | r = e^{-x} \paren {\paren {-2 B + 2 \paren {B - A} + 2 A} \cos x - \paren {2 A - 2 \paren {A + B} + 2 B} \sin x}
      | c = rearranging
}}
{{eqn | r = 0
      | c = simplifying
}}
{{end-eqn}}
thus demonstrating that $(1)$ is indeed a solution to the second order ODE given.
{{qed}}