---

Step * 1 1 of Lemma rmul-is-negative1

.....wf..... 
1. x : ℝ
2. y : ℝ
3. n : ℕ+
⊢ imax(|x 1|;|y 1|) + 4 ∈ {4...}
BY
{ (GenConcl ⌜imax(|x 1|;|y 1|) = M ∈ ℕ⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  imax(|x  1|;|y  1|)  +  4  \mmember{}  \{4...\}


By

---

Latex:
(GenConcl  \mkleeneopen{}imax(|x  1|;|y  1|)  =  M\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index