---

Step * 1 3 of Lemma rinv_wf

.....antecedent..... 
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ ∃m:{1...}. (↑((λn.eval k = x n in 4 <z |k|) m))
BY
{ (Reduce 0 THEN ParallelLast) }

1
1. x : ℝ
2. n : ℕ+
3. 4 < |x n|
⊢ ↑eval k = x n in
   4 <z |k|

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \mBbbR{}
2.  \mexists{}n:\mBbbN{}\msupplus{}.  4  <  |x  n|
\mvdash{}  \mexists{}m:\{1...\}.  (\muparrow{}((\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|)  m))


By

---

Latex:
(Reduce  0  THEN  ParallelLast)

---

Home Index