avewright/proofwiki-math huggingface dataset:
Theorem: Solution to Simultaneous Homogeneous Linear First Order ODEs with Constant Coefficients

Consider the system of linear first order ordinary differential equations with constant coefficients:
{{begin-eqn}}
{{eqn | n = 1
      | l = \dfrac {\d y} {\d x} + a y + b z
      | r = 0
}}
{{eqn | n = 2
      | l = \dfrac {\d x} {\d z} + c y + d z
      | r = 0
}}
{{end-eqn}}
The general solution to $(1)$ and $(2)$ consists of the linear combinations of the following:
{{begin-eqn}}
{{eqn | l = y
      | r = A_1 e^{k_1 x}
}}
{{eqn | l = z
      | r = B_1 e^{k_1 x}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y
      | r = A_2 e^{k_2 x}
}}
{{eqn | l = z
      | r = B_2 e^{k_2 x}
}}
{{end-eqn}}
where $A_1 : B_1 = A_2 : B_2 = r$
where $r$ is either of the roots of the quadratic equation:
:$\paren {k + a} \paren {k + d} - b c = 0$

Proof:
We look for solutions to $(1)$ and $(2)$ of the form:
{{begin-eqn}}
{{eqn | n = 3
      | l = y
      | r = A e^{k x}
}}
{{eqn | n = 4
      | l = z
      | r = B e^{k x}
}}
{{end-eqn}}
We do of course have the Trivial Solution of Homogeneous Linear 1st Order ODE:
:$y = z = 0$
which happens when $A = B = 0$.
So let us investigate solutions where either or both of $A$ and $B$ are non-zero.
Substituting $(3)$ and $(4)$ into $(1)$ and $(2)$ and cancelling $e^{k x}$, we get::
{{begin-eqn}}
{{eqn | n = 5
      | l = \paren {k + a} A + b B
      | r = 0
}}
{{eqn | n = 6
      | l = c A + \paren {k + d} B
      | r = 0
}}
{{end-eqn}}
From $(5)$ and $(6)$ we get:
{{begin-eqn}}
{{eqn | n = 7
      | o = 
      | r = \paren {\paren {k + a} \paren {k + d} - b c} A
      | c = 
}}
{{eqn | r = \paren {\paren {k + a} \paren {k + d} - b c} B
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So $A = B = 0$ unless $k$ is a root of the quadratic equation:
:$\paren {k + a} \paren {k + d} - b c = 0$
That is:
:$(8): \quad \begin {vmatrix} k + a & b \\ c & k + d \end {vmatrix} = 0$
where the above notation denotes the determinant.
Assume $(8)$ has distinct roots $k_1$ and $k_2$.
Taking $k = k_1$ and $k = k_2$ in $(7)$, we can obtain ratios $A_1 : B_1$ and $A_2 : B_2$ such that:
{{begin-eqn}}
{{eqn | l = y
      | r = A_1 e^{k_1 x}
}}
{{eqn | l = z
      | r = B_1 e^{k_1 x}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y
      | r = A_2 e^{k_2 x}
}}
{{eqn | l = z
      | r = B_2 e^{k_2 x}
}}
{{end-eqn}}
are solutions of $(1)$ and $(2)$.
By taking arbitrary linear combinations of these, we obtain the general solution.
{{finish|Cover the case where $k_1 {{=}} k_2$. The source work is vague on this subject. Recommend this solution be reworked, preferably in conjunction with a more rigorous and thorough source work than the one used here.}}
Theorem: Trivial Solution of Homogeneous Linear 1st Order ODE

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

Proof:
We have:
:$\map {\dfrac {\d} {\d x} } 0 = 0$
from which:
:$\dfrac {\d y} {\d x} + \map Q x y = 0$
Hence the result.
{{Qed}}
Category:Linear First Order ODEs
lcnebp3texs5ohrqzvn56sr3sek9gsg
Theorem: Simultaneous Homogeneous Linear First Order ODEs/Examples/y' - 3y + 2z = 0, y' + 4y - z = 0

Consider the system of linear first order ordinary differential equations with constant coefficients:
{{begin-eqn}}
{{eqn | n = 1
      | l = \dfrac {\d y} {\d x} - 3 y + 2 z
      | r = 0
}}
{{eqn | n = 2
      | l = \dfrac {\d x} {\d z} + 4 y - z
      | r = 0
}}
{{end-eqn}}
The general solution to $(1)$ and $(2)$ consists of the linear combinations of the following:
{{begin-eqn}}
{{eqn | l = y
      | r = C_1 e^{5 x} + C_2 e^{-x}
}}
{{eqn | l = z
      | r = -C_1 e^{5 x} + 2 C_2 e^{-x}
}}
{{end-eqn}}

Proof:
Using the technique of Solution to Simultaneous Homogeneous Linear First Order ODEs with Constant Coefficients, we calculate the roots of the quadratic equation:
:$\paren {k + a} \paren {k + d} - b c = 0$
where:
{{begin-eqn}}
{{eqn | l = a
      | r = -3
}}
{{eqn | l = b
      | r = 2
}}
{{eqn | l = c
      | r = 4
}}
{{eqn | l = d
      | r = -1
}}
{{end-eqn}}
That is:
:$\paren {k - 3} \paren {k - 1} - 8 = 0$
or:
:$k^2 - 4 k - 5 = 0$
This has roots:
{{begin-eqn}}
{{eqn | l = k_1
      | r = 5
}}
{{eqn | l = k_2
      | r = -1
}}
{{end-eqn}}
We also obtain:
{{begin-eqn}}
{{eqn | l = \paren {k - 3} A  + 2 B
      | r = 0
}}
{{eqn | l = 4 A + \paren {k - 1} B
      | r = -1
}}
{{end-eqn}}
When $k = 5$ we get that $A + B = 0$.
When $k = -1$ we get that $2 A - B = 0$.
This provides us with the solutions:
{{begin-eqn}}
{{eqn | l = y
      | r = e^{5 x}
}}
{{eqn | l = z
      | r = e^{-5 x}
}}
{{end-eqn}}
or:
{{begin-eqn}}
{{eqn | l = y
      | r = e^{-x}
}}
{{eqn | l = z
      | r = 2 e^{-x}
}}
{{end-eqn}}
From these, the general solution is constructed:
{{begin-eqn}}
{{eqn | l = y
      | r = C_1 e^{5 x} + C_2 e^{-x}
}}
{{eqn | l = z
      | r = -C_1 e^{5 x} + 2 C_2 e^{-x}
}}
{{end-eqn}}
{{qed}}
Theorem: Linear First Order ODE/y' - y = x^2

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

Proof:
$(1)$ 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 = -1$
:$\map Q x = x^2$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = -\int \rd x
      | c = 
}}
{{eqn | r = -x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{-x}
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\d} {\d x} } {y e^{-x} }
      | r = x^2 e^{-x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y e^{-x}
      | r = \int x^2 e^{-x} \rd x
      | c = 
}}
{{eqn | r = \frac {e^{-x} } {-1} \paren {x^2 - \frac {2 x} {-1} + \frac 2 {\paren {-1}^2} } + C
      | c = Primitive of $x^2 e^{a x}$ for $a = -1$
}}
{{eqn | r = -e^{-x} \paren {x^2 + 2 x + 2} + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = C e^x - \paren {x^2 + 2 x + 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Linear First Order ODE/y' - y = e^x/y(0) = 0

Consider the linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} - y = e^x$
subject to the initial condition:
:$\map y 0 = 0$
$(1)$ has the particular solution:
:$y = x e^x$

Proof:
$(1)$ 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 = -1$
:$\map Q x = e^x$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = -\int \rd x
      | c = 
}}
{{eqn | r = -x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{-x}
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\d} {\d x} } {y e^{-x} }
      | r = e^x e^{-x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y e^{-x}
      | r = \int 1 \rd x
      | c = 
}}
{{eqn | r = x + C
      | c = Primitive of Constant
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = y
      | r = e^x \paren {x + C}
      | c = 
}}
{{end-eqn}}
Substituting the initial condition into $(2)$:
{{begin-eqn}}
{{eqn | l = 0
      | r = e^0 \paren {0 + C}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = C
      | c = 
}}
{{end-eqn}}
which leads to the particular solution:
:$y = x e^x$
{{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 = e^{-2 x} \paren {C_1 \cos x + C_2 \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 + 4 m + 5 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = -2 + i$
:$m_2 = -2 - i$
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = e^{-2 x} \paren {C_1 \cos x + C_2 \sin x}$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
t1gsc2so7jt7d7i7mdzi5l6doadjmv2
Theorem: Linear Second Order ODE/y'' + 4 y' + 5 y = 2 exp -2 x

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

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = 4$
:$q = 5$
:$\map R x = 2 e^{-2 x}$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' + 4 y' + 5 y = 0$
From Linear Second Order ODE: $y'' + 4 y' + 5 y = 0$, this has the general solution:
:$y_g = e^{-2 x} \paren {C_1 \cos x + C_2 \sin x}$
It remains to find a particular solution $y_p$ to $(1)$.
We have that:
:$\map R x = 2 e^{-2 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 = 2$
:$a = -2$
:$p = 4$
:$q = 5$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = \dfrac {2 e^{-2 x} } {\paren {-2}^2 + 4 \times \paren {-2} + 5}
      | c = 
}}
{{eqn | r = \dfrac {2 e^{-2 x} } {4 - 8 + 5}
      | c = 
}}
{{eqn | r = 2 e^{-2 x}
      | 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 = e^{-2 x} \paren {C_1 \cos x + C_2 \sin x + 2}$
is the general solution to $(1)$.
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = exp -x cos x

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

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = 0$
:$q = 1$
:$\map R x = e^{-x} \cos 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 \sin x + C_2 \cos x$
It remains to find a particular solution $y_p$ to $(1)$.
We have that:
:$\map R x = e^{-x} \cos x$
From the Method of Undetermined Coefficients for Exponential of Sine and Cosine:
:$y_p = e^{-x} \paren {A \cos x + B \sin x}$
where $A$ and $B$ are to be determined.
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = e^{-x} \paren {A \cos x + B \sin x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = -e^{-x} \paren {A \cos x + B \sin x} + e^{-x} \paren {-A \sin x + B \cos x}
      | c = Product Rule for Derivatives etc.
}}
{{eqn | r = e^{-x} \paren {\paren {B - A} \cos x - \paren {A + B} \sin x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}''
      | 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 = Product Rule for Derivatives etc.
}}
{{eqn | r = e^{-x} \paren {-2 B \cos x + 2 A \sin x}
      | c = 
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = e^{-x} \paren {-2 B \cos x + 2 A \sin x} + e^{-x} \paren {A \cos x + B \sin x}
      | r = e^{-x} \cos x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -2 B \cos x + A \cos x
      | r = \cos x
      | c = equating coefficients
}}
{{eqn | l = 2 A \sin x + B \sin x
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A - 2 B
      | r = 1
      | c = 
}}
{{eqn | l = 2 A + B
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 5 A
      | r = 1
      | c = 
}}
{{eqn | l = 5 B
      | r = -2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A
      | r = \dfrac 1 5
      | c = 
}}
{{eqn | l = B
      | r = -\dfrac 2 5
      | c = 
}}
{{end-eqn}}
Hence the result:
:$y_p = \dfrac {e^{-x} } 5 \paren {\cos x - 2 \sin x}$
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = \dfrac {e^{-x} } 5 \paren {\cos x - 2 \sin x} + C_1 \sin x + C_2 \cos x$
is the general solution to $(1)$.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 5 y' + 6 y = 0

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

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

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE in the form:
:$y' ' + p y' + q y = \map R x $
where:
:$p = -5$
:$q = 5$
:$\map R x = \cos x + \sin x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y' ' - 5 y' + 6 y = 0$
From Linear Second Order ODE: $y'' - 5 y' + 6 y = 0$, this has the general solution:
:$y_g = C_1 e^{2 x} + C_2 e^{3 x}$
It remains to find a particular solution $y_p$ to $(1)$.
We have that:
:$\map R x = e^{-x} \cos x$
From the Method of Undetermined Coefficients for Sine and Cosine:
:$y_p = A \cos x + B \sin x$
where $A$ and $B$ are to be determined.
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = A \cos x + B \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = -A \sin x + B \cos x
      | c = Derivative of Sine Function, Derivative of Cosine Function
}}
{{eqn | ll= \leadsto
      | l = {y_p}' '
      | r = -A \cos x - B \sin x
      | c = Derivative of Sine Function, Derivative of Cosine Function
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = \paren {-A \cos x - B \sin x} - 5 \paren {-A \sin x + B \cos x} + 6 \paren {A \cos x + B \sin x}
      | r = \cos x + \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {5 A - 5 B} \cos x
      | r = \cos x
      | c = equating coefficients
}}
{{eqn | l = \paren {5 B + 5 A} \sin x
      | r = \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 10 A
      | r = 2
      | c = 
}}
{{eqn | l = 10 B
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A
      | r = \dfrac 1 5
      | c = 
}}
{{eqn | l = B
      | r = 0
      | c = 
}}
{{end-eqn}}
Hence the result:
:$y_p = \dfrac {\cos x} 5$
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^{2 x} + C_2 e^{3 x} + \dfrac {\cos x} 5$
is the general solution to $(1)$.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 4 y = x^2 - 3 x - 4

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

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 = x^2 - 3 x - 4$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - 4 y = 0$
From Linear Second Order ODE: $y'' - 4 y = 0$, this has the general solution:
:$y_g = C_1 e^{2 x} + C_2 e^{-2 x}$
We have that:
:$\map R x = x^2 - 3 x - 4$
and so from the Method of Undetermined Coefficients for Polynomial function:
:$y_p = A_1 x^2 + A_2 x + A_3$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = A_1 x^2 + A_2 x + A_3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = 2 A_1 x + A_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}''
      | r = 2 A_1
      | c = 
}}
{{end-eqn}}
Substituting in $(1)$:
{{begin-eqn}}
{{eqn | l = \paren {2 A_1} - 4 \paren {A_1 x^2 + A_2 x + A_3}
      | r = x^2 - 3 x - 4
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 A_1 - 4 A_3
      | r = -4
      | c = equating coefficients
}}
{{eqn | l = -4 A_2
      | r = -3
      | c = 
}}
{{eqn | l = -4 A_1
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_1
      | r = -\dfrac 1 4
      | c = 
}}
{{eqn | l = A_2
      | r = \dfrac 3 4
      | c = 
}}
{{eqn | l = A_3
      | r = \dfrac 7 8
      | 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^{2 x} + C_2 e^{-2 x} - \dfrac {x^2} 4 + \dfrac {3 x} 4 + \dfrac 7 8$
{{qed}}
Theorem: Angular Momentum Commutation Rules

Let $J_x$, $J_y$ and $J_z$ denote the angular momentum operators.
Then:
{{begin-eqn}}
{{eqn | l = \sqbrk {J_x, J_y}
      | r = i J_z
}}
{{eqn | l = \sqbrk {J_y, J_z}
      | r = i J_x
}}
{{eqn | l = \sqbrk {J_z, J_x}
      | r = i J_y
}}
{{end-eqn}}
where $\sqbrk {\, \cdot, \cdot \,}$ denotes the commutator operator.

Proof:
{{ProofWanted|Got a lot to work through before we get this far}}
Theorem: P-adic Norm of P-adic Expansion is determined by First Nonzero Coefficient

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\ds \sum_{i \mathop = m}^\infty d_i p^i$ be a $p$-adic expansion.
Let $a$ be the $p$-adic number, that is left coset, in $\Q_p$ containing $\ds \sum_{i \mathop = m}^\infty d_i p^i$.
Let $l$ be the index of the first non-zero coefficient in the $p$-adic expansion:
:$l = \min \set {i: i \ge m \land d_i \ne 0}$
Then:
:$\norm a_p = p^{-l}$

Proof:
For all $n \ge m$, let:
:$\alpha_n = \ds \sum_{i \mathop = m}^n d_i p^i$
By assumption:
:$\sequence{\alpha_n}$ is a representative of $a$
By definition of the induced norm:
:$\norm a_p = \ds \lim_{n \mathop \to \infty} \norm {\alpha_n}_p$
From Eventually Constant Sequence Converges to Constant it is sufficient to show:
:$\forall n \ge l + 1 : \norm {\alpha_n}_p = p^{-l}$
Let $n \ge l + 1$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {\sum_{i \mathop = m}^n d_i p^i}_p
      | r = \norm {\paren {\sum_{i \mathop = m}^{l - 1} d_i p^i} + d_l p^l + \paren {\sum_{i \mathop = l + 1}^n d_i p^i} }_p
}}
{{eqn | r = \norm {\paren {\sum_{i \mathop = m}^{l - 1} 0 \cdot p^i } + d_l p^l + \paren {\sum_{i \mathop = l + 1}^n d_i p^i} }_p
      | c = by choice of $l$, for all $i : m \le i < l \implies d_i = 0$
}}
{{eqn | r = \norm {d_l p^l + \paren {\sum_{i \mathop = l + 1}^n d_i p^i} }_p
}}
{{eqn | r = \max \set {\norm {d_l p^l }_p, \norm {\sum_{i \mathop = l + 1}^n d_i p^i}_p}
      | o = \le
      | c = {{NormAxiomNonArch|4}}
}}
{{end-eqn}}
The sum $\ds \sum_{i \mathop = l + 1}^n d_i p^i$ can be rewritten:
:$\ds \sum_{i \mathop = l + 1}^n d_i p^i = p^{l + 1} \sum_{i \mathop = l + 1}^n d_i p^{i - \paren {l + 1} }$
By definition of divisor:
:$\ds p^{l + 1} \divides \sum_{i \mathop = l + 1}^n d_i p^i$
Then:
{{begin-eqn}}
{{eqn | l = \norm {\sum_{i \mathop = l + 1}^n d_i p^i}_p
      | o = \le
      | r = p^{-\paren {l + 1} }
      | c = {{Defof|P-adic Norm|$p$-adic norm}}
}}
{{eqn | o = <
      | r = p^{-l}
      | c = Power Function on Base between Zero and One is Strictly Decreasing
}}
{{end-eqn}}
By definition of a $p$-adic expansion:
:$0 < d_l < p$
Then:
:$p^l \divides d_l p^l$
:$p^{l + 1} \nmid d_l p^l$
By definition of $p$-adic norm:
:$\norm {d_l p^l}_p = p^{-l}$
Thus:
:$\ds \norm {\sum_{i \mathop = l + 1}^n d_i p^i}_p < p^{-l} = \norm {d_l p^l}_p$
Finally:
{{begin-eqn}}
{{eqn | l = \norm {\sum_{i \mathop = m}^n d_i p^i}_p
      | r = \max \set {\norm {d_l p^l}_p, \norm {\sum_{i \mathop = l + 1}^n d_i p^i}_p}
      | c = {{Corollary|Three Points in Ultrametric Space have Two Equal Distances|2}}
}}
{{eqn | r = \norm {d_l p^l}_p
      | c = as $\ds \norm {\sum_{i \mathop = l + 1}^n d_i p^i}_p < \norm {d_l p^l}_p$
}}
{{eqn | r = p^{-l}
      | c = derived earlier
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Eventually Constant Sequence Converges to Constant

:$\ds \lim_{n \mathop \to \infty} x_n = \lambda$

Proof:
Let $\sequence {y_n}$ be the subsequence of $\sequence {\norm {x_n} }$ defined as:
:$\forall n: y_n = x_{N + n}$
The $\sequence {y_n}$ is the constant sequence $\tuple {\lambda, \lambda, \lambda, \dotsc}$.
Then:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} x_n
      | r = \lim_{n \mathop \to \infty} y_n
      | c = Limit of Subsequence equals Limit of Sequence in Normed Division Ring
}}
{{eqn | r = \lambda
      | c = Constant Sequence Converges to Constant in Normed Division Ring
}}
{{end-eqn}}
{{qed}}
Category:Sequences
Category:Normed Division Rings
sfgimgpr1ikfb67ki242hsqe2nn6raq
Theorem: Non-Zero Complex Numbers under Multiplication form Group

