Step
*
of Lemma
reg-less_wf
∀[x:ℝ]. ∀[y:{y:ℝ| ∃n:{ℕ+| (x n) + 4 < y n}} ]. (reg-less(x;y) ∈ {n:ℕ+| (x n) + 4 < y n} )
BY
{ ((UnivCD THENA Auto)
THEN D -1
THEN DupHyp (-1)
THEN (RWO "regular-less-iff" (-1) THENA Auto)
THEN (InstHyp [⌜4⌝] (-1)⋅ THENA Auto)
THEN ExRepD) }
1
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. (x n1) + 4 < y n1
5. ∀b:{4...}. ∃n:ℕ+. ∀m:{n...}. (x m) + b < y m
6. n : ℕ+
7. ∀m:{n...}. (x m) + 4 < y m
⊢ reg-less(x;y) ∈ {n:ℕ+| (x n) + 4 < y n}
Latex:
Latex:
\mforall{}[x:\mBbbR{}]. \mforall{}[y:\{y:\mBbbR{}| \mexists{}n:\{\mBbbN{}\msupplus{}| (x n) + 4 < y n\}\} ]. (reg-less(x;y) \mmember{} \{n:\mBbbN{}\msupplus{}| (x n) + 4 < y n\} )
By
Latex:
((UnivCD THENA Auto)
THEN D -1
THEN DupHyp (-1)
THEN (RWO "regular-less-iff" (-1) THENA Auto)
THEN (InstHyp [\mkleeneopen{}4\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN ExRepD)
Home
Index