Step * of Lemma self_divisor_mul

a:ℤ-o. ∀b:ℤ.  (((a b) a)  (b 1))
BY
Auto }

1
1. : ℤ-o
2. : ℤ
3. (a b) a
⊢ 1


Latex:


Latex:
\mforall{}a:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}b:\mBbbZ{}.    (((a  *  b)  |  a)  {}\mRightarrow{}  (b  \msim{}  1))


By


Latex:
Auto




Home Index