avewright/proofwiki-math huggingface dataset:
Theorem: Open Set Characterization of Denseness/Analytic Basis

Let $\BB \subseteq \tau$ be an analytic basis for $\tau$.
Then $S$ is (everywhere) dense in $X$ {{iff}} every non-empty open set of $\BB$ contains an element of $S$.

Proof:
=== Necessary Condition ===
Let $S$ be everywhere dense in $X$.
By Open Set Characterization of Denseness then every non-empty open set contains an element of $S$.
Every non-empty set of an analytic basis is an open set by definition.
Hence every non-empty set of non-empty open set of $\BB$ contains an element of $S$.
{{qed|lemma}}
Theorem: Open Set Characterization of Denseness/Open Ball

Let $\struct {X, d}$ be a metric space.
Let $\tau_d$ be the topology induced by the metric $d$.
Let $S \subseteq X$.
Then $S$ is (everywhere) dense in $\struct {X, \tau_d}$ {{iff}} every open ball contains an element of $S$.

Proof:
By Open Balls form Basis for Open Sets of Metric Space, the set of open balls are an analytic basis for the topology $\tau_d$.
By Analytic Basis Characterization of Denseness then:
:$S$ is (everywhere) dense in $\struct {X, \tau_d}$ {{iff}} every open ball contains an element of $S$.
{{qed}}
Category:Denseness
chjswen0pfkgw7ie029sis7p3osz2bq
Theorem: P-adic Valuation Extends to P-adic Numbers

Let $p$ be a prime number.
Let $\nu_p^\Q: \Q \to \Z \cup \set {+\infty}$ be the $p$-adic valuation on the set of  rational numbers.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\nu_p: \Q_p \to \Z \cup \set {+\infty}$ be defined by:
:<nowiki>$\forall x \in \Q_p : \map {\nu_p} x = \begin {cases}
-\log_p \norm x_p : x \ne 0 \\
+\infty : x = 0
\end{cases}$</nowiki>
Then $\nu_p: \Q_p \to \Z \cup \set {+\infty}$ is a valuation that extends $\nu_p^\Q$ from $\Q$ to $\Q_p$.

Proof:
It needs to be shown that $\nu_p$:
:$(1): \quad \nu_p$ is a mapping into $\Z \cup \set {+\infty}$
:$(2): \quad \nu_p$ satisfies the valuation axioms $\text V 1$, $\text V 2$ and $\text V 3$
:$(3): \quad \nu_p$ extends $\nu_p^\Q$.
Let $x, y \in \Q_p$.
Theorem: P-adic Integers is Metric Completion of Integers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $d$ be the subspace metric of the $p$-adic metric on the $p$-adic integers $\Z_p$.
Then $\struct {\Z_p, d}$ is the metric completion of the integers $\Z$.

Proof:
The integers $\Z$ are a subring of the $p$-adic integers $Z_p$ by Integers form Subring of P-adic Integers.
Hence $\Z \subseteq \Z_p$.
The set of $p$-adic integers $\Z_p$ is closed in the $p$-adic metric by Set of P-adic Integers is Clopen in P-adic Numbers.
By Closure of Subset of Closed Set of Metric Space is Subset then the closure of $\Z$ is contained in $\Z_p$:
:$\map \cl \Z \subseteq \Z_p$
By P-adic Integer is Limit of Unique Coherent Sequence of Integers then:
:for all $x \in \Z_p$ there exists a sequence $\sequence {x_n}$ in $\Z$ such that $\ds \lim_{n \mathop \to \infty} x_n = x$
By Closure of Subset of Metric Space by Convergent Sequence then:
:$\Z_p \subseteq \map \cl \Z$ 
Hence $\map \cl \Z = \Z_p$.
By Metric Subspace Induces Subspace Topology then the topology induced by $d$ on $\Z_p$ is the subspace topology.
By Closure of Subset in Subspace then $\map \cl \Z = \Z_p$ in the subspace metric $d$ on $\Z_p$.
It follows that $\struct {\Z_p, d}$ is the metric completion of $\Z$.
{{qed}}
Theorem: P-adic Metric on P-adic Numbers is Non-Archimedean Metric

