Step * of Lemma divisor_of_mul

a,b,c:ℤ.  ((a b)  (a (b c)))
BY
(UnivCD THENA Auto) }

1
1. : ℤ
2. : ℤ
3. : ℤ
4. b
⊢ (b c)


Latex:


Latex:
\mforall{}a,b,c:\mBbbZ{}.    ((a  |  b)  {}\mRightarrow{}  (a  |  (b  *  c)))


By


Latex:
(UnivCD  THENA  Auto)




Home Index