---

Step * 1 1 of Lemma punit-norm1


1. n : ℕ
2. a : ℙ^n
⊢ (|(r1/||a||)| * ||a||) = r1
BY
{ ((RWO "rabs-rdiv" 0 THEN Auto) THEN Repeat ((RWO "rabs-of-nonneg" 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
\mvdash{}  (|(r1/||a||)|  *  ||a||)  =  r1


By

---

Latex:
((RWO  "rabs-rdiv"  0  THEN  Auto)  THEN  Repeat  ((RWO  "rabs-of-nonneg"  0  THEN  Auto)))

---

Home Index