avewright/proofwiki-math huggingface dataset:
Theorem: Linear Second Order ODE/y'' - 7 y' - 5 y = x^3 - 1

The second order ODE:
:$(1): \quad y'' - 7 y' - 5 y = x^3 - 1$
has the general solution:
:$y = C_1 \, \map \exp {\paren {\dfrac 7 2 + \dfrac {\sqrt {69} } 2} x} + C_2 \, \map \exp {\paren {\dfrac 7 2 - \dfrac {\sqrt {69} } 2} x} + \dfrac 1 {625} \paren {-125 x^3 + 525 x^2 - 1620 x + 2603}$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -7$
:$q = -5$
:$\map R x = x^3 - 1$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$(2): \quad y'' - 7 y' - 5 y = 0$
From Linear Second Order ODE: $y'' - 7 y' - 5 y = 0$, this has the general solution:
:$y_g = C_1 \, \map \exp {\paren {\dfrac 7 2 + \dfrac {\sqrt {69} } 2} x} + C_2 \, \map \exp {\paren {\dfrac 7 2 - \dfrac {\sqrt {69} } 2} x}$
We have that:
:$\map R x = x^3 - 1$
and it is noted that $x^3 - 1$ is not itself a particular solution of $(2)$.
So from the Method of Undetermined Coefficients for Polynomials:
:$y_p = A_0 + A_1 x + A_2 x^2 + A_3 x^3$
for $A_n$ to be determined.
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = A_0 + A_1 x + A_2 x^2 + A_3 x^3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = A_1 + 2 A_2 x + 3 A_3 x^2
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_p}''
      | r = 2 A_2 + 6 A_3 x
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = 2 A_2 + 6 A_3 x - 7 \paren {A_1 + 2 A_2 x + 3 A_3 x^2} - 5 \paren {A_0 + A_1 x + A_2 x^2 + A_3 x^3}
      | r = x^3 - 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -5 A_3 x^3
      | r = x^3
      | c = equating powers
}}
{{eqn | l = \paren {-21 A_3 - 5 A_2} x^2
      | r = 0
      | c = 
}}
{{eqn | l = \paren {6 A_3 - 14 A_2 - 5 A_1} x
      | r = 0
      | c = 
}}
{{eqn | l = 2 A_2 - 7 A_1 - 5 A_0
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_3
      | r = -\dfrac 1 5
      | c = 
}}
{{eqn | l = A_2
      | r = -\dfrac {21} 5 A_3
      | c = 
}}
{{eqn | r = -\dfrac {21} {25}
      | c = 
}}
{{eqn | l = 5 A_1
      | r = -\dfrac 6 5 - \dfrac {294} {25}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_1
      | r = -\dfrac {324} {125}
      | c = 
}}
{{eqn | l = 5 A_0
      | r = \dfrac {42} {25} + \dfrac {2268} {125} + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_0
      | r = \dfrac {2603} {625}
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 \, \map \exp {\paren {\dfrac 7 2 + \dfrac {\sqrt {69} } 2} x} + C_2 \, \map \exp {\paren {\dfrac 7 2 - \dfrac {\sqrt {69} } 2} x} + \dfrac 1 {625} \paren {-125 x^3 + 525 x^2 - 1620 x + 2603}$
{{qed}}
Theorem: Linear Second Order ODE/y'' - 7 y' - 5 y = 0

The second order ODE:
:$(1): \quad y' ' - 7 y' - 5 y = 0$
has the general solution:
:$y = C_1 \, \map \exp {\paren {\dfrac 7 2 + \dfrac {\sqrt {69} } 2} x} + C_2 \, \map \exp {\paren {\dfrac 7 2 - \dfrac {\sqrt {69} } 2} 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 - 7 m - 5 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
{{begin-eqn}}
{{eqn | l = m
      | r = \dfrac {7 \pm \sqrt {7^2 - 4 \times 1 \times \paren {-5} } } 2
      | c = 
}}
{{eqn | r = \dfrac 7 2 \pm \dfrac {\sqrt {69} } 2
      | c = 
}}
{{end-eqn}}
These are real and unequal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 \, \map \exp {\paren {\dfrac 7 2 + \dfrac {\sqrt {69} } 2} x} + C_2 \, \map \exp {\paren {\dfrac 7 2 - \dfrac {\sqrt {69} } 2} x}$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
ozj875r6s8x44232z07q7pw7x2a0m3p
Theorem: Convergent Sequence is Cauchy Sequence/Normed Vector Space

Let $\struct{X, \norm{\,\cdot\,} }$ be a normed vector space.
Every convergent sequence in $X$ is a Cauchy sequence.

Proof:
Let $\sequence {x_n}$ be a sequence in $X$ that converges to the limit $L \in X$.
Let $\epsilon > 0$. 
Then also $\dfrac \epsilon 2 > 0$.
Because $\sequence {x_n}$ converges to $L$, we have:
:$\exists N: \forall n > N: \norm {x_n - L} < \dfrac \epsilon 2$
So if $m > N$ and $n > N$, then:
{{begin-eqn}}
{{eqn | l = \norm {x_n - x_m}
      | r = \norm {x_n - L + L - x_m}
}}
{{eqn | o = \le
      | r = \norm {x_n - L} + \norm {x_m - L}
      | c = Triangle Inequality Axiom of Norm
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \frac \epsilon 2
      | c = (by choice of $N$)
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Thus $\sequence {x_n}$ is a Cauchy sequence.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 3 y' + 2 y = 5 exp 3 x

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

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -3$
:$q = 2$
:$\map R x = 5 e^{3 x}$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - 3 y' + 2 y = 0$
From Linear Second Order ODE: $y'' - 3 y' + 2 y = 0$, this has the general solution:
:$y_g = C_1 e^x + C_2 e^{2 x}$
We have that:
:$\map R x = 5 e^{3 x}$
and so from the Method of Undetermined Coefficients for the Exponential function:
:$y_p = \dfrac {K e^{a x} } {a^2 + p a + q}$
where:
:$K = 5$
:$a = 3$
:$p = -3$
:$q = 2$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = \dfrac {5 e^{3 x} } {3^2 - 3 \times 3 + 2}
      | c = 
}}
{{eqn | r = \dfrac {5 e^{3 x} } {9 - 9 + 2}
      | c = 
}}
{{eqn | r = \dfrac {5 e^{3 x} } 2
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^x + C_2 e^{2 x} + \dfrac {5 e^{3 x} } 2$
{{qed}}
Theorem: Linear Second Order ODE/y'' - y = 3 exp -x

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

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = 0$
:$q = -1$
:$\map R x = 3 e^{-x}$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - y = 0$
From Linear Second Order ODE: $y'' - y = 0$, this has the general solution:
:$y_g = C_1 e^x + C_2 e^{-x}$
We have that:
:$\map R x = 3 e^{-x}$
and so from the Method of Undetermined Coefficients for the Exponential function:
:$y_p = \dfrac {K x e^{a x} } {2 a + p}$
where:
:$K = 3$
:$a = -1$
:$p = 0$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = \dfrac {3 x e^{-x} } {2 \times \paren {-1} + 0}
      | c = 
}}
{{eqn | r = \dfrac {3 x e^{-x} } {-2}
      | c = 
}}
{{eqn | r = -\dfrac {3 x e^{-x} } 2
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^x + C_2 e^{-x} - \dfrac {3 x e^{-x} } 2$
{{qed}}
Theorem: Linear Second Order ODE/y'' - 2 y' + y = exp x

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

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -2$
:$q = 1$
:$\map R x = e^x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - 2 y' + y = 0$
From Linear Second Order ODE: $y'' - 2 y' + y = 0$, this has the general solution:
:$y_g = C_1 e^x + C_2 x e^x$
We have that:
:$\map R x = e^x$
and so from the Method of Undetermined Coefficients for the Exponential function:
:$y_p = \dfrac {K x^2 e^{a x} } 2$
where:
:$K = 1$
:$a = 1$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = \dfrac {x^2 e^x} 2
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^x + C_2 x e^x + \dfrac {x^2 e^x} 2$
{{qed}}
Theorem: Linear Second Order ODE/y'' - 2 y' - 5 y = 0

The second order ODE:
:$(1): \quad y' ' - 2 y' - 5 y = 0$
has the general solution:
:$y = C_1 \map \exp {\paren {1 + \sqrt 6} x} + C_2 \map \exp {\paren {1 - \sqrt 6} 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 - 5 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = 1 + \sqrt 6$
:$m_2 = 1 - \sqrt 6$
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 \map \exp {\paren {1 + \sqrt 6} x} + C_2 \map \exp {\paren {1 - \sqrt 6} x}$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
8hroyxdat6gk274nlgxj3mwnbh2mvjq
Theorem: Linear Second Order ODE/y'' - 2 y' - 5 y = 2 cos 3 x - sin 3 x

The second order ODE:
:$(1): \quad y'' - 2 y' - 5 y = 2 \cos 3 x - \sin 3 x$
has the general solution:
:$y = C_1 \map \exp {\paren {1 + \sqrt 6} x} + C_2 \map \exp {\paren {1 - \sqrt 6} x} + \dfrac 1 {116} \paren {\sin 3 x - 17 \cos 3 x}$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -2$
:$q = -5$
:$\map R x = 2 \cos 3 x - \sin 3 x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - 2 y' - 5 y = 0$
From Linear Second Order ODE: $y'' - 2 y' - 5 y = 0$, this has the general solution:
:$y_g = C_1 \map \exp {\paren {1 + \sqrt 6} x} + C_2 \map \exp {\paren {1 - \sqrt 6} x}$
We have that:
:$\map R x = 2 \cos 3 x - \sin 3 x$
and it is noted that $2 \cos 3 x - \sin 3 x$ is not itself a particular solution of $(2)$.
We then determine the particular solution:
Theorem: Linear Second Order ODE/y'' - 2 y' - 5 y = 2 cos 3 x - sin 3 x/Particular Solution

The second order ODE:
:$(1): \quad y'' - 2 y' - 5 y = 2 \cos 3 x - \sin 3 x$
has a particular solution:
:$y_p = \dfrac 1 {116} \paren {\sin 3 x - 17 \cos 3 x}$

Proof:
From Linear Second Order ODE: $y'' - 2 y' - 5 y = 0$, we have established that the general solution to $(1)$ is:
:$y_g = C_1 \map \exp {\paren {1 + \sqrt 6} x} + C_2 \map \exp {\paren {1 - \sqrt 6} x}$
Theorem: Linear Second Order ODE/y'' + 4 y = 3 sin 2 x

The second order ODE:
:$(1): \quad y'' + 4 y = 3 \sin 2 x$
has the general solution:
:$y = C_1 \sin k x + C_2 \cos k x - \dfrac 3 4 x \cos 2 x$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = 0$
:$q = 4$
:$\map R x = 3 \sin 2 x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$(2): \quad y'' + 4 y = 0$
From Linear Second Order ODE: $y'' + 4 y = 0$, this has the general solution:
:$y_g = C_1 \sin 2 x + C_2 \cos 2 x$
It is noted that $3 \sin 2 x$ is a particular solution of $(2)$.
So from the Method of Undetermined Coefficients for Sine and Cosine:
:$y_p = A x \sin 2 x + B x \cos 2 x$
where $A$ and $B$ are to be determined.
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = A x \sin 2 x + B x \cos 2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = 2 A x \cos 2 x - 2 B x \sin 2 x + A \sin 2 x + B \cos 2 x
      | c = Derivative of Sine Function, Derivative of Cosine Function, Product Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_p}''
      | r = -4 A x \sin 2 x - 4 B x \cos 2 x + 2 A \cos 2 x - 2 B \sin 2 x + 2 A \cos 2 x - 2 B \sin 2 x
      | c = Derivative of Sine Function, Derivative of Cosine Function, Product Rule for Derivatives
}}
{{eqn | r = -4 A x \sin 2 x - 4 B x \cos 2 x + 4 A \cos 2 x - 4 B \sin 2 x
      | c = 
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = -4 A x \sin 2 x - 4 B x \cos 2 x + 4 A \cos 2 x - 4 B \sin 2 x + 4 \paren {A x \sin 2 x + B x \cos 2 x}
      | r = 3 \sin 2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A \paren {4 - 4} x \sin 2 x - 4 B \sin 2 x
      | r = 3 \sin 2 x
      | c = equating coefficients
}}
{{eqn | l = B \paren {4 - 4} x \cos 2 x + 4 A \cos 2 x
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -4 B
      | r = 3
      | c = 
}}
{{eqn | l = 4 A
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = B
      | r = -\dfrac 3 4
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 \sin k x + C_2 \cos k x - \dfrac 3 4 x \cos 2 x$
is the general solution to $(1)$.
{{qed}}
Theorem: Cauchy Sequence is Bounded/Normed Vector Space

Let $V = \struct {X, \norm {\,\cdot\,} }$ be a normed vector space.
Every Cauchy sequence in $X$ is bounded.

Proof:
Let $\sequence {x_n} $ be a Cauchy sequence in $V$.
Then by definition:
:$\forall \epsilon \in \R_{>0}: \exists N \in \N : \forall n, m \ge N: \norm {x_n - x_m} < \epsilon$
Let $N$ satisfy:
:$\forall n, m \ge N: \norm {x_n - x_m} < 1$
Let $m = N + 1 > N$.
Then $\forall n \ge N$:
{{begin-eqn}}
{{eqn | l = \norm {x_n}
      | r = \norm {x_n - x_{N + 1} + x_{N + 1} }
}}
{{eqn | o = \le
      | r = \norm {x_n - x_{N + 1} } + \norm {x_{N + 1} }
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = \le
      | r = 1 + \norm {x_{N + 1} }
}}
{{end-eqn}}
Let $M = \max \set {\norm {x_1}, \norm {x_2}, \dots, \norm {x_N}, 1 + \norm {x_{N + 1} } }$.
Then:
:$\forall n < N: \norm {x_n} \le M$
:$\forall n \ge N: \norm {x_n} \le 1 + \norm {x_{N + 1} } \le M$
It follows by definition that $\sequence {x_n}$ is bounded.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 4 y' - 5 y = 0

The second order ODE:
:$(1): \quad y' ' - 4 y' - 5 y = 0$
has the general solution:
:$y = C_1 e^{5 x} + C_2 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 - 4 m - 5 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = 5$
:$m_2 = -1$
These are real and unequal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 e^{5 x} + C_2 e^{-x}$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
6xsrpee81d3d8m97oa5fektc7uiesn5
Theorem: Linear Second Order ODE/y'' - 4 y' - 5 y = x^2/y(0) = 1, y'(0) = -1

Consider the second order ODE:
:$(1): \quad y'' - 4 y' - 5 y = x^2$
whose initial conditions are:
:$y = 1$ when $x = 0$
:$y' = -1$ when $x = 0$
$(1)$ has the particular solution:
:$y = \dfrac {e^{5 x} } {375} + \dfrac {4 e^{-x} } 3 - \dfrac {x^2} 5 + \dfrac {8 x} {25} - \dfrac {42} {125}$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -4$
:$q = -5$
:$\map R x = x^2$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$(2): \quad y'' - 4 y' - 5 y = 0$
From Linear Second Order ODE: $y'' - 4 y' - 5 y = 0$, this has the general solution:
:$y_g = C_1 e^{5 x} + C_2 e^{-x}$
We have that:
:$\map R x = x^2$
and it is noted that $x^2$ is not itself a particular solution of $(2)$.
So from the Method of Undetermined Coefficients for Polynomials:
:$y_p = A_0 + A_1 x + A_2 x^2$
for $A_n$ to be determined.
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = A_0 + A_1 x + A_2 x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = A_1 + 2 A_2 x
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_p}''
      | r = 2 A_2
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = 2 A_2 - 4 \paren {A_1 + 2 A_2 x} - 5 \paren {A_0 + A_1 x + A_2 x^2}
      | r = x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -5 A_2 x^2
      | r = x^2
      | c = equating coefficients of powers
}}
{{eqn | l = \paren {-8 A_2 - 5 A_1} x
      | r = 0
      | c = 
}}
{{eqn | l = 2 A_2 - 4 A_1 - 5 A_0
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_2
      | r = -\dfrac 1 5
      | c = 
}}
{{eqn | l = 5 A_1
      | r = \dfrac 8 5
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_1
      | r = \dfrac 8 {25}
      | c = 
}}
{{eqn | l = 5 A_0
      | r = -\dfrac 2 5 - \dfrac {4 \times 8} {25}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_0
      | r = -\dfrac {42} {125}
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^{5 x} + C_2 e^{-x} - \dfrac 1 5 x^2 + \dfrac 8 {25} x - \dfrac {42} {125}$
Differentiating {{WRT|Differentiation}} $x$:
:$y' = 5 C_1 e^{5 x} - C_2 e^{-x} - \dfrac 2 5 x + \dfrac 8 {25}$
Substituting the initial conditions, remembering that $e^0 = 1$:
{{begin-eqn}}
{{eqn | l = 1
      | r = C_1 + C_2 - \dfrac {42} {125}
      | c = setting $y = 1$ when $x = 0$
}}
{{eqn | l = -1
      | r = 5 C_1 - C_2 + \dfrac 8 {25}
      | c = setting $y' = -1$ when $x = 0$
}}
{{eqn | ll= \leadsto
      | l = -\dfrac 2 {125} + 6 C_1
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C_1
      | r = \dfrac 1 {375}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C_2
      | r = 1 - 5 A + \dfrac 8 {25}
      | c = 
}}
{{eqn | r = 1 + \dfrac 1 {75} + \dfrac 8 {27}
      | c = 
}}
{{eqn | r = \dfrac 4 3
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 2 y' + y = 1 over 1 + e^x

The second order ODE:
:$(1): \quad y'' - 2 y' + y = \dfrac 1 {1 + e^x}$
has a particular solution:
:$y = 1 + e^x \ds \int \map \ln {1 + e^{-x} } \rd x$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {D^2 - 2 D + 1} y
      | r = \dfrac 1 {1 + e^x}
      | c = expressing $(1)$ in a different form
}}
{{eqn | ll= \leadsto
      | l = \paren {D^2 - 1}^2 y
      | r = \dfrac 1 {1 + e^x}
      | c = and in a different form again
}}
{{eqn | ll= \leadsto
      | l = \paren {D - 1} z
      | r = \dfrac 1 {1 + e^x}
      | c = putting $\paren {D - 1} y = z$
}}
{{eqn | ll= \leadsto
      | l = \map D {z e^{-x} }
      | r = \dfrac {e^{-x} } {1 + e^x}
      | c = Solution to Linear First Order ODE with Constant Coefficients: integrating factor $e^x$
}}
{{eqn | r = \dfrac {e^{-2 x} } {1 + e^{-x} }
      | c = multiplying top and bottomof {{RHS}} by $e^{-x}$
}}
{{eqn | ll= \leadsto
      | l = z e^{-x}
      | r = \int \dfrac {e^{-2 x} } {1 + e^{-x} } \rd x
      | c = integrating both sides {{WRT|Integration}} $x$
}}
{{eqn | r = -\int \dfrac u {1 + u} \rd u
      | c = Integration by Substitution: setting $e^{-x} = u$
}}
{{eqn | r = -\int 1 - \dfrac 1 {1 + u} \rd u
      | c = 
}}
{{eqn | r = -u + \map \ln {1 + u}
      | c = Primitive of Constant, Primitive of Reciprocal
}}
{{eqn | r = -e^{-x} + \map \ln {1 + e^{-x} }
      | c = substituting back for $u$
}}
{{end-eqn}}
Then we need to solve:
{{begin-eqn}}
{{eqn | l = \paren {D - 1}y
      | r = z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map D {y e^{-x} }
      | r = z e^{-x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y e^{-x}
      | r = e^{-x} + \int \map \ln {1 + e^{-x} } \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = 1 + e^x \int \map \ln {1 + e^{-x} } \rd x
      | c = 
}}
{{end-eqn}}
and so on.
{{Qed}}
Theorem: ODE/(D^4 - 1) y = sin x

The second order ODE:
:$(1): \quad \paren {D^4 - 1} y' = \sin x$
has a general solution:
:$y = C_1 e^x + C_2 e^{-x} + C_3 \sin x + C_4 \cos x + \dfrac {x \cos x} 4$

Proof:
First we solve the reduced equation of $(1)$:
:$(2): \quad \paren {D^4 - 1} y' = 0$
The auxiliary equation of $(1)$ is:
:$(3): \quad: m^4 - 1 = 0$
From Complex $4$th Roots of Unity, the roots of $(2)$ are:
:$m_1 = 1$
:$m_2 = i$
:$m_3 = -1$
:$m_4 = -i$
So from Solution of Constant Coefficient Linear nth Order ODE, the general solution of $(2)$ is:
:$y_g = C_1 e^x + C_2 e^{-x} + C_3 \sin x + C_4 \cos x$
Because $\sin x$ is already a solution of $(2)$, we try:
:$y = A x e^{i x}$
with a view to taking the real part in due course.
{{begin-eqn}}
{{eqn | l = y
      | r = A x e^{i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y'
      | r = A e^{i x} + A i x e^{i x}
      | c = 
}}
{{eqn | r = A \paren {1 + i x} e^{i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y''
      | r = A \paren {1 + i x} i e^{i x} + A i e^{i x}
      | c = 
}}
{{eqn | r = A \paren {2 i - x} e^{i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^{\paren 3}
      | r = A \paren {2 i - x} i e^{i x} - A e^{i x}
      | c = 
}}
{{eqn | r = A \paren {-3 - i x} e^{i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^{\paren 4}
      | r = A \paren {-3 - i x} i e^{i x} - i e^{i x}
      | c = 
}}
{{eqn | r = A \paren {x - 4 i} e^{i x}
      | c = 
}}
{{end-eqn}}
It follows that
:$-4 i A - 1$
and so:
:$A = -\dfrac 1 4$
Thus a particular solution to $(1)$ can be given as:
{{begin-eqn}}
{{eqn | l = y_p
      | r = \map \Im {\dfrac 1 4 i x e^{i x} }
      | c = 
}}
{{eqn | r = \dfrac {x \cos x} 4
      | c = 
}}
{{end-eqn}}
and the general solution is:
:$y = C_1 e^x + C_2 e^{-x} + C_3 \sin x + C_4 \cos x + \dfrac {x \cos x} 4$
{{Qed}}
Theorem: P-adic Unit has Norm Equal to One

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ denote the $p$-adic integers.
Let $x \in \Q_p$.
Then x is a $p$-adic unit {{iff}} $\norm x_p = 1$

Proof:
=== Necessary Condition ===
Let $x$ be a $p$-adic unit.
Then:
:$x \in \Z_p$
:$x^{-1} \in \Z_p$
By definition of the $p$-adic integers:
:$\norm x_p \le 1$
:$\norm {x^{-1} }_p \le 1$
From Norm of Inverse in Division Ring:
:$\norm x_p \ge 1$
It follows that:
:$\norm x_p = 1$
{{qed|lemma}}
Theorem: P-adic Number times P-adic Norm is P-adic Unit

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p^\times$ be the $p$-adic units.
Let $a \in \Q_p$.
Then there exists $n \in \Z$ such that:
:$p^n a \in \Z_p^\times$
where
:$p^n = \norm a_p$

Proof:
From P-adic Norm of p-adic Number is Power of p, there exists $v \in \Z$ such that $\norm a_p = p^{-v}$.
Let $n = -v$.
Now:
{{begin-eqn}}
{{eqn | l = \norm{p^n a}_p
      | r = \norm{p^n }_p \norm a_p
      | c = Norm axiom (N2) (Multiplicativity)
}}
{{eqn | r = p^{-n} \norm a_p
      | c = {{Defof|P-adic Norm|$p$-adic norm}} on the rational numbers
}}
{{eqn | r = p^{-n} p^{n}
      | c = Definition of $n$
}}
{{eqn | r = 1
}}
{{eqn | ll= \leadsto
      | l = p^n a
      | o = \in
      | r = \Z_p^\times
      | c = P-adic Unit has Norm Equal to One
}}
{{end-eqn}}
{{qed}}