avewright/proofwiki-math huggingface dataset:
Theorem: Principle of Stationary Action with Standard Lagrangian implies Newton's Laws of Motion

Let $\MM$ be an $n$-dimensional Euclidean manifold.
Let $P$ be a physical system composed of a countable number of classical particles with inertial masses $m_i$ with $i \in \N$.
Let $\mathbf x = \map {\mathbf x} t$ be twice-differentiable vector-valued function embedded in $\MM$.
Suppose ${\mathbf x}_i$ represents the position of the $i$th particle of $P$.
Suppose the action of $P$ is of the following form:
:$\ds S = \int_{t_0}^{t_1} L \rd t$
where $L$ is the standard Lagrangian.
Suppose, all (internal or external) forces ${\mathbf F}_i$ acting upon $P$ are of the form:
:${\mathbf F}_i = -\dfrac {\partial U} {\partial \mathbf x_i}$
where:
:$U = \map U {t, \set {\mathbf x_i} }$ is a differentiable real function
:$\set {\mathbf x_i}$ denotes dependence on the positions of all the particles.
Then the stationary point of $S$ implies Newton's Second Law of Motion.

Proof:
Standard Lagrangian is of the following form:
:$\ds L = \sum_{i \mathop = 1}^n \frac {m_i} 2 \dot {\mathbf x}_i^2 - U$
By the Principle of Stationary Action, equations of motion of $P$ are:
:$\forall i \in \N: m_i {\ddot {\mathbf x} }_i + \dfrac {\partial U} {\partial \mathbf x_i} = 0$
By definition of velocity:
:${\dot {\mathbf x} }_i = {\mathbf v}_i$
By assumption:
:${\mathbf F}_i = -\dfrac {\partial U} {\partial {\mathbf x}_i}$
Then it follows that the equations of motion of $P$ can be rewritten as:
:$\map {\dfrac \d {\d t} } {m_i {\mathbf v}_i } = {\mathbf F}_i$
By definition, these equations together represent Newton's Second Law of Motion.
{{qed}}
Theorem: Altitudes of Triangle Bisect Angles of Orthic Triangle

Let $\triangle ABC$ be a triangle.
Let $\triangle DEF$ be its orthic triangle.
The altitudes of $\triangle ABC$ are the angle bisectors of $\triangle DEF$.

Proof:
:400px
Consider the triangles $\triangle ABE$ and $\triangle ACF$.
We have that:
:$\angle FAC$ and $\angle BAE$ are common
:$\angle AFC$ and $\angle AEB$ are both right angles
and it follows from Triangles with Two Equal Angles are Similar that $\triangle ABE$ and $\triangle ACF$ are similar.
Thus:
:$\angle ABE = \angle ACF$
Consider the quadrilateral $\Box BFHD$.
We have that $\angle BFH$ and $\angle BDH$ are both right angles.
Thus two opposite angles of $\Box BFHD$ sum to two right angles
So by Opposite Angles of Cyclic Quadrilateral sum to Two Right Angles $\Box BFHD$ is a cyclic quadrilateral.
From Angles in Same Segment of Circle are Equal:
:$\angle FBH = \angle FDH$.
By similar analysis of quadrilateral $\Box DHEC$, we note that:
:$\angle HDE = \angle HCE$
But then we have:
:$\angle FBH = \angle ABE$
and:
:$\angle HCE = \angle ACF$
Hence it follows that:
:$\angle FDH = \angle HDE$
demonstrating that $AD$ is the angle bisector of $\angle FDE$.
The same argument applies {{mutatis}} to $\angle FDE$ and $\angle FED$.
Hence the result.
{{Qed}}
Theorem: Open Ball in Normed Division Ring is Open Ball in Induced Metric

Let $\struct{R, \norm {\,\cdot\,} }$ be a normed division ring.
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
Let $a \in R$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {B_\epsilon} {a; \norm {\,\cdot\,} }$ denote the open ball in the normed division ring $\struct {R, \norm {\,\cdot\,} }$.
Let $\map {B_\epsilon} {a; d }$ denote the open ball in the metric space $\struct {R, d}$.
Then:
:$\map {B_\epsilon} {a; \norm {\,\cdot\,} }$ = $\map {B_\epsilon} {a; d }$

