---

Step * of Lemma multiply_functionality_wrt_le

∀[i1,i2:ℕ]. ∀[j1,j2:ℤ].  ((i1 * i2) ≤ (j1 * j2)) supposing ((i2 ≤ j2) and (i1 ≤ j1))
BY
{ Auto }

1
1. i1 : ℕ
2. i2 : ℕ
3. j1 : ℤ
4. j2 : ℤ
5. i1 ≤ j1
6. i2 ≤ j2
⊢ (i1 * i2) ≤ (j1 * j2)

---

Latex:

---

Latex:
\mforall{}[i1,i2:\mBbbN{}].  \mforall{}[j1,j2:\mBbbZ{}].    ((i1  *  i2)  \mleq{}  (j1  *  j2))  supposing  ((i2  \mleq{}  j2)  and  (i1  \mleq{}  j1))


By

---

Latex:
Auto

---

Home Index