Let $p \in \N$ be a prime.
Let $\norm{\,\cdot\,}_p: \Q_p \to \R_{\ge 0}$ be the $p$-adic norm on the $p$-adic numbers $\Q_p$.
Let $d_p$ be the $p$-adic metric on $\Q_p$:
:$\forall x, y \in \Q_p: \map {d_p} {x, y} = \norm{x - y}_p$
Then $d_p$ is a non-Archimedean metric that extends the $p$-adic metric on the rationals $\Q$ to $\Q_p$.

Proof:
The $p$-adic metric on $\Q_p$ is defined as the metric induced by the $p$-adic norm on $\Q_p$.
It follows from Metric Induced by Norm is Metric that $d_p$ is a metric.
By definition of the $p$-adic norm on $\Q_p$, $\norm{\,\cdot\,}_p$ is a non-Archimedean norm.
From Non-Archimedean Norm iff Non-Archimedean Metric, then $d_p$ is a non-Archimedean metric.
From Rational Numbers are Dense Subfield of P-adic Numbers:
:the $p$-adic norm $\norm{\,\cdot\,}_p$ on the $p$-adic numbers $\Q_p$ is an extension of the $p$-adic norm $\norm{\,\cdot\,}_p$ on $\Q$.
By the definition of the metric induced by the $p$-adic norm, it follows that $d_p$ is an extension of the $p$-adic metric on the rationals $\Q$.
{{qed}}
Category:P-adic Metrics
rosnxpnyfigoa1sndry0w4kgokgh8vk
Theorem: Order of Automorphism Group of Cyclic Group

Let $C_n$ denote the cyclic group of order $n$.
Let $\Aut {C_n}$ denote the automorphism group of $C_n$.
Then:
:$\order {\Aut {C_n} } = \map \phi n$
where:
:$\order {\, \cdot \,}$ denotes the order of a group
:$\map \phi n$ denotes the Euler $\phi$ function.

Proof:
Let $g$ be a generator of $C_n$.
Let $\varphi$ be an automorphism on $C_n$.
By Homomorphic Image of Cyclic Group is Cyclic Group, $\map \varphi g$ is a generator of $C_n$.
By Homomorphism of Generated Group, $\varphi$ is uniquely determined by $\map \varphi g$.
By Finite Cyclic Group has Euler Phi Generators, there are $\map \phi n$ possible values for $\map \varphi g$.
Therefore there are $\map \phi n$ automorphisms on $C_n$:
:$\order {\Aut {C_n} } = \map \phi n$
{{qed}}
Theorem: Kernel of Group Homomorphism is not Empty

Let $G$ and $H$ be groups whose identity elements are $e_G$ and $e_H$ respectively.
Let $\phi: G \to H$ be a homomorphism from $G$ to $H$.
Let $\map \ker \phi$ denote the kernel of $\phi$.
Then:
:$\map \ker \phi \ne \O$
where $\O$ denotes the empty set.

Proof:
From Identity is in Kernel of Group Homomorphism we have that:
:$e_G \in \map \ker \phi$
Hence the result.
{{Qed}}
Theorem: Valuation Ring of P-adic Norm on Rationals/Corollary 1

The set of integers $\Z$ is a subring of $\OO$.

Proof:
By Valuation Ring of P-adic Norm on Rationals, the induced valuation ring $\OO$ is the set:
:$\OO = \Z_{\paren p} = \set {\dfrac a b \in \Q : p \nmid b}$
Since $p \nmid 1$ then for all $a \in \Z$, $a = \dfrac a 1 \in \OO$.
Hence $\Z \subseteq \OO$.
By Valuation Ring of Non-Archimedean Division Ring is Subring then $\OO$ is a subring of $\Q$.
By Integers form Subdomain of Rationals then $\Z$ is a subring of $\Q$.
By Intersection of Subrings is Largest Subring Contained in all Subrings then $\Z \cap \OO = \Z$ is a subring of $\OO$. 
{{qed}}
Theorem: Valuation Ring of P-adic Norm is Subring of P-adic Integers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $\Z_{\ideal p}$ be the induced valuation ring on $\struct {\Q,\norm {\,\cdot\,}_p}$.
Then:
:$(1): \quad \Z_{\ideal p} = \Q \cap \Z_p$.
:$(2): \quad \Z_{\ideal p}$ is a subring of $\Z_p$.