Proof:
{{begin-eqn}}
{{eqn | l = x \in \map {B_\epsilon} {a; \norm {\,\cdot\,} }
      | o = \leadstoandfrom
      | r = \norm {x - a} < \epsilon
      | c = {{Defof|Open Ball of Normed Division Ring|Open Ball}} in $\struct {R, \norm {\,\cdot\,} }$
}}
{{eqn | o = \leadstoandfrom
      | r = \map d {x, a} < \epsilon
      | c = {{Defof|Metric Induced by Norm on Division Ring|Metric Induced}} by $\norm {\,\cdot\,}$
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \map {B_\epsilon} {a; d }
      | c = {{Defof|Open Ball of Metric Space|Open Ball}} in $\struct {R, d}$
}}
{{end-eqn}}
The result follows from Equality of Sets.
{{qed}}
Theorem: Closed Ball in Normed Division Ring is Closed Ball in Induced Metric

Let $\struct{R, \norm {\,\cdot\,} }$ be a normed division ring.
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
Let $a \in R$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {{B_\epsilon}^-} {a; \norm {\,\cdot\,} }$ denote the closed ball in the normed division ring $\struct {R, \norm {\,\cdot\,} }$.
Let $\map {{B_\epsilon}^-} {a; d }$ denote the closed ball in the metric space $\struct {R, d}$.
Then:
:$\map {{B_\epsilon}^-} {a; \norm {\,\cdot\,} }$ = $\map {{B_\epsilon}^-} {a; d }$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map { {B_\epsilon}^-} {a; \norm {\,\cdot\,} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \norm {x - a}
      | o = \le
      | r = \epsilon
      | c = {{Defof|Closed Ball of Normed Division Ring}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map d {x, a}
      | o = \le
      | r = \epsilon
      | c = {{Defof|Metric Induced by Norm on Division Ring}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \map { {B_\epsilon}^-} {a; d }
      | c = {{Defof|Closed Ball}}
}}
{{end-eqn}}
The result follows from Equality of Sets.
{{qed}}
Theorem: Sphere in Normed Division Ring is Sphere in Induced Metric

Let $\struct{R, \norm {\,\cdot\,} }$ be a normed division ring.
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
Let $a \in R$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {S_\epsilon} {a; \norm {\,\cdot\,} }$ denote the sphere in the normed division ring $\struct {R, \norm {\,\cdot\,} }$.
Let $\map {S_\epsilon} {a; d }$ denote the sphere in the metric space $\struct {R, d}$.
Then:
:$\map {S_\epsilon} {a; \norm {\,\cdot\,} }$ = $\map {S_\epsilon} {a; d }$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {S_\epsilon} {a; \norm {\,\cdot\,} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \norm {x - a}
      | r = \epsilon
      | c = {{Defof|Sphere in Normed Division Ring}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map d {x, a}
      | r = \epsilon
      | c = {{Defof|Metric Induced by Norm on Division Ring}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \map {S_\epsilon} {a; d }
      | c = {{Defof|Sphere}} in $\struct {R, d}$
}}
{{end-eqn}}
The result follows from Equality of Sets.
{{qed}}
Theorem: Sphere is Set Difference of Closed Ball with Open Ball

Let $M = \struct{A, d}$ be a metric space or pseudometric space.
Let $a \in A$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {{B_\epsilon}^-} {a; d}$ denote the closed $\epsilon$-ball of $a$ in $M$.
Let $\map {B_\epsilon} {a; d}$ denote the open $\epsilon$-ball of $a$ in $M$.
Let $\map {S_\epsilon} {a; d}$ denote the $\epsilon$-sphere of $a$ in $M$.
Then:
:$\map {S_\epsilon} {a; d} = \map { {B_\epsilon}^-} {a; d} \setminus \map {B_\epsilon} {a; d}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {S_\epsilon } a
      | r = \set {x : \map d {x, a} = \epsilon}
      | c = {{Defof|Sphere}}
}}
{{eqn | r = \set {x : \map d {x, a} \le \epsilon} \setminus \set {x : \map d {x, a} < \epsilon }
      | c = 
}}
{{eqn | r = \set {x : \map d {x, a} \le \epsilon} \setminus \map {B_\epsilon} a
      | c = {{Defof|Open Ball of Metric Space}}
}}
{{eqn | r = \map { {B_\epsilon}^- } a \setminus \map {B_\epsilon } a
      | c = {{Defof|Closed Ball of Metric Space}}
}}
{{end-eqn}}
{{qed}}
Category:Metric Spaces
Category:Closed Balls
Category:Open Balls
azeopxkbfxxtk6e9g5jguvy5hk9tocd
Theorem: Sphere is Set Difference of Closed Ball with Open Ball/Normed Division Ring

