---

Step * of Lemma exp_assoced

∀n:ℕ+. ∀x,y:ℤ.  (x^n ~ y^n ⇐⇒ x ~ y)
BY
{ Auto }

1
1. n : ℕ+@i
2. x : ℤ@i
3. y : ℤ@i
4. x^n ~ y^n@i
⊢ x ~ y

2
1. n : ℕ+@i
2. x : ℤ@i
3. y : ℤ@i
4. x ~ y@i
⊢ x^n ~ y^n

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbZ{}.    (x\^{}n  \msim{}  y\^{}n  \mLeftarrow{}{}\mRightarrow{}  x  \msim{}  y)


By

---

Latex:
Auto

---

Home Index