---

Step * 1 2 1 1 1 1 1 of Lemma sine-exists


1. x : ℝ
2. i : ℕ
⊢ x^2 * i = |x|^2 * i
BY
{ (RWO "rnexp-mul<" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  i  :  \mBbbN{}
\mvdash{}  x\^{}2  *  i  =  |x|\^{}2  *  i


By

---

Latex:
(RWO  "rnexp-mul<"  0  THEN  Auto)\mcdot{}

---

Home Index