Proof:
The $p$-adic integers is defined as:
:$\Z_p = \set {x \in \Q_p: \norm x_p \le 1}$
The induced valuation ring on $\struct {\Q,\norm {\,\cdot\,}_p}$ is defined as:
:$\Z_{\ideal p} = \set {x \in \Q: \norm x_p \le 1}$
From Rational Numbers are Dense Subfield of P-adic Numbers:
:the $p$-adic norm $\norm {\,\cdot\,}_p$ on $\Q_p$ is an extension of the $p$-adic norm $\norm {\,\cdot\,}_p$ on $\Q$.
It follows that $\Z_{\ideal p} = \Q \cap \Z_p$.
This proves $(1)$ above.
By Valuation Ring of Non-Archimedean Division Ring is Subring then $\Z_p$ is a subring of $\Q_p$.
By definition of $p$-adic integers then $\Q$ is a subring of $\Q_p$.
By Intersection of Subrings is Largest Subring Contained in all Subrings then $\Z_{\paren p}$ is a subring of $\Z_p$.
This proves $(2)$ above.
{{qed}}
Theorem: Valuation Ring of P-adic Norm is Subring of P-adic Integers/Corollary 1

The set of integers $\Z$ is a subring of $\Z_p$.

Proof:
Let $\Z_{\paren p}$ be the valuation ring induced by $\norm {\,\cdot\,}_p$ on $\Q$.
By Integers form Subring of Valuation Ring of P-adic Norm on Rationals then:
:$\Z$ is a subring of $\Z_{\paren p}$
By Valuation Ring of P-adic Norm is Subring of P-adic Integers then:
:$\Z_{\paren p}$ is a subring of $\Z_p$
The result follows.
{{qed}}
Theorem: Laplace Transform of 1

