---

Step * 1 of Lemma radd-positive-implies


1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. (r0 n) + 4 < (x + y) n
5. ¬4 < x (4 * n)
⊢ 4 < y (4 * n)
BY
{ (SupposeNot
   THEN (Assert ⌜¬(r0 n) + 4 < (x + y) n⌝⋅ THENM Auto)
   THEN (Assert ((x (4 * n)) + (y (4 * n))) ≤ 8 BY
               Auto)
   THEN RepeatFor 3 (Thin (-2))
   THEN (Subst' (r0 n) + 4 ~ 4 0 THENA (Computation THEN Auto))) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ((x (4 * n)) + (y (4 * n))) ≤ 8
⊢ ¬4 < (x + y) n

---

Latex:

---

Latex:

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


By

---

Latex:
(SupposeNot
  THEN  (Assert  \mkleeneopen{}\mneg{}(r0  n)  +  4  <  (x  +  y)  n\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  (Assert  ((x  (4  *  n))  +  (y  (4  *  n)))  \mleq{}  8  BY
                          Auto)
  THEN  RepeatFor  3  (Thin  (-2))
  THEN  (Subst'  (r0  n)  +  4  \msim{}  4  0  THENA  (Computation  THEN  Auto)))

---

Home Index