---

Step * 1 1 of Lemma radd-positive-implies


1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ((x (4 * n)) + (y (4 * n))) ≤ 8
⊢ ¬4 < (x + y) n
BY
{ ((RWO "radd-approx" 0 THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜(x (4 * n)) + (y (4 * n))⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. v : ℤ
2. v ≤ 8
⊢ ¬4 < v ÷ 4

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  ((x  (4  *  n))  +  (y  (4  *  n)))  \mleq{}  8
\mvdash{}  \mneg{}4  <  (x  +  y)  n


By

---

Latex:
((RWO  "radd-approx"  0  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}(x  (4  *  n))  +  (y  (4  *  n))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index