---

Step * 1 1 of Lemma divides-iff-factors

.....assertion..... 
1. n : ℕ+
2. m : ℕ+
3. c : ℤ
4. m = (n * c) ∈ ℤ
⊢ 0 < c
BY
{ xxx((Assert (n * c) > 0 BY Auto) THEN (FLemma `pos_mul_arg_bounds` [-1]⋅ THENA Auto) THEN D -1 THEN Auto)xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  m  :  \mBbbN{}\msupplus{}
3.  c  :  \mBbbZ{}
4.  m  =  (n  *  c)
\mvdash{}  0  <  c


By

---

Latex:
xxx((Assert  (n  *  c)  >  0  BY
                      Auto)
        THEN  (FLemma  `pos\_mul\_arg\_bounds`  [-1]\mcdot{}  THENA  Auto)
        THEN  D  -1
        THEN  Auto)xxx

---

Home Index