Step * of Lemma exp-divides-exp2

x,y:ℤ.  (x ⇐⇒ ∃n:ℕ+(x^n y^n))
BY
(Auto THEN ExRepD) }

1
1. : ℤ
2. : ℤ
3. y
⊢ ∃n:ℕ+(x^n y^n)

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


Latex:


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


By


Latex:
(Auto  THEN  ExRepD)




Home Index