avewright/proofwiki-math huggingface dataset:
Theorem: Topology Defined by Neighborhood System

Let $S$ be a set.
Let $\family {\NN_x}_{x \mathop \in S}$ be an indexed family where $\NN_x$ is non-empty set of subsets of $S$.
Assume that
:$(\text N 1): \quad \forall x \in S, U \in \NN_x: x \in U$
:$(\text N 2): \quad \forall x \in S, U \in \NN_x, y \in U:\exists V \in \NN_y: V \subseteq U$
:$(\text N 3): \quad \forall x \in S, U_1, U_2 \in \NN_x: \exists U \in \NN_x: U \subseteq U_1 \cap U_2$
Then $T = \struct {S, \tau}$ is a topological space where:
:$\ds \tau = \set {\bigcup \GG: \GG \subseteq \bigcup_{x \mathop \in S} \NN_x}$
Moreover, $\family {\NN_x}_{x \mathop \in S}$ is a neighborhood system of $T$.

Proof:
Define:
:$\BB := \ds \bigcup_{x \mathop \in S} \NN_x$
According to Topology Defined by Basis it should be proved that
:$(\text B 1): \quad \forall A_1, A_2 \in \BB: \forall x \in A_1 \cap A_2: \exists A \in \BB: x \in A \subseteq A_1 \cap A_2$
:$(\text B 2): \quad \forall x \in S: \exists A \in \BB: x \in A$
Ad $(\text B 1)$:
Let $A_1, A_2 \in \BB$.
Let $x \in A_1 \cap A_2$.
By definition of intersection:
:$x \in A_1 \land x \in A_2$
By definition of union:
:$\exists x_1 \in S: A_1 \in \NN_{x_1}$
and
:$\exists x_2 \in S: A_2 \in \NN_{x_2}$
By $(\text N 2)$:
:$\exists V_1 \in \NN_x: V_1 \subseteq A_1$
and
:$\exists V_2 \in \NN_x: V_2 \subseteq A_2$
By $(\text N 3)$:
:$\exists U \in \NN_x: U \subseteq V_1 \cap V_2$
By definition of union:
:$U \in \BB$
By Set Intersection Preserves Subsets:
:$V_1 \cap V_2 \subseteq A_1 \cap A_2$
Thus by Subset Relation is Transitive:
:$U \subseteq A_1 \cap A_2$
Ad $(\text B 2)$:
Let $x \in S$.
By definition of empty set:
:$\exists U: U \in \NN_x$
By $(\text N 1)$:
:$x \in U$
By definition of union:
:$U \in \BB$
Thus:
:$\exists A \in \BB: x \in A$
By definition of $\tau$ and $\BB$:
:$\tau = \set {\bigcup \GG: \GG \subseteq \BB}$
Thus by Topology Defined by Basis:
:$T = \struct {S, \tau}$ is a topological space
It remains to prove that
:$\family {\NN_x}_{x \mathop \in S}$ is a neighborhood system
Let $x \in S$.
Let $U \in \tau$.
By definition of $\tau$:
:$\exists \GG \subseteq \BB: U = \bigcup \GG$
Let $x \in U$.
By definition of union:
:$\exists V \in \GG: x \in V$
By definition of subset:
:$V \in \BB$
By definition of union:
:$\exists y \in S: V \in \NN_y$
By $(\text N 2)$:
:$\exists W \in \NN_x: W \subseteq V$
By Set is Subset of Union/Set of Sets:
:$V \subseteq U$
Thus by Subset Relation is Transitive:
:$\exists W \in \NN_x: W \subseteq U$
Thus by definition:
:$\NN_x$ is a local basis.
{{qed}}
Theorem: Orthogonal Trajectories/Examples/x + C exp -x

Consider the one-parameter family of curves:
:$(1): \quad y = x + C e^{-x}$
Its family of orthogonal trajectories is given by the equation:
:$x = y - 2 + C e^{-y}$
:600px

