avewright/proofwiki-math huggingface dataset:
Theorem: Characterization of Closure by Basis

Let $T = \struct {S, \tau}$ be a topological space.
Let $\BB \subseteq \tau$ be a basis.
Let $A$ be a subset of $S$.
Let $x$ be a point of $S$.
Then $x \in A^-$ {{iff}}:
:$\forall U \in \BB: x \in U \implies A \cap U \ne \O$
where:
:$A^-$ denotes the closure of $A$

Proof:
=== Sufficient Condition ===
Let $x \in A^-$.
Let $U \in \BB$.
By definition of basis, $U$ is an open set of $T$.
Thus from Condition for Point being in Closure:
:if $x \in U$ then $A \cap U \ne \O$.
{{qed|lemma}}
Theorem: Sorgenfrey Line is Separable

The Sorgenfrey line is separable.

Proof:
{{Recall|Separable Space|separable space}}
{{:Definition:Separable Space}}
By Rationals are Everywhere Dense in Sorgenfrey Line:
:$\Q$ is dense in the Sorgenfrey line.
By Rational Numbers are Countably Infinite:
:$\Q$ is countable.
Thus by definition:
:The Sorgenfrey line is separable.
{{qed}}
Theorem: First Order ODE/y dx + x dy = 0

The first order ODE:
:$(1): \quad y \rd x + x \rd y = 0$
has the general solution:
:$x y = C$

Proof:
$(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = x \rd y
      | r = -y \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = C x^{-1}
      | c = First Order ODE: $x \rd y = k y \rd x$
}}
{{eqn | ll= \leadsto
      | l = x y
      | r = C
      | c = multiplying through by $x$
}}
{{end-eqn}}
{{qed}}
Category:Examples of First Order ODEs
Category:Examples of Solutions to Separable Differential Equation
58mu603fe3lwqbla62j9ua366vdh3m7
Theorem: First Order ODE/y dy = k dx

Let $k \in \R$ be a real number.
The first order ODE:
:$y \, \dfrac {\d y} {\d x} = k$
has the general solution:
:$y^2 = 2 k x + C$

