Step
*
1
of Lemma
rmul_reverses_rleq
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. x ≤ z
5. y ≤ r0
⊢ (z * y) ≤ (x * y)
BY
{ (((FLemma `rminus-reverses-rleq` [-1]) THENM (nRNorm (-1))) THEN Auto) }
1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. x ≤ z
5. y ≤ r0
6. r0 ≤ -(y)
⊢ (z * y) ≤ (x * y)
Latex:
Latex:
1. x : \mBbbR{}
2. y : \mBbbR{}
3. z : \mBbbR{}
4. x \mleq{} z
5. y \mleq{} r0
\mvdash{} (z * y) \mleq{} (x * y)
By
Latex:
(((FLemma `rminus-reverses-rleq` [-1]) THENM (nRNorm (-1))) THEN Auto)
Home
Index