Let $\struct{R, \norm {\,\cdot\,} }$ be a normed division ring.
Let $a \in R$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {{B_\epsilon}^-} {a; \norm {\,\cdot\,} }$ denote the $\epsilon$-closed ball of $a$ in $\struct {R, \norm {\,\cdot\,} }$.
Let $\map {B_\epsilon} {a; \norm {\,\cdot\,} }$ denote the $\epsilon$-open ball of $a$ in $\struct {R, \norm {\,\cdot\,} }$.
Let $\map {S_\epsilon} {a; \norm {\,\cdot\,} }$ denote the $\epsilon$-sphere of $a$ in $\struct {R, \norm {\,\cdot\,} }$.
Then:
:$\map {S_\epsilon} {a; \norm {\,\cdot\,} } = \map { {B_\epsilon}^-} {a; \norm {\,\cdot\,} } \setminus \map {B_\epsilon} {a; \norm {\,\cdot\,} }$

Proof:
The result follows directly from:
:Closed Ball in Normed Division Ring is Closed Ball in Induced Metric
:Open Ball in Normed Division Ring is Open Ball in Induced Metric
:Sphere in Normed Division Ring is Sphere in Induced Metric
:Sphere is Set Difference of Closed Ball with Open Ball
{{qed}}
Category:Normed Division Rings
6vn02xt3symwmexuwwu1ze2ydr4u7br
Theorem: Conservation of Energy

Let $P$ be a physical system.
Let it have the action $S$:
:$\ds S = \int_{t_0}^{t_1} L \rd t$
where $L$ is the standard Lagrangian, and $t$ is time.
Suppose $L$ does not depend on time explicitly:
:$\dfrac {\partial L} {\partial t} = 0$
Then the total energy of $P$ is conserved.

Proof:
By assumption, $S$ is invariant under the following family of transformations:
:$T = t + \epsilon$
:$\mathbf X = \mathbf x$
By Noether's Theorem:
:$\nabla_{\dot {\mathbf x} } L \cdot \boldsymbol \psi + \paren {L - \dot {\mathbf x} \cdot \nabla_{\dot {\mathbf x} } L} \phi = C$
where $\phi = 1$, $\boldsymbol \psi = \mathbf 0$ and $C$ is an arbitrary constant.
Then it follows that:
{{begin-eqn}}
{{eqn | l = L - \dot {\mathbf x} \cdot \nabla_{\dot {\mathbf x} } L
      | r = T - U - \dot {\mathbf x} \cdot \nabla_{\dot{\mathbf x} } \paren {T - U}
}}
{{eqn | r = T - U - \dot {\mathbf x} \cdot \nabla_{\dot{\mathbf x} } \paren{\frac m 2 \dot {\mathbf x}^2}
}}
{{eqn | r = T - U - m \dot {\mathbf x}^2
}}
{{eqn | r = T - U - 2 T
}}
{{eqn | r = - \paren {T + U}
}}
{{end-eqn}}
Since the last term is the total energy of $P$, we conclude that it is conserved.
{{qed}}
Theorem: Principle of Conservation of Linear Momentum

Let $P$ be a physical system.
Let it have the action $S$:
:$\ds S = \int_{t_0}^{t_1} L \rd t$
where $L$ is the standard Lagrangian, and $t$ is time.
Suppose $L$ does not depend on one of the coordinates explicitly:
:$\dfrac {\partial L} {\partial x_j} = 0$
Then the total momentum of $P$ along the axis $x_j$ is conserved.