Proof:
We use the technique of formation of ordinary differential equation by elimination.
Differentiating $(1)$ {{WRT|Differentiation}} $x$ gives:
:$\dfrac {\d y} {\d x} = 1 - C e^{-x}$
Eliminating $C$:
{{begin-eqn}}
{{eqn | l = C
      | o = =
      | r = \frac {y - x} {e^{-x} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = 1 - \frac {y - x} {e^{-x} } e^{-x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x} + y
      | r = x + 1
      | c = 
}}
{{end-eqn}}
Thus from Orthogonal Trajectories of One-Parameter Family of Curves, the family of orthogonal trajectories is given by:
:$-\dfrac {\d y} {\d x} = - x = 1 - y$
The integrating factor is $e^y$, giving:
:$\ds e^y x = \int y e^y - e^y \rd y$
Using Primitive of $x e^{a x}$:
:$\ds \int y e^y \rd y = y e^y - e^y$
Thus we get:
:$e^y x = y e^y - e^y  - e^y + C$
which gives us:
:$x = y - 2 + C e^{-y}$
{{qed}}
Theorem: Differential Equation of Family of Linear Combination of Functions is Linear

Consider the one-parameter family of curves:
:$(1): \quad y = C \map f x + \map g x$
The differential equation that describes $(1)$ is linear and of first order.

Proof:
Differentiating $(1)$ {{WRT|Differentiation}} $x$ gives:
:$(2): \quad \dfrac {\d y} {\d x} = C \map {f'} x + \map {g'} x$
Rearranging $(1)$, we have:
:$C = \dfrac {y - \map g x} {\map f x}$
Substituting for $C$ in $(2)$:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x}
      | r = \dfrac {y - \map g x} {\map f x} \map {f'} x + \map {g'} x
      | c = 
}}
{{eqn | r = \dfrac {\map {f'} x} {\map f x} y - \dfrac {\map g x \map {f'} x} {\map f x} + \map g x
      | c = 
}}
{{end-eqn}}
which leaves:
:$\dfrac {\d y} {\d x} - \dfrac {\map {f'} x} {\map f x} y = \map g x \paren {1 - \dfrac {\map {f'} x} {\map f x} }$
which is linear and of first order.
{{qed}}
Theorem: Solution of Second Order Differential Equation with Missing Dependent Variable

