Step
*
1
of Lemma
m-k-regular-mcauchy
1. b : ℕ+
2. k : ℕ+
3. n : ℕ
4. m : ℕ
5. ((2 * b) * k) ≤ n
6. ((2 * b) * k) ≤ m
⊢ ((r(b)/r(n + 1)) + (r(b)/r(m + 1))) ≤ (r1/r(k))
BY
{ ((Assert (r(b)/r(m + 1)) ≤ (r1/r(2 * k)) BY
Auto)
THEN (Assert (r(b)/r(n + 1)) ≤ (r1/r(2 * k)) BY
Auto)
THEN (RWO "-1 -2" 0 THENA Auto)
THEN All Thin
THEN RWO "radd-int-fractions" 0
THEN Auto) }
Latex:
Latex:
1. b : \mBbbN{}\msupplus{}
2. k : \mBbbN{}\msupplus{}
3. n : \mBbbN{}
4. m : \mBbbN{}
5. ((2 * b) * k) \mleq{} n
6. ((2 * b) * k) \mleq{} m
\mvdash{} ((r(b)/r(n + 1)) + (r(b)/r(m + 1))) \mleq{} (r1/r(k))
By
Latex:
((Assert (r(b)/r(m + 1)) \mleq{} (r1/r(2 * k)) BY
Auto)
THEN (Assert (r(b)/r(n + 1)) \mleq{} (r1/r(2 * k)) BY
Auto)
THEN (RWO "-1 -2" 0 THENA Auto)
THEN All Thin
THEN RWO "radd-int-fractions" 0
THEN Auto)
Home
Index