Proof:
By assumption, $S$ is invariant under the following family of transformations:
:$T = t$
:$X_j = x_j + \epsilon$
:$X_{i \mathop \ne j} = x_{i \mathop \ne j}$
By Noether's Theorem:
:$\nabla_{\mathbf x} L \cdot \boldsymbol \psi + \paren {L - \dot {\mathbf x} \cdot \nabla_{\dot {\mathbf x} } L} \phi = C$
where $\phi = 0$, $\psi_i = 1$,  $\psi_{j \mathop \ne i} = 0$  and $C$ is an arbitrary constant.
Then it follows that:
:$\dfrac {\partial L} {\partial x_j} = C$
Since the last term is the momentum of $P$, we conclude that it is conserved.
{{qed}}
Theorem: Conservation of Angular Momentum (Lagrangian Mechanics)

Let $P$ be a physical system composed of a finite number of particles.
Let $P$ have the action $S$:
:$\ds S = \int_{t_0}^{t_1} L \rd t$
where:
:$L$ is the standard Lagrangian
:$t$ is time.
Let $L$ be invariant {{WRT}} rotation around the $z$-axis.
Then the total angular momentum of $P$ along the $z$-axis is conserved.

Proof:
By assumption, $S$ is invariant under the following family of transformations:
{{begin-eqn}}
{{eqn | l = T
      | r = t
}}
{{eqn | l = X_i
      | r = x_i \cos \epsilon + y_i \sin \epsilon
}}
{{eqn | l = Y_i
      | r = -x_i \sin \epsilon + y_i \cos \epsilon
}}
{{eqn | l = Z_i
      | r = z_i
}}
{{end-eqn}}
where $\epsilon \in \R$.
By Noether's Theorem:
:$\nabla_{\dot {\mathbf x} } L \cdot \boldsymbol \psi + \paren {L - \dot {\mathbf x} \cdot \nabla_{\dot {\mathbf x} } L } \phi = C$
where:
{{begin-eqn}}
{{eqn | l = \phi
      | r = 0
}}
{{eqn | l = \psi_{i x}
      | r = \valueat {\dfrac {\partial X_i} {\partial \epsilon} } {\epsilon \mathop = 0}
      | rr= = y_i
}}
{{eqn | l = \psi_{i y}
      | r = \valueat {\dfrac {\partial Y_i} {\partial \epsilon} } {\epsilon \mathop = 0}
      | rr= = -x_i
}}
{{eqn | l = \psi_{i z}
      | r = 0
}}
{{end-eqn}}
and $C$ is an arbitrary constant.
Then it follows that:
:$\ds \sum_i \paren {\dfrac {\partial L} {\partial {\dot x}_i} y_i - \dfrac {\partial L} {\partial {\dot y}_i} x_i} = C$
Since the {{RHS}} is the $z$ component of angular momentum of $P$ along the $z$-axis, we conclude that it is conserved.
{{qed}}
Theorem: Leibniz's Law for Sets

Let $S$ be an arbitrary set.
Then:
:$x = y \dashv \vdash x \in S \iff y \in S$
for all $S$ in the universe of discourse.
This is therefore the justification behind the notion of the definition of set equality.

Proof:
A direct application of Leibniz's law.
Theorem: Area of Annulus

Let $A$ be an annulus whose inner radius is $r$ and whose outer radius is $R$.
The area of $A$ is given by:
:$\map \Area A = \pi \paren {R^2 - r^2}$

Proof:
:400px
The area of $A$ is seen to be:
:the area of the outer circle with the area of the inner circle removed.
From Area of Circle:
:the area of the outer circle is $\pi R^2$
:the area of the inner circle is $\pi r^2$
The result follows.
{{qed}}
Theorem: Area of Annulus as Area of Rectangle

Let $A$ be an annulus whose inner radius is $r$ and whose outer radius is $R$.
The area of $A$ is given by:
:$\map \Area A = 2 \pi \paren {r + \dfrac w 2} \times w$
where $w$ denotes the width of $A$.
That is, it is the area of the rectangle contained by:
:the width of $A$
:the circle midway in radius between the inner radius and outer radius of $A$.