Let $\map f {x, y', y' '} = 0$ be a second order ordinary differential equation in which the dependent variable $y$ is not explicitly present.
Then $f$ can be reduced to a first order ordinary differential equation, whose solution can be determined.

Proof:
Consider the second order ordinary differential equation:
:$(1): \quad \map f {x, y', y' '} = 0$
Let a new dependent variable $p$ be introduced:
:$y' = p$
:$y' ' = \dfrac {\d p} {\d x}$
Then $(1)$ can be transformed into:
:$(2): \quad \map f {x, p, \dfrac {\d p} {\d x} } = 0$
which is a first order ODE.
If $(2)$ has a solution which can readily be found, it will be expressible in the form:
:$(3): \quad \map g {x, p}$
which can then be expressed in the form:
:$\map g {x, \dfrac {\d y} {\d x} } = 0$
which is likewise subject to the techniques of solution of a first order ODE.
Hence such a second order ODE is reduced to the problem of solving two first order ODEs in succession.
{{qed}}
Theorem: Second Order ODE/x y'' - y' = 3 x^2

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

Proof:
The proof proceeds by using Solution of Second Order Differential Equation with Missing Dependent Variable.
Substitute $p$ for $y'$ in $(1)$:
:$x \dfrac {\d p} {\d x} - p = 3 x^2$
and divide through by $x$:
:$\dfrac {\d p} {\d x} - \dfrac p x = 3 x$
From:
:Linear First Order ODE: $y' - \dfrac y x = 3 x$
its solution is:
:$p = 3 x^2 + C_1 x$
Substituting back for $p$:
:$\dfrac {\d y} {\d x} = 3 x^2 + C_1 x$
which is separable, leading to:
:$y = x^3 + \dfrac {C_1 x^2} 2 + C^2$
{{qed}}
Theorem: Solution of Second Order Differential Equation with Missing Independent Variable

Let $\map g {y, \dfrac {\d y} {\d x}, \dfrac {\d^2 y} {\d x^2} } = 0$ be a second order ordinary differential equation in which the independent variable $x$ is not explicitly present.
Then $g$ can be reduced to a first order ordinary differential equation, whose solution can be determined.

Proof:
Consider the second order ordinary differential equation:
:$(1): \quad \map g {y, \dfrac {\d y} {\d x}, \dfrac {\d^2 y} {\d x^2} } = 0$
Let a new dependent variable $p$ be introduced:
:$y' = p$
Hence:
:$y' ' = \dfrac {\d p} {\d x} = \dfrac {\d p} {\d y} \dfrac {\d y} {\d x} = p \dfrac {\d p} {\d y}$
Then $(1)$ can be transformed into:
:$(2): \quad \map g {y, p, p \dfrac {\d p} {\d y} = 0}$
which is a first order ODE.
If $(2)$ has a solution which can readily be found, it will be expressible in the form:
:$(3): \quad \map g {x, p}$
which can then be expressed in the form:
:$\map g {x, \dfrac {\d y} {\d x} }$
which is likewise subject to the techniques of solution of a first order ODE.
Hence such a second order ODE is reduced to the problem of solving two first order ODEs in succession.
{{qed}}
Theorem: Linear Second Order ODE/y'' + k^2 y = 0

The second order ODE:
:$(1): \quad y' ' + k^2 y = 0$
has the general solution:
:$y = A \, \map \sin {k x + B}$
or can be expressed as:
:$y = C_1 \sin k x + C_2 \cos k x$

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
:$p \dfrac {\d p} {\d y} = -k^2 y$
where $p = \dfrac {\d y} {\d x}$.
From:
:First Order ODE: $y \rd y = k x \rd x$
this has the general solution:
:$p^2 = -k^2 y^2 + C$
or: 
:$p^2 + k^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 + k^2 y^2
      | r = k^2 \alpha^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p = \dfrac {\d y} {\d x}
      | r = \pm k \sqrt {\alpha^2 - y^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} {\sqrt {\alpha^2 - y^2} }
      | r = \int \pm k \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \arcsin \dfrac y \alpha
      | r = \pm k x + \beta
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$, Primitive of Constant
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \alpha \map \sin {\pm k x + \beta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = A \map \sin {k x + B}
      | c = 
}}
{{end-eqn}}
From Multiple of Sine plus Multiple of Cosine: Sine Form, this can be expressed as:
:$y = C_1 \sin k x + C_2 \cos k x$
{{qed}}
Theorem: Linear Second Order ODE/y'' + k^2 y = 0

The second order ODE:
:$(1): \quad y' ' + k^2 y = 0$
has the general solution:
:$y = A \, \map \sin {k x + B}$
or can be expressed as:
:$y = C_1 \sin k x + C_2 \cos k 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 + k^2 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = k i$
:$m_2 = -k i$
These are complex and unequal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 \cos k x + C_2 \sin k x$
or, by disposing the constants differently:
:$y = C_1 \sin k x + C_2 \cos k x$
{{qed}}
Theorem: Second Order ODE/y y'' + (y')^2 = 0

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

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = y p \frac {\d p} {\d y} + p^2
      | r = 0
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = y \rd p + p \rd y
      | r = 0
      | c = multiplying by $\dfrac {\d y} p$
}}
{{eqn | ll= \leadsto
      | l = p y
      | r = C
      | c = First Order ODE: $y \rd x + x \rd y = 0$
}}
{{eqn | ll= \leadsto
      | l = y \dfrac {\d y} {\d x}
      | r = C
      | c = substituting $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = 2 C x + C_2
      | c = First Order ODE: $y \dfrac {\d y} {\d x} = k$
}}
{{eqn | r = C_1 x + C_2
      | c = reassigning constant
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/x y'' = y' + (y')^3

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

Proof:
The proof proceeds by using Solution of Second Order Differential Equation with Missing Dependent Variable.
Substitute $p$ for $y'$ in $(1)$:
{{begin-eqn}}
{{eqn | l = x \dfrac {\d p} {\d x}
      | r = p + p^3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p = \frac {\d y} {\d x}
      | r = \frac x {\sqrt {C_1^2 - x^2} }
      | c = First Order ODE: $x \rd y = \paren {y + y^3} \rd x$
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = \int \frac x {\sqrt {C_1^2 - x^2} }
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -\sqrt {C_1^2 - x^2} + C_2
      | c = Primitive of $\dfrac x {\sqrt{a^2 - x^2} }$
}}
{{eqn | ll= \leadsto
      | l = x^2 + \paren {y - C_2}^2
      | r = C_1^2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Linear Second Order ODE/y'' - k^2 y = 0

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

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = p \frac {\d p} {\d y} 
      | r = k^2 y
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = p^2
      | r = k^2 y^2 + k^2 \alpha
      | c = First Order ODE: $y \rd y = k x \rd x$
}}
{{eqn | ll= \leadsto
      | l = p = \dfrac {\d y} {\d x}
      | r = \pm k \sqrt {y^2 + k^2 \alpha}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} {\sqrt {y^2 + \alpha} }
      | r = \int \pm k \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \map \ln {y + \sqrt{y^2 + \alpha} }
      | r = \pm k x + \beta
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 + k} }$
}}
{{eqn | ll= \leadsto
      | l = y + \sqrt {y^2 + \alpha}
      | r = e^{\pm k x + \beta}
      | c = 
}}
{{eqn | r = C e^{\pm k x}
      | c = where $C = e^\beta$
}}
{{eqn | ll= \leadsto
      | l = y^2 + \alpha
      | r = \paren {C e^{\pm k x} - y}^2
      | c = 
}}
{{eqn | r = C^2 e^{\pm 2 k x} - 2 C e^{\pm k x} + y^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \frac {C^2 e^{\pm 2 k x} - \alpha} {2 C e^{\pm k x} }
      | c = Quadratic Formula
}}
{{eqn | r = \frac {C e^{\pm k x} - \frac \alpha C e^{\mp k x} } 2
      | c = Quadratic Formula
}}
{{end-eqn}}
Setting $C_1 = \dfrac C 2$ and $C_2 = - \dfrac \alpha {2 C}$:
:$y = C_1 e^{\pm k x} + C_2 e^{\mp k x}$
which is the same thing as:
:$y = C_1 e^{k x} + C_2 e^{-k x}$
by allowing for the constants to be interchanged.
{{qed}}
Theorem: Linear Second Order ODE/y'' - k^2 y = 0

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