Let $f: \R \to \R$ be the function defined as:
:$\forall t \in \R: \map f t = 1$
Then the Laplace transform of $\map f t$ is given by:
:$\laptrans {\map f t} = \dfrac 1 s$
for $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f t}
      | r = \laptrans 1
      | c = Definition of $\map f t$
}}
{{eqn | r = \int_0^{\to +\infty} e^{-s t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \int_0^L e^{-s t} \rd t
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \intlimits {-\frac 1 s e^{-s t} } 0 L
      | c = Primitive of Exponential Function
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {-\frac 1 s e^{-s L}  - \paren {-\frac 1 s} }
      | c = Exponential of Zero
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\frac {1 - e^{-s L} } s}
      | c = simplification
}}
{{eqn | r = \frac 1 s
      | c = Complex Exponential Tends to Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform Exists if Function Piecewise Continuous and of Exponential Order

Let $f$ be a real function which is:
:piecewise continuous in every closed interval $\closedint 0 N$
:of exponential order $\gamma$ for $t > N$.
Then the Laplace transform $\map F s$ of $\map f t$ exists for all $s > \gamma$.

Proof:
For all $N \in \Z_{>0}$:
:$\ds \int_0^\infty e^{-s t} \map f t \rd t = \int_0^N e^{-s t} \map f t \rd t + \int_N^\infty e^{-s t} \map f t \rd t$
We have that $f$ is piecewise continuous in every closed interval $\closedint 0 N$.
Hence the first of the integrals on the {{RHS}} exists.
Also, as $\map f t$ is of exponential order $\gamma$ for $t > N$, so does the second integral on the {{RHS}}.
Indeed:
{{begin-eqn}}
{{eqn | l = \size {\int_N^\infty e^{-s t} \map f t \rd t}
      | o = \le
      | r = \int_N^\infty \size {e^{-s t} \map f t} \rd t
      | c = 
}}
{{eqn | o = \le
      | r = \int_0^\infty e^{-s t} \size {\map f t} \rd t
      | c = 
}}
{{eqn | o = \le
      | r = \int_0^\infty e^{-s t} M e^{\gamma t} \rd t
      | c = 
}}
{{eqn | r = \dfrac M {s - \gamma}
      | c = Laplace Transform of Exponential
}}
{{end-eqn}}
Thus the Laplace transform exists for $s > \gamma$.
{{qed}}
Theorem: Laplace Transform of Derivative/Discontinuity at t = 0

Let $f$ fail to be continuous at $t = 0$, but let:
:$\ds \lim_{t \mathop \to 0} \map f t = \map f {0^+}$
exist.
Then $\laptrans f$ exists for $\map \Re s > a$, and:
:$\laptrans {\map {f'} t} = s \laptrans {\map f t} - \map f {0^+}$

Proof:
See Laplace Transform of Derivative/Discontinuity at t = a and use $a = 0$ and $\map f {0^-} = 0$.
Theorem: Laplace Transform of Derivative/Discontinuity at t = a

Let $f$ have a jump discontinuity at $t = a$.
Then:
:$\laptrans {\map {f'} t} = s \laptrans {\map f t} - \map f 0 - e^{-a s} \paren {\map f {a^+} - \map f {a^-} }$

Proof:
See Laplace Transform of Derivative with Finite Discontinuities and use $n = 1$ and $a_1 = a$.
Theorem: Laplace Transform of Integral

:$\ds \laptrans {\int_0^t \map f u \rd u} = \dfrac {\map F s} s$
wherever $\laptrans f$ exists.

Proof:
Let $\map g t = \ds \int_0^t \map f u \rd u$.
Then:
:$\map {g'} t = \map f t$
and:
:$\map g 0 = 0$
Thus:
{{begin-eqn}}
{{eqn | l = \laptrans {\map {g'} t}
      | r = s \laptrans {\map g t} - \map g 0
      | c = Laplace Transform of Derivative
}}
{{eqn | r = s \laptrans {\map g t}
      | c = 
}}
{{eqn | r = \map F s
      | c = as $\map F s = \laptrans {\map f t}$
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map g t}
      | r = \dfrac {\map F s} s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\int_0^t \map f u \rd u}
      | r = \dfrac {\map F s} s
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral of Laplace Transform

:$\ds \laptrans {\dfrac {\map f t} t} = \int_s^{\to \infty} \map F u \rd u$
wherever $\ds \lim_{t \mathop \to 0} \dfrac {\map f t} t$ and $\laptrans f$ exist.

Proof:
Let $\map g t := \dfrac {\map f t} t$.
Then:
{{begin-eqn}}
{{eqn | l = \map f t
      | r = t \map g t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = \laptrans {t \map g t}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = -\dfrac \d {\d s} \laptrans {\map g t}
      | c = Derivative of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = \map F s
      | r = -\dfrac {\d G} {\d s}
      | c = $\map F s := \laptrans {\map f t}$, and so on
}}
{{eqn | ll= \leadsto
      | l = \map G s
      | r = -\int_{-\infty}^s \map f u \rd u
      | c =
}}
{{eqn | r = \int_s^\infty \map f u \rd u
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Inclusion Mapping on Subring is Homomorphism

Let $\struct {R, +, \circ}$ be a ring.
Let $\struct {S, +{\restriction_S}, \circ {\restriction_S}}$ be a subring of $R$.
Let $i_S: S \to R$ be the inclusion mapping from $S$ to $R$.
Then ${i_S}$ is a ring homomorphism.

Proof:
Let $x, y \in S$.
Then:
{{begin-eqn}}
{{eqn | l = \map {i_S} x + \map {i_S} y
      | r = x + y
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | r = x \mathbin{ + {\restriction_S} } y
      | c = as $x, y \in S$
}}
{{eqn | r = \map {i_S} {x \mathbin{ + {\restriction_S} } y}
      | c = as $x \mathbin{ + {\restriction_S} } y \in S$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {i_S} x \circ \map {i_S} y
      | r = x \circ y
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | r = x \mathbin{\circ {\restriction_S} } y
      | c = as $x, y \in S$
}}
{{eqn | r = \map {i_S} {x \mathbin{ \circ {\restriction_S} } y}
      | c = as $x \mathbin{ \circ {\restriction_S} } y \in S$
}}
{{end-eqn}}
Hence ${i_S}$ is a ring homomorphism by definition.
{{qed}}
Category:Ring Homomorphisms
Category:Inclusion Mappings
n1i0aoahsj9suxon5donbspmxfj84sr
Theorem: Inclusion Mapping on Subring is Monomorphism

Let $\struct {R, +, \circ}$ be a ring.
Let $\struct {S, +{\restriction_S}, \circ {\restriction_S} }$ be a subring of $R$.
Let $i_S: S \to R$ be the inclusion mapping from $S$ to $R$.
Then $i_S$ is a ring monomorphism.

Proof:
By Inclusion Mapping on Subring is Homomorphism, $i_S$ is a ring homomorphism.
By Inclusion Mapping is Injection, $i_S$ is an injection.
The result follows by definition of (ring) monomorphism.
{{qed}}
Category:Group Monomorphisms
Category:Inclusion Mappings
h5ohqc6l5mbb3zoxs5vxcw9butsp61s
Theorem: Negative of Subring is Negative of Ring

Let $\struct {R, +, \circ}$ be a ring.
For each $x \in R$ let $-x$ denote the ring negative of $x$ in $R$.
Let $\struct {S, + {\restriction_S}, \circ {\restriction_S}}$ be a subring of $R$.
For each $x \in S$ let $\mathbin \sim x$ denote the ring negative of $x$ in $S$.
Then:
:$\forall x \in S: \mathbin \sim x = -x$

Proof:
Let $i_S: S \to R$ be the inclusion mapping from $S$ to $R$.
By Inclusion Mapping on Subring is Homomorphism, $i_S$ is a ring homomorphism.
By Ring Homomorphism of Addition is Group Homomorphism, $i_S$ is a group homomorphism on ring addition $+$.
Let $x \in S$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbin \sim x
      | r = \map {i_S} {\mathbin \sim x}
      | c = as $\mathbin \sim x \in S$
}}
{{eqn | r = -x
      | c = Group Homomorphism Preserves Inverses
}}
{{end-eqn}}
{{qed}}
Category:Ring Theory
m4kp7cy9zr5f3hq4oksoxoc5bccqsta
Theorem: Subtraction of Subring is Subtraction of Ring

Let $\struct {R, +, \circ}$ be an ring.
For each $x, y \in R$ let $x - y$ denote the subtraction of $x$ and $y$ in $R$.
Let $\struct {S, + {\restriction_S}, \circ {\restriction_S}}$ be a subring of $R$.
For each $x, y \in S$ let $x \sim y$ denote the subtraction of $x$ and $y$ in $S$.
Then:
:$\forall x, y \in S: x \sim y = x - y$

Proof:
Let $x, y \in S$.
Let $-x$ denote the ring negative of $x$ in $R$.
Let $\mathbin \sim x$ denote the ring negative of $x$ in $S$.
Then:
{{begin-eqn}}
{{eqn | l = x \sim y
      | r = x \mathbin {+ {\restriction_S} } \paren {\mathbin \sim y}
      | c = {{Defof|Ring Subtraction}}
}}
{{eqn | r = x + \paren {\mathbin \sim y}
      | c = {{Defof|Subring|Addition on Subring}}
}}
{{eqn | r = x + \paren {-y}
      | c = Negative of Subring is Negative of Ring
}}
{{eqn | r = x - y
      | c = {{Defof|Ring Subtraction}}
}}
{{end-eqn}}
{{qed}}
Category:Ring Theory
qt1dwlw2zy1nwl6tzgkgzzos92fs2na
Theorem: Initial Value Theorem of Laplace Transform

Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of the real function $f$.
Then:
:$\ds \lim_{t \mathop \to 0} \map f t = \lim_{s \mathop \to \infty} s \, \map F s$
if those limits exist.

Proof:
We have that $\map {f'} t$ is piecewise continuous with one-sided limits and of exponential order.
Hence:
:$\ds \lim_{s \mathop \to \infty} \int_0^\infty e^{-s t} \map {f'} t \rd t = 0$
Suppose that $f$ is continuous at $t = 0$.
From Laplace Transform of Derivative:
:$(1): \quad \laptrans {\map {f'} t} = s \map F s - \map f 0$
Taking the limit as $s \to \infty$ in $(1)$, where it is assumed that $\map f t$ is continuous at $t = 0$:
:$0 = \ds \lim_{s \mathop \to \infty} s \map F s - \map f 0$
or:
:$\ds \lim_{s \mathop \to \infty} s \map F s = \map f 0 = \lim_{t \mathop \to 0} \map f t$
{{qed|lemma}}
Suppose that $f$ is not continuous at $t = 0$.
From Laplace Transform of Derivative with Discontinuity at Zero:
:$\laptrans {\map {f'} t} = s \map F s - \map f {0^+}$
which means:
:$(2): \quad \laptrans {\map {f'} t} = s \map F s - \ds \lim_{u \mathop \to 0} \map f u$
Similarly taking the limit as $s \to \infty$ in $(2)$, where it is assumed that $\map f t$ is continuous at $t = 0$:
:$0 = \ds \lim_{s \mathop \to \infty} s \map F s - \lim_{u \mathop \to 0} \map f u$
and so:
:$\ds \lim_{s \mathop \to \infty} s \map F s = \lim_{u \mathop \to 0} \map f u = \lim_{t \mathop \to 0} \map f t$
{{qed}}
Theorem: Final Value Theorem of Laplace Transform

Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of the real function $f$.
Then:
:$\ds \lim_{t \mathop \to \infty} \map f t = \lim_{s \mathop \to 0} s \, \map F s$
if those limits exist.

Proof:
From Laplace Transform of Derivative:
:$(1): \quad \laptrans {\map {f'} t} = s \, \map F s - \map f 0$
We have that:
{{begin-eqn}}
{{eqn | l = \lim_{s \mathop \to 0} \laptrans {\map {f'} t}
      | r = \lim_{s \mathop \to 0} \int_0^\infty e^{-s t} \map {f'} t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^\infty \map {f'} t \rd t
      | c = 
}}
{{eqn | r = \lim_{L \mathop \to \infty} \int_0^L \map {f'} t \rd t
      | c = 
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\map f L - \map f 0}
      | c = Fundamental Theorem of Calculus
}}
{{eqn | n = 2
      | r = \lim_{t \mathop \to \infty} \map f t - \map f 0
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \lim_{s \mathop \to 0} \laptrans {\map {f'} t}
      | r = \lim_{s \mathop \to 0} s \, \map F s - \map f 0
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{t \mathop \to \infty} \map f t - \map f 0
      | r = \lim_{s \mathop \to 0} s \, \map F s - \map f 0
      | c = from $(2)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{t \mathop \to \infty} \map f t
      | r = \lim_{s \mathop \to 0} s \, \map F s
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Suppose that $f$ is not continuous at $t = 0$.
From Laplace Transform of Derivative with Discontinuity at Zero:
:$\laptrans {\map {f'} t} = s \, \map F s - \map f {0^+}$
which means:
:$(3): \quad \laptrans {\map {f'} t} = s \, \map F s - \ds \lim_{u \mathop \to 0} \map f u$
We have that:
{{begin-eqn}}
{{eqn | l = \lim_{s \mathop \to 0} \laptrans {\map {f'} t}
      | r = \lim_{u \mathop \to 0} \paren {\lim_{s \mathop \to 0} \int_u^\infty e^{-s t} \map {f'} t \rd t}
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \lim_{u \mathop \to 0} \paren {\int_u^\infty \map {f'} t \rd t}
      | c = 
}}
{{eqn | r = \lim_{u \mathop \to 0} \paren {\lim_{L \mathop \to \infty} \int_u^L \map {f'} t \rd t}
      | c = 
}}
{{eqn | r = \lim_{u \mathop \to 0} \paren {\lim_{L \mathop \to \infty} \paren {\map f L - \map f u} }
      | c = Fundamental Theorem of Calculus
}}
{{eqn | r = \lim_{u \mathop \to 0} \paren {\lim_{t \mathop \to \infty} \map f t - \map f u}
      | c = 
}}
{{eqn | n = 4
      | r = \lim_{t \mathop \to \infty} \map f t - \lim_{u \mathop \to 0} \map f u
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \lim_{s \mathop \to 0} \laptrans {\map {f'} t}
      | r = \lim_{s \mathop \to 0} s \, \map F s - \lim_{u \mathop \to 0} \map f u
      | c = from $(3)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{t \mathop \to \infty} \map f t - \lim_{u \mathop \to 0} \map f u
      | r = \lim_{s \mathop \to 0} s \, \map F s - \lim_{u \mathop \to 0} \map f u
      | c = from $(4)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{t \mathop \to \infty} \map f t
      | r = \lim_{s \mathop \to 0} s \, \map F s
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Evaluation of Integral using Laplace Transform

Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of the real function $f$.
Then:
:$\ds \int_0^{\to \infty} \map f t \rd t = \map F 0$
assuming the integral is convergent.

Proof:
By definition of Laplace transform:
:$\ds \int_0^{\to \infty} e^{-s t} \map f t \rd t = \map F s$
The result follows by taking the limit as $s \to 0$.
{{qed}}
Theorem: Valuation Ring of Non-Archimedean Division Ring is Clopen

Let $\struct {R, \norm {\,\cdot\,} }$ be a non-Archimedean normed division ring with zero $0_R$.
Let $\OO$ be valuation ring induced by $\norm{\,\cdot\,}$.
Then $\OO$ is a both open and closed in the metric induced by $\norm{\,\cdot\,}$.

Proof:
The valuation ring $\OO$ Is the open ball $\map {B_1^-} {0_R}$ by definition.
By Open Balls of Non-Archimedean Division Rings are Clopen then $\OO$ is both open and closed in the metric induced by $\norm {\,\cdot\,}$.
{{qed}}
Category:Normed Division Rings
Category:Valuation Ring of Non-Archimedean Division Ring is Clopen
p0p9p4h4opirp3ciwbjo8jbsgs3q8wq
Theorem: Valuation Ring of Non-Archimedean Division Ring is Clopen/Corollary 1

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Then the $p$-adic integers $\Z_p$ is both open and closed in the $p$-adic metric.

Proof:
The $p$-adic integers $\Z_p$ is the valuation ring induced by $\norm {\,\cdot\,}_p$ by definition.
By Valuation Ring of Non-Archimedean Division Ring is Clopen then the $p$-adic integers $\Z_p$ is both open and closed in the $p$-adic metric.
{{qed}}
Category:Valuation Ring of Non-Archimedean Division Ring is Clopen
iq83agm6hmowjjwe8npd7shuiggktor
Theorem: Bessel Function of the First Kind of Negative Integer Order

:$\map {J_{-n} } x = \paren {-1}^n \map {J_n} x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {J_{-n} } x 
      | r = \dfrac 1 \pi \int_0^\pi \map \cos {-n \theta - x \sin \theta} \rd \theta
      | c = Integral Representation of Bessel Function of the First Kind/Integer Order
}}
{{eqn | r = \dfrac 1 \pi \int_0^\pi \map \cos {-n \paren {\pi - \theta} - x \sin \paren {\pi - \theta} } \rd \paren {\pi - \theta}
      | c = substitution of $\pi - \theta$
}}
{{eqn | r = -\dfrac 1 \pi \int_\pi^0 \map \cos {n \theta - x \sin \theta - n \pi} \rd \theta
      | c = Sine of Supplementary Angle
}}
{{eqn | r = \dfrac 1 \pi \int_0^\pi \map \cos {n \theta - x \sin \theta - n \pi} \rd \theta
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = \paren {-1}^{-n} \dfrac 1 \pi \int_0^\pi \map \cos {n \theta - x \sin \theta} \rd \theta
      | c = Cosine of Angle plus Integer Multiple of Pi
}}
{{eqn | r = \paren {-1}^n \map {J_n} x
      | c = Integral Representation of Bessel Function of the First Kind/Integer Order
}}
{{end-eqn}}
{{qed}}