Step * 1 of Lemma mul-imax


1. : ℕ
2. : ℤ
3. : ℤ
4. ¬((n a) ≤ (n b))
5. a ≤ b
⊢ (n b) (n a) ∈ ℤ
BY
(D (-2) THEN EAuto 1) }


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  \mneg{}((n  *  a)  \mleq{}  (n  *  b))
5.  a  \mleq{}  b
\mvdash{}  (n  *  b)  =  (n  *  a)


By


Latex:
(D  (-2)  THEN  EAuto  1)




Home Index