The second order ODE:
:$x^2 y' ' = 2 x y' + \paren {y'}^2$
has the general solution:
:$y = -\dfrac {x^2} 2 - C_1 x - {C_1}^2 \, \map \ln {x - C_1} + C_2$

Proof:
The proof proceeds by using Solution of Second Order Differential Equation with Missing Dependent Variable.
Substitute $p$ for $y'$:
{{begin-eqn}}
{{eqn | l = x^2 \dfrac {\d p} {\d x} 
      | r = 2 x p + p^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p = \frac {\d y}{\d x}
      | r = -\frac {x^2} {x - C_1}
      | c = Bernoulli's Equation: $x^2 \rd y = \paren {2 x y + y^2} \rd x$
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = -\int \frac {x^2} {x - C_1} \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -\frac {x^2} 2 - C_1 x - {C_1}^2 \, \map \ln {x - C_1} + C_2
      | c = Primitive of $\dfrac {x^2} {a x + b}$
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/(x^2 + 2 y') y'' + 2 x y' = 0

The second order ODE:
:$(1): \quad \paren {x^2 + 2 y'} y' ' + 2 x y' = 0$
subject to the initial conditions:
:$y = 1$ and $y' = 0$ when $x = 0$
has the particular solution:
:$y = 1$
or:
:$3 y + x^3 = 3$

Proof:
The proof proceeds by using Solution of Second Order Differential Equation with Missing Dependent Variable.
Substitute $p$ for $y'$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \paren {x^2 + 2 p} \dfrac {\d p} {\d x} + 2 x p
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 x p \rd x + \paren {x^2 + 2 p} \rd p 
      | r = 0
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = p \paren {x^2 + p}
      | r = C_1 
      | c = Bernoulli's Equation: $2 x y \rd x + \paren {x^2 + 2 y} \rd y = 0$
}}
{{end-eqn}}
Consider the initial condition:
:$y' = p = 0$ when $x = 0$
Hence putting $p = x = 0$ in $(2)$ we get:
:$0 \cdot 0^2 + 0^2 = C_1$
:$C_1 = 0$
and so $(2)$ becomes:
{{begin-eqn}}
{{eqn | l = p x^2
      | r = -p^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p \paren {x^2 - p}
      | r = 0
      | c = 
}}
{{end-eqn}}
There are two possibilities here:
{{begin-eqn}}
{{eqn | l = p
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d x}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = C_2
      | c = 
}}
{{end-eqn}}
From our initial condition:
:$y = 1$ when $x = 0$
gives us:
:$C_2 = 1$
and so the solution is obtained:
:$y = 1$
{{qed|lemma}}
The other option is:
{{begin-eqn}}
{{eqn | l = p = \dfrac {\d y} {\d x}
      | r = -x^2 
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -\int x^2 \rd x
      | c = 
}}
{{eqn | n = 3
      | r = -\frac {x^3} 3 + C_2
      | c = 
}}
{{end-eqn}}
From our initial condition:
:$y = 1$ when $x = 0$
Hence putting $x = 0$ and $y = 1$ in $(3)$ we get:
:$1 = - \dfrac {0^3} 3 = C_2$
and so $C_2 = 1$.
Thus we have:
:$y + \dfrac {x^3} 3 = 1$
or:
:$3 y + x^3 = 3$
Hence the result.
{{qed}}
Theorem: Second Order ODE/y y'' = y^2 y' + (y')^2