Proof:
:400px
{{begin-eqn}}
{{eqn | l = \map \Area A
      | r = \pi \paren {R^2 - r^2}
      | c = Area of Annulus
}}
{{eqn | r = \pi \paren {\paren {r + w}^2 - r^2}
      | c = {{Defof|Width of Annulus}}
}}
{{eqn | r = \pi \paren {r^2 + 2 r w + w^2 - r^2}
      | c = Square of Sum
}}
{{eqn | r = \pi \paren {2 r + w} w 
      | c = simplifying
}}
{{eqn | r = 2 \pi \paren {r + \frac w 2} \times w 
      | c = extracting $2$
}}
{{end-eqn}}
The result follows from Area of Rectangle.
{{Qed}}
Theorem: Hamiltonian of Standard Lagrangian is Total Energy

Let $P$ be a physical system of classical particles.
Let $L$ be a standard Lagrangian associated with $P$.
Then the Hamiltonian of $P$ is the total energy of $P$.

Proof:
{{begin-eqn}}
{{eqn | l = H 
      | r = -L + \sum_{i \mathop = 1}^n \dot {x_i} L_{\dot {x_i} }
}}
{{eqn | r = - \paren{T - V} + \sum_{i \mathop = 1}^n \dot {x_i} \dfrac {\partial} {\partial {\dot x}_i }\paren {\map T {\dot x} - \map V {t, x} }
      | c = {{Defof|Standard Lagrangian}}
}}
{{eqn | r = -\paren{T - V} + \sum_{i \mathop = 1}^n m_i \dot {x_i}^2
      | c = Kinetic Energy of Classical Particle
}}
{{eqn | r = -T + V + 2 T
      | c = Kinetic Energy of Classical Particle
}}
{{eqn | r = T + V
}}
{{end-eqn}}
By definition, the last expression is the total energy of $P$.
{{qed}}
Theorem: Characterization of Closed Ball in P-adic Numbers

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.
For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map {{B_\epsilon}^-} a$ denote the closed ball of center $a$ of radius $\epsilon$. 
Let $x, y \in \Q_p$.
Let $n \in \Z$.
{{TFAE}}
::$(1)\quad x \in \map {B^{\,-}_{p^{-n}}} y$
::$(2)\quad \norm{x -y}_p \le p^{-n}$
::$(3)\quad \map {B^{\,-}_{p^{-n}}} x = \map {B^{\,-}_{p^{-n}}} y$
::$(4)\quad x - y \in p^n \Z_p$
::$(5)\quad x + p^n \Z_p = y + p^n \Z_p$

Proof:
From P-adic Numbers form Non-Archimedean Valued Field:
:$\norm {\,\cdot\,}_p$ is a non-Archimedean norm.
Theorem: Characterization of Open Ball in P-adic Numbers

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.
For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map {B_\epsilon} a$ denote the open ball of center $a$ of radius $\epsilon$. 
Let $n \in \Z$.
Let $x, y \in \Q_p$.
{{TFAE}}
:$(1): \quad x \in \map {B_{p^{-n} } } y$
:$(2): \quad \norm{x - y}_p < p^{-n}$
:$(3): \quad \map {B_{p^{-n} } } x = \map {B_{p^{-n} } } y$
:$(4): \quad x - y \in p^{n + 1} \Z_p$
:$(5): \quad x + p^{n + 1} \Z_p = y + p^{n + 1} \Z_p$

Proof:
From P-adic Numbers form Non-Archimedean Valued Field:
:$\norm {\,\cdot\,}_p$ is a non-Archimedean norm.
Theorem: Poisson Brackets of Harmonic Oscillator

Let $P$ be a classical harmonic oscillator.
Let the real-valued function $\map x t$ be the position of $P$, where $t$ is time.
Then $P$ has the following Poisson brackets:
{{begin-eqn}}
{{eqn | l = \sqbrk {x, p}
      | r = 1
}}
{{eqn | l = \sqbrk {x, H}
      | r = \dfrac p m
}}
{{eqn | l = \sqbrk {p, H}
      | r = -k x
}}
{{end-eqn}}

