---

Step * of Lemma rnexp_functionality

No Annotations
∀[n:ℕ]. ∀[x,y:ℝ].  x^n = y^n supposing x = y
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto THEN (RWO "rnexp_unroll" 0 THEN Auto) THEN RepeatFor 2 (AutoSplit)) }

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

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "rnexp\_unroll"  0  THEN  Auto)
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index