Theorem: P-adic Norm is Norm

The $p$-adic norm forms a norm on the rational numbers $\Q$.

Proof:
Recall that the $p$-adic norm is defined as:
:<nowiki>$\forall q \in \Q: \norm r_p := \begin {cases}
  0 & : r = 0 \\
  p^{- k} & : r \ne 0
\end {cases}$
</nowiki>
where:
:$r = p^k \dfrac m n$
and:
:$k, n \in \Z, m \in \Z_{\ne 0} : p \nmid m, n$
where $\nmid$ stands for "does not divide".
We must show that the norm axioms for all $r_1$, $r_2 \in \Q$:
{{begin-axiom}}
{{axiom | n = \text N 1
        | q = \forall r \in \Q
        | ml= \norm r_p = 0
        | mo= \iff
        | mr= x = 0
}}
{{axiom | n = \text N 2
        | q = \forall r_1, r_2 \in \Q
        | ml= \norm {r_1 r_2}
        | mo= =
        | mr= \norm {r_1}_p \times \norm {r_2}_p
}}
{{axiom | n = \text N 3
        | q = \forall r_1, r_2 \in \Q
        | ml= \norm {r_1 + r_2}_p
        | mo= \le
        | mr= \norm {r_1}_p + \norm {r_2}_p
}}
{{end-axiom}}
=== {{Norm-axiom-mult|1|nolink}} ===
Let $r \in \Q : r \ne 0$.
Let $k, m\in \Z, n \in \Z_{\ne 0} : p \nmid m, n$.
Suppose $r = 0$.
By definition:
:$\norm {r}_p = 0$
Suppose $r = p^k \dfrac m n \ne 0$
By definition:
:$\norm r_p = \dfrac 1 {p^k} > 0$
Suppose $\norm r_p = 0$.
By definition:
:$r = 0$
{{qed|lemma}}
=== {{Norm-axiom-mult|2|nolink}} ===
Suppose $r_1 = 0$ or $r_2 = 0$.
From {{Norm-axiom-mult|1}}, $\norm {r_1}_p = 0$ or $\norm {r_2}_p = 0$.
Suppose $r_1 \ne 0 \ne r_2$.
Let $k_1, k_2, m_1, m_2 \in \Z, n_1, n_2 \in \Z_{\ne 0} : p \nmid n_1, n_2, m_1, m_2$
Let $r_1 = p^{k_1} \dfrac {m_1} {n_1}, r_2 = p^{k_2} \frac {m_2} {n_2}$
Then:
:$r_1 r_2 = p^{k_1 + k_2} \dfrac {m_1 m_2}{n_1 n_2}$
We have that $p \nmid m_1$, $p \nmid m_2$.
Since $p$ is prime:
:$p \nmid m_1 m_2$.
Similarly:
:$p \nmid n_1 n_2$.
Therefore:
{{begin-eqn}}
{{eqn| l = \norm {r_1 r_2}_p 
     | r = p^{-\paren {k_1 + k_2} }
}}
{{eqn| r = p^{-k_1} p^{-k_2} 
}}
{{eqn| r = \norm {r_1}_p \norm {r_2}_p
}}
{{end-eqn}}
{{qed|lemma}}
=== {{Norm-axiom-mult|3|nolink}} ===
Suppose one of the following is true:
:$r_1 = 0$
:$r_2 = 0$
:$r_1 + r_2 = 0$
Then the result is straightforward.
Suppose $r_1 \ne 0$, $r_2 \ne 0$, $r_1 + r_2 \ne 0$.
Let $r_1 = p^{k_1} \dfrac {m_1} {n_1}, r_2 = p^{k_2} \dfrac {m_2} {n_2}$ where:
:$k_1, k_2, m_1, m_2 \in \Z, n_1, n_2 \in \Z_{\ne 0} : p \nmid m_1, m_2, n_1, n_2$
Then:
{{begin-eqn}}
{{eqn | l = r_1 + r_2
      | r = \frac {p^{k_1} m_1 n_2 + p^{k_2} m_2 n_1} {n_1 n_2}
}}
{{eqn | r = p^{\map \min {k_1, k_2} } \frac {p^{k_1 \mathop - \map \min {k_1, k_2} } m_1 n_2 + p^{k_2 \mathop - \map \min {k_1, k_2} } n_1 m_2} {n_1 n_2}
      | c = {{Defof|Min Operation}}
}}
{{eqn | r = p^{\map \min {k_1, k_2} } \frac {\tilde m} {n_1 n_2}
      | c = $\tilde m := p^{k_1 \mathop - \map \min {k_1, k_2} } m_1 n_2 + p^{k_2 \mathop - \map \min {k_1, k_2} } n_1 m_2$
}}
{{end-eqn}}
By Fundamental Theorem of Arithmetic:
:$\exists ! \tilde k \in \Z_{\ge 0} : \exists m \in \Z : p \nmid m : \tilde m = p^{\tilde k} m$
Obviously, $p \nmid n_1 n_2$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {r_1 + r_2}_p
      | r = \frac 1 {p^{\tilde k + \map \min {k_1, k_2} } }
}}
{{eqn | o = \le
      | r = \frac 1 {p^{\map \min {k_1, k_2} } }
}}
{{eqn | r = \map \max {p^{-k_1}, p^{-k_2} }
      | c = {{Defof|Max Operation}}
}}
{{eqn | r = \map \max {\norm {r_1}_p, \norm {r_1}_p}
}}
{{eqn | o = \le
      | r = \map \max {\norm {r_1}_p, \norm {r_2}_p} + \map \min {\norm {r_1}_p, \norm {r_2}_p}
}}
{{eqn | r = \norm {r_1}_p + \norm {r_2}_p
}}
{{end-eqn}}
{{qed|lemma}}
All norm axioms are seen to be satisfied.
Hence the result.
{{qed}}