---

Step * 1 2 1 1 of Lemma unbounded-decidable-nset-infinite


1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. ∀j:ℕ. (-1 < j ⇒ (↑(d j)) ⇒ (n ≤ j))
⊢ ||filter(d;upto(n))|| = 0 ∈ ℕ
BY
{ (Assert ∀m:ℕ. (¬(m ∈ filter(d;upto(n)))) BY
         ((D 0 THENA Auto)
          THEN ((RWO "member_filter" 0 THENA Auto) THEN (RWO "member_upto" 0 THENA Auto))
          THEN (D 0 THENA Auto)
          THEN (D -1 THEN FHyp 3 [-1])
          THEN Auto)) }

1
1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. ∀j:ℕ. (-1 < j ⇒ (↑(d j)) ⇒ (n ≤ j))
4. ∀m:ℕ. (¬(m ∈ filter(d;upto(n))))
⊢ ||filter(d;upto(n))|| = 0 ∈ ℕ

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbN{}
3.  \mforall{}j:\mBbbN{}.  (-1  <  j  {}\mRightarrow{}  (\muparrow{}(d  j))  {}\mRightarrow{}  (n  \mleq{}  j))
\mvdash{}  ||filter(d;upto(n))||  =  0


By

---

Latex:
(Assert  \mforall{}m:\mBbbN{}.  (\mneg{}(m  \mmember{}  filter(d;upto(n))))  BY
              ((D  0  THENA  Auto)
                THEN  ((RWO  "member\_filter"  0  THENA  Auto)  THEN  (RWO  "member\_upto"  0  THENA  Auto))
                THEN  (D  0  THENA  Auto)
                THEN  (D  -1  THEN  FHyp  3  [-1])
                THEN  Auto))

---

Home Index