Step
*
1
of Lemma
rless-int-fractions2
1. a : ℤ@i
2. b : ℤ@i
3. d : ℕ+@i
4. r(a) < (r(b)/r(d))@i
⊢ a * d < b
BY
{ (nRMul ⌜r(d)⌝ (-1)⋅ THEN Auto)⋅ }
1
1. a : ℤ@i
2. b : ℤ@i
3. d : ℕ+@i
4. r(a * d) < r(b)
⊢ a * d < b
Latex:
Latex:
1. a : \mBbbZ{}@i
2. b : \mBbbZ{}@i
3. d : \mBbbN{}\msupplus{}@i
4. r(a) < (r(b)/r(d))@i
\mvdash{} a * d < b
By
Latex:
(nRMul \mkleeneopen{}r(d)\mkleeneclose{} (-1)\mcdot{} THEN Auto)\mcdot{}
Home
Index