Proof:
The standard Lagrangian of $P$ is:
:$L = \dfrac 1 2 \paren {m {\dot x}^2 - k x^2}$
The canonical momentum is:
:$p = \dfrac {\partial L} {\partial \dot x} = m \dot x$
The Hamiltonian associated to $L$ in canonical coordinates reads:
:$H = \dfrac {p^2} {2 m} + \dfrac k 2 x^2$
Then:
{{begin-eqn}}
{{eqn | l = \sqbrk {x, p}
      | r = \dfrac {\partial x} {\partial x} \dfrac {\partial p} {\partial p} - \dfrac {\partial p} {\partial x} \dfrac {\partial x} {\partial p} 
      | rr= = 1
}}
{{eqn | l = \sqbrk {x, H}
      | r = \dfrac {\partial x} {\partial x} \dfrac {\map \partial {\frac {p^2} {2 m} + \frac {k x^2} 2} } {\partial p} - \dfrac {\map \partial {\frac {p^2} {2 m} + \frac {k x^2} 2} } {\partial x} \dfrac {\partial x} {\partial p} 
      | rr= = \dfrac p m
}}
{{eqn | l = \sqbrk {p, H}
      | r = \dfrac {\partial p} {\partial x} \dfrac {\map \partial {\frac {p^2} {2 m} + \frac {k x^2} 2} } {\partial p} - \dfrac {\map \partial {\frac {p^2} {2 m} + \frac {k x^2} 2} } {\partial x} \dfrac {\partial p} {\partial p} 
      | rr= = -k x
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Convergent P-adic Sequence

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\sequence {x_n} $ be a sequence in $\Q_p$.
{{TFAE|def = Convergent P-adic Sequence|view = convergent $p$-adic sequence}}
=== Definition 1 ===
{{:Definition:Convergent Sequence/P-adic Numbers/Definition 1|Definition 1}}
=== Definition 2 ===
{{:Definition:Convergent Sequence/P-adic Numbers/Definition 2}}
=== Definition 3 ===
{{:Definition:Convergent Sequence/P-adic Numbers/Definition 3}}
=== Definition 4 ===
{{:Definition:Convergent Sequence/P-adic Numbers/Definition 4}}

Proof:
From P-adic Numbers form Non-Archimedean Valued Field:
:the $p$-adic norm is the norm on a division ring.
By definition, the $p$-adic metric is the metric induced by the $p$-adic norm.
From Equivalence of Definitions of Convergence in Normed Division Rings, it follows that 
Definition 2, Definition 3 and Definition 4 are equivalent.
By definition of convergence in a normed division ring, $\sequence {x_n}$ converges to $x$ in the $p$-adic norm {{iff}}:
:$\forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \norm {x_n - x}_p < \epsilon$
So Definition 1 is equivalent to Definition 2.
{{qed}}
Category:Sequences
Category:Convergence
Category:P-adic Number Theory
jj3d70ycwgaba4rcf3bguzuk7hlpacc
Theorem: Equivalence of Definitions of Convergence in Normed Division Rings

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\sequence {x_n}$ be a sequence in $R$.
{{TFAE|def = Convergent Sequence in Normed Division Ring}}
=== Definition 1 ===
{{:Definition:Convergent Sequence/Normed Division Ring/Definition 1}}
=== Definition 2 ===
{{:Definition:Convergent Sequence/Normed Division Ring/Definition 2}}
=== Definition 3 ===
{{:Definition:Convergent Sequence/Normed Division Ring/Definition 3}}
=== Definition 4 ===
{{:Definition:Convergent Sequence/Normed Division Ring/Definition 4}}

Proof:
=== Definition 1 iff Definition 2 ===
By definition, the metric induced by the norm $\norm {\, \cdot \,}$ is the mapping $d: R \times R \to \R_{\ge 0}$ defined as:
:$\map d {x, y} = \norm {x - y}$
From Metric Induced by Norm on Normed Division Ring is Metric, $d$ is a metric.
By definition of a convergent sequence in a metric space, $\sequence{x_n}$ converges to $x \in R$ {{iff}}:
:$\forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \map d {x_n, x} < \epsilon$
{{iff}}:
:$\forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \norm {x_n - x} < \epsilon$
The result follows.
{{qed|lemma}}
Theorem: Finite Complement Topology is not Metrizable

Let $T = \struct {S, \tau}$ be a finite complement topology on an infinite set $S$.
Then $T$ is not a metrizable space.

Proof:
We have:
:Metrizable Space is Hausdorff
:Finite Complement Space is not $T_2$ (Hausdorff)
Hence the result.
{{qed}}
Theorem: Multiplication by Power of 10 by Moving Decimal Point

Let $n \in \R$ be a real number.
Let $n$ be expressed in decimal notation.
Let $10^d$ denote a power of $10$ for some integer $d$
Then $n \times 10^d$ can be expressed in decimal notation by shifting the decimal point $d$ places to the right.
Thus, if $d$ is negative, and so $10^d = 10^{-e}$ for some $e \in \Z_{>0}$, $n \times 10^d$ can be expressed in decimal notation by shifting the decimal point $e$ places to the left.

Proof:
Let $n$ be expressed in decimal notation as:
:$n = \sqbrk {a_r a_{r - 1} \dotso a_1 a_0 \cdotp a_{-1} a_{-2} \dotso a_{-s} a_{-s - 1} \dotso}$
That is:
:$n = \ds \sum_{k \mathop \in \Z} a_k 10^k$
Then:
{{begin-eqn}}
{{eqn | l = n \times 10^d
      | r = 10^d \times \sum_{k \mathop \in \Z} a_k 10^k
      | c = 
}}
{{eqn | r = \sum_{k \mathop \in \Z} 10^d \times a_k 10^k
      | c = Distributive Property
}}
{{eqn | r = \sum_{k \mathop \in \Z} a_k 10^{k + d}
      | c = Product of Powers
}}
{{eqn | r = \sum_{k \mathop \in \Z} a_{k - d} 10^k
      | c = Translation of Index Variable of Summation
}}
{{end-eqn}}
The effect of presenting digit $a_{k - d}$ in position $k$ of $n$ is the same as what you get having moved the decimal point from between $a_0$ and $a_{-1}$ to between $a_{-d}$ and $a_{-d - 1}$.
Thus:
:if $d$ is positive, that is equivalent to moving the decimal point $d$ places to the right
and:
:if $d$ is negative, that is equivalent to moving the decimal point $d$ places to the left.
{{qed}}
Theorem: Number of Significant Figures in Result of Multiplication

Let $m$ and $n$ be numbers which are presented to $d_m$ and $d_n$ significant figures respectively.
Then the most significant figures that $m \times n$ can have is $\min \set {d_m, d_n}$.

Proof:
{{ProofWanted|I need a run-up.}}
Theorem: Number of Significant Figures in Result of Division

Let $m$ and $n$ be numbers which are presented to $d_m$ and $d_n$ significant figures respectively.
Then the most significant figures that $\dfrac m n$ can have is $\min \set {d_m, d_n}$.

Proof:
{{ProofWanted|I need a run-up.}}
Theorem: Number of Significant Figures in Result of Square Root

Let $m$ be a number which is presented to $d$ significant figures.
Then the most significant figures that $\sqrt m$ can have is also $d$.

Proof:
{{ProofWanted|I need a run-up.}}
Theorem: Number of Significant Figures in Result of Addition or Subtraction

Let $m$ and $n$ be numbers.
Let $d_m$ and $d_n$ be the position of the {{LSD}} of $m$ and $n$ respectively.
Then the {{LSD}} in either $m + n$ or $m - n$ is in the position corresponding to the greater significant digit of $d_m$ and $d_n$.

Proof:
{{ProofWanted|I need a run-up.}}
Theorem: Range of Common Logarithm of Number between 1 and 10

Let $x \in \R$ be a real number such that:
:$1 \le x < 10$
Then:
:$0 \le \log_{10} x \le 1$
where $\log_{10}$ denotes the common logarithm function.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 1
      | r = 10^0
      | c = {{Defof|Integer Power}}
}}
{{eqn | l = 10
      | r = 10^1
      | c = {{Defof|Integer Power}}
}}
{{eqn | ll= \leadsto
      | l = \log_{10} 1
      | r = 0
      | c = 
}}
{{eqn | l = \log_{10} 10
      | r = 1
      | c = 
}}
{{end-eqn}}
The result follows from Logarithm is Strictly Increasing.
{{explain|Strictly speaking we need another step in here, the above is just for the natural logarithm.}}