Let $\C_{\ne 0}$ be the set of complex numbers without zero, that is:
:$\C_{\ne 0} = \C \setminus \set 0$
The structure $\struct {\C_{\ne 0}, \times}$ is a group.

Proof:
Taking the group axioms in turn:
Theorem: Real Numbers under Addition form Group

Let $\R$ be the set of real numbers.
The structure $\struct {\R, +}$ is a group.

Proof:
Taking the group axioms in turn:
Theorem: Complex Numbers under Addition form Group

Let $\C$ be the set of complex numbers.
The structure $\struct {\C, +}$ is a group.

Proof:
Taking the group axioms in turn:
Theorem: Unitary Group is Group

The set of unitary $n \times n$ matrices forms a group under (conventional) matrix multiplication.

Proof:
Let $\mathbf A$ and $\mathbf B$ be $n \times n$ unitary matrices.
Theorem: General Linear Group is not Abelian

Let $K$ be a field whose zero is $0_K$ and unity is $1_K$.
Let $\GL {n, K}$ be the general linear group of order $n$ over $K$.
Then $\GL {n, K}$ is not an abelian group.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = A
      | r = \begin {pmatrix} 1 & 1 \\ 0 & 1 \end {pmatrix}
}}
{{eqn | l = B
      | r = \begin {pmatrix} 1 & 1 \\ 1 & 1 \end {pmatrix}
}}
{{end-eqn}}
Both $A$ and $B$ are elements of the general linear group.
Then:
{{begin-eqn}}
{{eqn | l = A B
      | r = \begin {pmatrix} 1 & 1 \\ 0 & 1 \end {pmatrix} \begin {pmatrix} 1 & 1 \\ 1 & 1 \end {pmatrix}
      | c = 
}}
{{eqn | r = \begin {pmatrix} 2 & 2 \\ 1 & 1 \end {pmatrix}
      | c = 
}}
{{eqn | l = B A
      | r = \begin {pmatrix} 1 & 1 \\ 1 & 1 \end {pmatrix} \begin {pmatrix} 1 & 1 \\ 0 & 1 \end {pmatrix}
      | c = 
}}
{{eqn | r = \begin {pmatrix} 2 & 1 \\ 2 & 1 \end {pmatrix}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AB
      | o = \ne
      | r = BA
      | c = 
}}
{{end-eqn}}
and it follows by definition that the general linear group is not abelian.
{{qed}}
Theorem: Group of Unitary Matrices under Multiplication is not Abelian

