Step * 2 of Lemma fractions-rleq


1. : ℝ
2. : ℝ
3. : ℝ
4. : ℝ
5. r0 < c
6. r0 < d
7. (a d) ≤ (b c)
⊢ (a/c) ≤ (b/d)
BY
((nRMul ⌜c⌝ 0⋅ THENA Auto) THEN nRMul ⌜d⌝ 0⋅ THEN Auto) }


Latex:


Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  d  :  \mBbbR{}
5.  r0  <  c
6.  r0  <  d
7.  (a  *  d)  \mleq{}  (b  *  c)
\mvdash{}  (a/c)  \mleq{}  (b/d)


By


Latex:
((nRMul  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  nRMul  \mkleeneopen{}d\mkleeneclose{}  0\mcdot{}  THEN  Auto)




Home Index