The second order ODE:
:$(1): \quad y y' ' = y^2 y' + \paren {y'}^2$
subject to the initial conditions:
:$y = -\dfrac 1 2$ and $y' = 1$ when $x = 0$
has the particular solution:
:$2 y - 3 = 8 y \, \map \exp {\dfrac {3 x} 2}$

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = y p \frac {\d p} {\d y}
      | r = y^2 p + p^2
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d p} {\d y} - \frac p y
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p = \dfrac {\d y} {\d x}
      | r = y \paren {y + C_1}
      | c = Linear First Order ODE: $y' - \dfrac y x = k x$
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d y} {y \paren {y + C_1} }
      | r = \int \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {C_1} \map \ln {\frac y {y + C_1} }
      | r = x + C_2
      | c = Primitive of Reciprocal of $\dfrac x {\paren {a x + b} }$
}}
{{end-eqn}}
Now to consider the initial conditions:
:$y = -\dfrac 1 2$ and $y' = 1$ when $x = 0$
After algebra:
{{begin-eqn}}
{{eqn | l = \map \ln {\frac y {y + C_1} }
      | r = C_1 x + C_2
      | c = reassigning $C_2$
}}
{{eqn | ll= \leadsto
      | l = \frac y {y + C_1}
      | r = e^{C_1 x + C_2}
      | c = 
}}
{{eqn | r = e^{C_2} e^{C_1 x}
      | c = 
}}
{{end-eqn}}
When $x = 0$ we have $y = -1/2$:
{{begin-eqn}}
{{eqn | l = \frac {-1/2} {-1/2 + C_1}
      | r = \frac 1 {1 - 2 C_1}
      | c = 
}}
{{eqn | r = e^{C_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac y {y + C_1}
      | r = \frac {e^{C_1 x} } {1 - 2 C_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y \paren {1 - 2 C_1}
      | r = \paren {y + C_1} e^{C_1 x}
      | c = 
}}
{{end-eqn}}
Differentiating to get $y'$:
:$y' \paren {1 - 2 C_1} = \paren {y + C_1} C_1 e^{C_1 x} + e^{C_1 x} y'$
Putting $y' = 1$ when $x = 0$ we get:
{{begin-eqn}}
{{eqn | l = 1 - 2 C_1
      | r = \paren {-\frac 1 2 + C_1} C_1 + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C_1
      | r = -\frac 3 2
      | c = 
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = y \paren {1 - 2 C_1}
      | r = \paren {y + C_1} e^{C_1 x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y \paren {1 - 2 \frac {-3} 2}
      | r = \paren {y - \frac 3 2} e^{\frac {-3 x} 2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 8 y
      | r = \paren {2 y - 3} e^{\frac {-3 x} 2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 y - 3
      | r = 8 y \, \map \exp {\dfrac {3 x} 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/y'' = 1 + (y')^2

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

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = p \frac {\d p} {\d y}
      | r = p^2 + 1
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = \int \frac {p \rd p} {p^2 + 1}
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \frac 1 2 \, \map \ln {p^2 + 1} + k
      | c = Primitive of $\dfrac x {x^2 + a^2}$
}}
{{eqn | ll= \leadsto
      | l = p = \frac {\d y} {\d x}
      | r = \sqrt {A_1^2 e^{2 y} - 1}
      | c = where $A_1^2 = e^{2 k}$
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \int \rd x
      | r = \int \frac {\d y} {\sqrt {A_1^2 e^{2 y} - 1} }
      | c = Solution to Separable Differential Equation
}}
{{end-eqn}}
Making the subtitution $u = A_1 e^y$:
:$\d u = A_1 e^y \rd y = u \rd y$
Thus $(2)$ transforms into:
{{begin-eqn}}
{{eqn | l = \int \rd x
      | r = \int \frac {\d u} {u \sqrt {u^2 - 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \arcsec u + A_2
      | c = Primitive of $\dfrac 1 {x \sqrt {x^2 - a^2} }$
}}
{{eqn | r = \map \arcsec {A_1 e^y} + A_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \sec {x - A_2}
      | r = A_1 e^y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\ln \sec} {x - A_2}
      | r = \ln A_1 + \ln e^y
      | c = 
}}
{{eqn | r = \ln A_1 + y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \map {\ln \sec} {x - A_2} - \ln A_1
      | c = 
}}
{{eqn | r = \map {\ln \sec} {x + C_1} + C_2
      | c = setting $C_1 = -A_2$ and $C_2 = -\ln A_1$
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/y'' = 1 + (y')^2

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

Proof:
The proof proceeds by using Solution of Second Order Differential Equation with Missing Dependent Variable.
Substitute $p$ for $y'$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \dfrac {\d p} {\d x}
      | r = p^2 + 1
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = \int \rd x
      | r = \int \frac {\d p} {p^2 + 1}
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \arctan p + A_1
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | ll= \leadsto
      | l = p = \frac {\d y} {\d x}
      | r = \map \tan {x - A_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = \int \map \tan {x - A_1} \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \map {\ln \sec} {x - A_1} + A_2
      | c = Primitive of $\tan a x$
}}
{{eqn | r = \map {\ln \sec} {x + C_1} + C_2
      | c = rearranging constants
}}
{{end-eqn}}
{{qed}}