Let $n > 1$ be a natural number.
Let $\map U n$ denote the unitary group.
Then $\map U n$ is not abelian.

Proof:
;Proof by Counterexample
{{Recall|Unitary Group}}
{{:Definition:Unitary Group}}
The matrices:
:$A = \begin {pmatrix} 1 & 0 \\ 0 & -1 \end {pmatrix}$
and
:$B = \begin {pmatrix} 0 & 1 \\ 1 & 0 \end {pmatrix}$
are both real and symmetric.
Hence, by Real Symmetric Matrix is Hermitian, both are Hermitian.
Furthermore, both are their own inverse.
Hence they satisfy the definition of a unitary matrix.
However:
:$AB = \begin {pmatrix} 0 & 1 \\ -1 & 0\end {pmatrix}$
and 
:$BA = \begin {pmatrix} 0 & -1 \\ 1 & 0 \end {pmatrix}$
Hence their product is not commutative.
Hence, by definition, $\map U n$ is not an abelian group.
{{qed}}
Theorem: Complex Numbers form Vector Space over Themselves

The set of complex numbers $\C$, with the operations of addition and multiplication, forms a vector space.

Proof:
Let the field of complex numbers be denoted $\struct {\C, +, \times}$.
By Complex Numbers under Addition form Infinite Abelian Group, $\struct {\C, +}$ is an abelian group.
From Complex Multiplication Distributes over Addition:
{{begin-eqn}}
{{eqn | q = \forall x, y, z \in \C
      | l = x \times \paren {y + z}
      | r = x \times y + x \times z
}}
{{eqn | l = \paren {y + z} \times x
      | r = y \times x + z \times x
}}
{{end-eqn}}
From Complex Multiplication is Associative:
:$\forall x, y, z \in \C: x \times \paren {y \times z} = \paren {x \times y} \times z$
From Complex Multiplication Identity is One:
:$\forall x \in \C: 1 \times x = x$
Therefore $\struct {\C, +, \times}$ forms a vector space.
{{qed}}