---

Step * 1 of Lemma multiply_functionality_wrt_le


1. i1 : ℕ
2. i2 : ℕ
3. j1 : ℤ
4. j2 : ℤ
5. i1 ≤ j1
6. i2 ≤ j2
⊢ (i1 * i2) ≤ (j1 * j2)
BY
{ (Using [`n',⌜i1⌝] (FwdThruLemma `mul_preserves_le` [6]) THENA Auto) }

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

---

Latex:

---

Latex:

1.  i1  :  \mBbbN{}
2.  i2  :  \mBbbN{}
3.  j1  :  \mBbbZ{}
4.  j2  :  \mBbbZ{}
5.  i1  \mleq{}  j1
6.  i2  \mleq{}  j2
\mvdash{}  (i1  *  i2)  \mleq{}  (j1  *  j2)


By

---

Latex:
(Using  [`n',\mkleeneopen{}i1\mkleeneclose{}]  (FwdThruLemma  `mul\_preserves\_le`  [6])  THENA  Auto)

---

Home Index