Step
*
of Lemma
self_divisor_mul
∀a:ℤ-o. ∀b:ℤ.  (((a * b) | a) 
⇒ (b ~ 1))
BY
{ Auto }
1
1. a : ℤ-o
2. b : ℤ
3. (a * b) | a
⊢ b ~ 1
Latex:
Latex:
\mforall{}a:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}b:\mBbbZ{}.    (((a  *  b)  |  a)  {}\mRightarrow{}  (b  \msim{}  1))
By
Latex:
Auto
Home
Index