---

Step * 1 of Lemma exp_assoced


1. n : ℕ+
2. x : ℤ
3. y : ℤ
4. x^n ~ y^n
⊢ x ~ y
BY
{ xxx(RepeatFor 2 (ParallelLast) THEN BLemma `exp-divides-exp2` THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbZ{}
3.  y  :  \mBbbZ{}
4.  x\^{}n  \msim{}  y\^{}n
\mvdash{}  x  \msim{}  y


By

---

Latex:
xxx(RepeatFor  2  (ParallelLast)  THEN  BLemma  `exp-divides-exp2`  THEN  Auto)xxx

---

Home Index