---

Step * of Lemma rnexp-rmul

No Annotations
∀[n:ℕ]. ∀[x,y:ℝ].  (x * y^n = (x^n * y^n))
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto) }

1
1. n : ℤ
2. 0 < n
3. ∀[x,y:ℝ].  (x * y^n - 1 = (x^n - 1 * y^n - 1))
4. x : ℝ
5. y : ℝ
⊢ x * y^n = (x^n * y^n)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}].    (x  *  y\^{}n  =  (x\^{}n  *  y\^{}n))


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Auto)

---

Home Index