Proof:
{{begin-eqn}}
{{eqn | l = y \, \dfrac {\d y} {\d x}
      | r = k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int y \rd y
      | r = \int k \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \frac {y^2} 2
      | r = k x + \frac C 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = 2 k x + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of First Order ODEs
Category:Examples of Solutions to Separable Differential Equation
gglxc275lfbocl5dsh6u19v00ooo33w
Theorem: First Order ODE/x dy = (y + y^3) dx

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

Proof:
{{begin-eqn}}
{{eqn | l = x \dfrac {\d y} {\d x}
      | r = y + y^3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d y} {y \paren {1 + y^2} }
      | r = \int \frac {\d x} x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \frac 1 2 \, \map \ln {\frac {y^2} {y^2 + 1} }
      | r = \ln x + \ln k
      | c = Primitive of $\dfrac 1 {x \paren {x^2 + a^2} }$
}}
{{eqn | r = \map \ln {k x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\frac {y^2} {y^2 + 1} }
      | r = \map \ln {k^2 x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {y^2} {y^2 + 1} 
      | r = k^2 x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {y^2 + 1} {y^2}
      | r = \frac 1 {k^2 x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1 + \frac 1 {y^2}
      | r = \frac 1 {k^2 x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {y^2}
      | r = \frac 1 {k^2 x^2} - 1
      | c = 
}}
{{eqn | r = \frac {1 - k^2 x^2} {k^2 x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = \frac {k^2 x^2} {1 - k^2 x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = \frac {x^2} {\frac 1 {k^2} - x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = \frac {x^2} {C^2 - x^2}
      | c = letting $C = \dfrac 1 k$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \frac x {\sqrt {C^2 - x^2} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of First Order ODEs
Category:Examples of Solutions to Separable Differential Equation
r65x7wiov98oxpkh8xygqcmtqcm2ssl
Theorem: First Order ODE/y dy = k x dx

Let $k \in \R$ be a real number.
The first order ODE:
:$y \rd y = k x \rd x$
has the general solution:
:$y^2 = k x^2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = y \rd y
      | r = k x \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int y \rd y
      | r = \int k x \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \frac {y^2} 2
      | r = \frac {k x^2} 2 + C_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = k x^2 + C
      | c = reassigning the arbitrary constant.
}}
{{end-eqn}}
{{qed}}
Category:Examples of First Order ODEs
Category:Examples of Solutions to Separable Differential Equation
tovmctl0axqju5cggh3ter02kmpoixy
Theorem: Primitive of Reciprocal of Root of x squared plus k

Let $k \in \R$.
Then:
:$\ds \int \frac {\d x} {\sqrt {\size {x^2 + k} } } = \map \ln {x + \sqrt {\size {x^2 + k} } } + C$

Proof:
There are three cases:
:$0 \le k$
:$-x^2 < k < 0$
:$k < -x^2$
Theorem: Bernoulli's Equation/x^2 dy = (2 x y + y^2) dx

The first order ODE:
:$(1): \quad x^2 \rd y = \paren {2 x y + y^2} \rd x$
has the general solution:
:$y = -\dfrac {x^2} {x + C}$

Proof:
Rearranging $(1)$:
:$(2): \quad \dfrac {\d y} {\d x} - \dfrac 2 x y = \dfrac {y^2} {x^2}$
It can be seen that $(2)$ is in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x y^n$
where:
:$\map P x = -\dfrac 2 x$
:$\map Q x = \dfrac 1 {x^2}$
:$n = 2$
and so is an example of Bernoulli's equation.
By Solution to Bernoulli's Equation it has the general solution:
:$(3): \quad \ds \frac {\map \mu x} {y^{n - 1} } = \paren {1 - n} \int \map Q x \map \mu x \rd x + C$
where:
:$\map \mu x = e^{\paren {1 - n} \int \map P x \rd x}$
Thus $\map \mu x$ is evaluated:
{{begin-eqn}}
{{eqn | l = \paren {1 - n} \int \map P x \rd x
      | r = \paren {1 - 2} \int -\dfrac 2 x \rd x
      | c = 
}}
{{eqn | r = 2 \ln x
      | c = 
}}
{{eqn | r = \ln x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \mu x
      | r = e^{\ln x^2}
      | c = 
}}
{{eqn | r = x^2
      | c = 
}}
{{end-eqn}}
and so substituting into $(3)$:
{{begin-eqn}}
{{eqn | l = x^2 \frac 1 y
      | r = \paren {1 - 2} \int \dfrac 1 {x^2} x^2 \rd x
      | c = 
}}
{{eqn | r = -\int \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {x^2} y
      | r = -x + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -\frac {x^2} {x + C}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of Bernoulli's Equation
gkrqtd3n8ftbpaeshh4n2klc01n7op9
Theorem: Bernoulli's Equation/2 x y dx + (x^2 + 2 y) dy = 0

The first order ODE:
:$(1): \quad 2 x y \rd x + \paren {x^2 + 2 y} \rd y = 0$
has the solution:
:$y \paren {x^2 + y} = C$

Proof:
{{begin-eqn}}
{{eqn | l = 2 x y \rd x + \paren {x^2 + 2 y} \rd y
      | r = 0
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \dfrac {\d x} {\d y} + \frac 1 {2 y} x
      | r = -\frac 1 x
      | c = 
}}
{{end-eqn}}
It can be seen that $(2)$ is in the form:
:$\dfrac {\d x} {\d y} + \map P y x = \map Q y x^n$
where:
:$\map P y = \dfrac 1 {2 y}$
:$\map Q y = -1$
:$n = -1$
and so is an example of Bernoulli's equation.
By Solution to Bernoulli's Equation it has the general solution:
:$(3): \quad \ds \frac {\map \mu y} {x^{n - 1} } = \paren {1 - n} \int \map Q y \, \map \mu y \rd y + C$
where:
:$\map \mu y = e^{\paren {1 - n} \int \map P y \rd y}$
Thus $\map \mu x$ is evaluated:
{{begin-eqn}}
{{eqn | l = \paren {1 - n} \int \map P y \rd y
      | r = \paren {1 - \paren {-1} } \int \dfrac 1 {2 y} \rd y
      | c = 
}}
{{eqn | r = 2 \frac 1 2 \ln y
      | c = 
}}
{{eqn | r = \ln y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \mu y
      | r = e^{\ln y}
      | c = 
}}
{{eqn | r = y
      | c = 
}}
{{end-eqn}}
and so substituting into $(3)$:
{{begin-eqn}}
{{eqn | l = \frac y {x^{\paren {-1} - 1} }
      | r = \paren {1 - \paren {-1} } \int \paren {-1} y \rd y
      | c = 
}}
{{eqn | r = -2 \int y \rd y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y x^2
      | r = -2 \frac {y^2} 2 + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y \paren {x^2 + y}
      | r = C
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of Bernoulli's Equation
oj7viqrbzht917ri3n1u9zsh5u8kytb
Theorem: Linear First Order ODE/y' - (y over x) = k x

Let $k \in \R$ be a real number.
The linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} - \dfrac y x = k x$
has the general solution:
:$\dfrac y x = k x + C$
or:
:$y = k x^2 + C x$

Proof:
$(1)$ is in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x$
where $\map P x = -\dfrac 1 x$.
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = \int -\frac 1 x \rd x
      | c = 
}}
{{eqn | r = -\ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{-\ln x}
      | c = 
}}
{{eqn | r = \frac 1 x
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
:$\map {\dfrac {\d} {\d x} } {\dfrac y x} = \dfrac 1 x k x = k$
and the general solution is:
:$\dfrac y x = k x + C$
or:
:$y = k x^2 + C x$
{{qed}}
Category:Examples of Linear First Order ODEs
3o817zfo2s8hr8k4lgxmmx3qu324k92
Theorem: First Order ODE/x dy = k y dx

The first order ODE:
:$(1): \quad x \rd y = k y \rd x$
has the general solution:
:$y = C x^k$

Proof:
$(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = x \rd y
      | r = k y \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} y
      | r = k \int \dfrac {\d x} x
      | c = Solutions to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \ln y
      | r = k \ln x + \ln C
      | c = 
}}
{{eqn | r = \map \ln {C x^k}
      | c = 
}}
{{eqn | l = y
      | r = C x^k
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of First Order ODEs
Category:Examples of Solutions to Separable Differential Equation
Category:First Order ODE/x dy = k y dx
r7a5sj85fe7uyd4amr7uhekbat3684w
Theorem: First Order ODE/dy = k y dx

Let $k \in \R$ be a real number.
The first order ODE:
:$\dfrac {\d y} {\d x} = k y$
has the general solution:
:$y = C e^{k x}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x}
      | r = k y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} y
      | r = \int k \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \ln y
      | r = k x + C'
      | c = Primitive of Reciprocal, Primitive of Constant
}}
{{eqn | ll= \leadsto
      | l = y
      | r = e^{k x + C'}
      | c = 
}}
{{eqn | r = e^{k x} e^{C'}
      | c = 
}}
{{eqn | r = C e^{k x}
      | c = putting $C = e^{C'}$
}}
{{end-eqn}}
{{qed}}
Theorem: First Order ODE/dy = k y dx

Let $k \in \R$ be a real number.
The first order ODE:
:$\dfrac {\d y} {\d x} = k y$
has the general solution:
:$y = C e^{k x}$

Proof:
Write the differential equation as: 
:$y' - k y = 0$
Taking Laplace transforms:
:$\laptrans {y' - k y} = \laptrans 0$
From Laplace Transform of Constant Mapping, we have: 
:$\laptrans 0 = 0$
We also have: 
{{begin-eqn}}
{{eqn	| l = \laptrans {y' - k y}
	| r = \laptrans {y'} - k \laptrans y
	| c = Linear Combination of Laplace Transforms
}}
{{eqn	| r = s \laptrans y - \map y 0 - k \laptrans y
	| c = Laplace Transform of Derivative
}}
{{end-eqn}}
So:
:$\paren {s - k} \laptrans y = \map y 0$
Giving: 
:$\laptrans y = \dfrac {\map y 0} {s - k}$
So:
{{begin-eqn}}
{{eqn	| l = y
	| r = \invlaptrans {\frac {\map y 0} {s - k} }
	| c = {{Defof|Inverse Laplace Transform}}
}}
{{eqn	| r = \map y 0 \invlaptrans {\laptrans {e^{k x} } } 
	| c = Linear Combination of Laplace Transforms, Laplace Transform of Exponential
}}
{{eqn	| r = \map y 0 e^{k x}
	| c = {{Defof|Inverse Laplace Transform}}
}}
{{end-eqn}}
Setting $C = \map y 0$ gives the result.
{{qed}}
Theorem: First Order ODE/dy = k y dx

Let $k \in \R$ be a real number.
The first order ODE:
:$\dfrac {\d y} {\d x} = k y$
has the general solution:
:$y = C e^{k x}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x}
      | r = k y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d x} - k y
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{-k x} \paren {\dfrac {\d y} {\d x} - k y}
      | r = 0
      | c = Solution to Linear First Order Ordinary Differential Equation: $e^{\int -k \rd x} = e^{-k x}$
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {y e^{-k x} }
      | r = 0
      | c = Solution to Linear First Order Ordinary Differential Equation continued
}}
{{eqn | ll= \leadsto
      | l = y e^{-k x}
      | r = C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = C e^{k x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: First Order ODE/(1 over x^3 y^2 + 1 over x) dx + (1 over x^2 y^3 - 1 over y) dy = 0

The first order ordinary differential equation:
:$(1): \quad \paren {\dfrac 1 {x^3 y^2} + \dfrac 1 x} \rd x + \paren {\dfrac 1 {x^2 y^3} - \dfrac 1 y} \rd y = 0$
is an exact differential equation with solution:
:$-\dfrac 1 {2 x^2 y^2} = \ln \dfrac y x + C$

Proof:
Let:
:$\map M {x, y} = \dfrac 1 {x^3 y^2} + \dfrac 1 x$
:$\map N {x, y} = \dfrac 1 {x^2 y^3} - \dfrac 1 y$
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial M} {\partial y}
      | r = -\dfrac 2 {x^3 y^3}
      | c = 
}}
{{eqn | l = \dfrac {\partial N} {\partial x}
      | r = -\dfrac 2 {x^3 y^3}
      | c = 
}}
{{end-eqn}}
Thus $\dfrac {\partial M} {\partial y} = \dfrac {\partial N} {\partial x}$ and $(1)$ is seen by definition to be exact.
By Solution to Exact Differential Equation, the solution to $(1)$ is:
:$\map f {x, y} = C$
where:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial f} {\partial x}
      | r = \map M {x, y}
      | c = 
}}
{{eqn | l = \dfrac {\partial f} {\partial y}
      | r = \map N {x, y}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = f
      | r = \map M {x, y} \rd x + \map g y
      | c = 
}}
{{eqn | r = \int \paren {\dfrac 1 {x^3 y^2} + \dfrac 1 x} \rd x + \map g y
      | c = 
}}
{{eqn | r = -\frac 1 {2 x^2 y^2} + \ln x + \map g y
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = f
      | r = \int \map N {x, y} \rd y + \map h x
      | c = 
}}
{{eqn | r = \int \paren {\dfrac 1 {x^2 y^3} - \dfrac 1 y} \rd y + \map h x
      | c = 
}}
{{eqn | r = -\frac 1 {2 x^2 y^2} - \ln y + \map h x
      | c = 
}}
{{end-eqn}}
Thus:
:$\map f {x, y} = -\dfrac 1 {2 x^2 y^2} + \ln x - \ln y$
and by Solution to Exact Differential Equation, the solution to $(1)$ is:
:$-\dfrac 1 {2 x^2 y^2} + \ln x - \ln y = C$
or:
:$-\dfrac 1 {2 x^2 y^2} = \ln \dfrac y x + C$
{{qed}}
Category:Examples of Exact Differential Equation
Category:Examples of First Order ODEs
elj3pqu434rv543uhq03hq1pfoewrfd
Theorem: Linear First Order ODE/y' + (y over x) = k x^n

Let $k, n \in \R$ be real numbers.
The linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} + \dfrac y x = k x^n$
has the general solution:
:<nowiki>$y = \begin{cases}
\dfrac {k x^{n + 1} } {n + 2} + \dfrac C x & : n \ne -2 \\
& \\
\dfrac {k \ln x} x + \dfrac C x & : n = -2
\end{cases}$</nowiki>

Proof:
$(1)$ is in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x$
where:
:$\map P x = \dfrac 1 x$
:$\map Q x = k x^n$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = \int \frac 1 x \rd x
      | c = 
}}
{{eqn | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{\ln x}
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
:$\map {\dfrac \d {\d x} } {x y} = k x^{n + 1}$
When $n + 1 \ne -1$, Primitive of Power is used to obtain:
:$x y = \dfrac {k x^{n + 2} } {n + 2} + C$
or:
:$y = \dfrac {k x^{n + 1} } {n + 2} + \dfrac C x$
When $n + 1 = -1$, we have:
:$\map {\dfrac \d {\d x} } {x y} = \dfrac k x$
and Primitive of Reciprocal is used, yielding:
:$x y = k \ln x + C$
or:
:$y = \dfrac {k \ln x} x + \dfrac C x$
{{qed}}
Category:Examples of Linear First Order ODEs
7ohw8zl7vtf17ehlmodoa94f844d5uy
Theorem: Linear First Order ODE/(x^2 + y) dx = x dy

The linear first order ODE:
:$(1): \quad \paren {x^2 + y} \rd x = x \rd y$
has the general solution:
:$y = x^2 + C x$

Proof:
Rearranging $(1)$:
:$(2): \quad \dfrac {\d y} {\d x} - \dfrac y x = x$
$(2)$ is in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x$
where:
:$\map P x = -\dfrac 1 x$
:$\map Q x = x$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = \int -\dfrac 1 x \rd x
      | c = 
}}
{{eqn | r = -\ln x
      | c = 
}}
{{eqn | r = \map \ln {\frac 1 x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = \frac 1 x
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
:$\map {\dfrac \d {\d x} } {\dfrac y x} = 1$
and the general solution is:
:$\dfrac y x = x + C$
or:
:$y = x^2 + C x$
{{qed}}
Theorem: Linear First Order ODE/x y' + y = x^2 cosine x

The linear first order ODE:
:$x \, \dfrac {\d y} {\d x} + y = x^2 \cos x$
has the general solution:
:$y = 2 \cos x + x \sin x - \dfrac 2 x \sin x + \dfrac C x$

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

The linear first order ODE:
:$x \, \dfrac {\d y} {\d x} + y = x^2 \cos x$
has the general solution:
:$y = 2 \cos x + x \sin x - \dfrac 2 x \sin x + \dfrac C x$

Proof:
{{begin-eqn}}
{{eqn | l = x \dfrac {\d y} {\d x} + y
      | r = x^2 \cos x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \rd y + y \rd x
      | r = x^2 \cos x \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \d {x y}
      | r = x^2 \cos x \rd x
      | c = Product Rule for Differentials
}}
{{eqn | ll= \leadsto
      | l = x y
      | r = \int x^2 \cos x \rd x
      | c = 
}}
{{eqn | r = 2 x \cos x + \paren {x^2 - 2} \sin x + C
      | c = Primitive of $x^2 \cos a x$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = 2 \cos x + x \sin x - \frac 2 x \sin x + \frac C x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Linear First Order ODE/x y' + y = x^2 cosine x

The linear first order ODE:
:$x \, \dfrac {\d y} {\d x} + y = x^2 \cos x$
has the general solution:
:$y = 2 \cos x + x \sin x - \dfrac 2 x \sin x + \dfrac C x$

Proof:
{{begin-eqn}}
{{eqn | l = x \dfrac {\d y} {\d x} + y
      | r = x^2 \cos x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x y
      | r = \int x^2 \cos x \d x + C
      | c = Linear First Order ODE: $x y' + y = \map f x$
}}
{{eqn | r = 2 x \cos x + \paren {x^2 - 2} \sin x + C
      | c = Primitive of $x^2 \cos a x$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = 2 \cos x + x \sin x - \frac 2 x \sin x + \frac C x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: First Order ODE/(6x + 4y + 3) dx + (3x + 2y + 2) dy = 0

The first order ODE:
:$(1): \quad \paren {6 x + 4 y + 3} \rd x + \paren {3 x + 2 y + 2} \rd y = 0$
has the general solution:
:$3 x + 2 y + \map \ln {\paren {3 x + 2 y}^2} + x = C$

Proof:
We put $(1)$ in the form:
:$\dfrac {\d y} {\d x} = -\dfrac {6 x + 4 y + 3} {3 x + 2 y + 2}$
Substitute $z = 3 x + 2 y$, which gives:
:$\dfrac {\d z} {\d x} = 3 + 2 \dfrac {\d y} {\d x}$
and so:
:$\dfrac {\d z} {\d x} = -2 \dfrac {2 z + 3} {z + 2} + 3$
which simplifies down to:
:$\dfrac {\d z} {\d x} = \dfrac {-z} {z + 2}$
This is separable:
:$\ds -\int \frac {z + 2} z \rd z = \int \rd x$
which gives:
:$- z - 2 \ln z = x + C$
which, after the substitutions, gives:
:$3 x + 2 y + \map \ln {\paren {3 x + 2 y}^2} + x = C$
{{qed}}
Theorem: First Order ODE/Cosine (x + y) dx = sine (x + y) dx + x sine (x + y) dy

The first order ordinary differential equation:
:$\map \cos {x + y} \rd x = \map \sin {x + y} \rd x + x \map \sin {x + y} \rd y$
is an exact differential equation with solution:
:$x \map \cos {x + y} = C$

Proof:
Express it in the form:
:$\paren {x \map \sin {x + y} - \map \cos {x + y} } \rd x + x \map \sin {x + y} \rd y$
Let:
:$\map M {x, y} = x \map \sin {x + y} - \map \cos {x + y}$
:$\map N {x, y} = x \map \sin {x + y}$
Then:
{{begin-eqn}}
{{eqn | l = \frac {\partial M} {\partial y}
      | r = x \map \cos {x + y} + \map \sin {x + y}
      | c = 
}}
{{eqn | l = \frac {\partial N} {\partial x}
      | r = x \map \cos {x + y} + \map \sin {x + y}
      | c = 
}}
{{end-eqn}}
Thus $\dfrac {\partial M} {\partial y} = \dfrac {\partial N} {\partial x}$ and $(1)$ is seen by definition to be exact.
By Solution to Exact Differential Equation, the solution to $(1)$ is:
:$\map f {x, y} = C$
where:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial f} {\partial x}
      | r = \map M {x, y}
      | c = 
}}
{{eqn | l = \dfrac {\partial f} {\partial y}
      | r = \map N {x, y}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = f
      | r = \map M {x, y} \rd x + \map g y
      | c = 
}}
{{eqn | r = \int \paren {x \map \sin {x + y} - \map \cos {x + y} } \rd x + \map g y
      | c = 
}}
{{eqn | r = \map \sin {x + y} - x \map \cos {x + y} - \map \sin {x + y}
      | c = 
}}
{{eqn | r = -x \map \cos {x + y}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = f
      | r = \map N {x, y} \rd y + \map h x
      | c = 
}}
{{eqn | r = \int x \map \sin {x + y} \rd y + \map h x
      | c = 
}}
{{eqn | r = -x \map \cos {x + y} + \map h x
      | c = 
}}
{{end-eqn}}
Thus:
:$\map f {x, y} = -x \map \cos {x + y}$
and by Solution to Exact Differential Equation, the solution to $(1)$ is:
:$-x \map \cos {x + y} = C_1$
or setting $C = -C_1$:
:$x \map \cos {x + y} = C$
{{qed}}
Theorem: Linear First Order ODE/x y' + y = f (x)

The linear first order ODE:
:$(1): \quad x \, \dfrac {\d y} {\d x} + y = \map f x$
has the general solution:
:$\ds x y = \int \map f x \rd x + C$

Proof:
{{begin-eqn}}
{{eqn | l = x \dfrac {\d y} {\d x} + y
      | r = \map f x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \rd y + y \rd x
      | r = \map f x \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \d {x y}
      | r = \map f x \rd x
      | c = Product Rule for Differentials
}}
{{eqn | ll= \leadsto
      | l = x y
      | r = \int \map f x \rd x + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/x^2 y'' + x y' = 1

The second order ODE:
:$x^2 y' ' + x y' = 1$
has the general solution:
:$y = \dfrac {\paren {\ln x}^2} 2 + C_1 \ln x + 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} + x p
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \dfrac {\d p} {\d x} + p
      | r = \frac 1 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x p
      | r = \int \frac {\d x} x
      | c = Linear First Order ODE: $x y' + y = \map f x$
}}
{{eqn | r = \ln x + C_1
      | c = Primitive of Reciprocal
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d x}
      | r = \frac {\ln x} x + \frac {C_1} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \int \paren {\frac {\ln x} x + \frac {C_1} x} \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \frac {\paren {\ln x}^2} 2 + C_1 \ln x + C_2
      | c = Primitive of $\dfrac {\ln x} x$
}}
{{end-eqn}}
{{qed}}