---

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


1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. m : ℕ
4. m < n
5. ∀j:ℕ. (m < j ⇒ (↑(d j)) ⇒ (n ≤ j))
6. ↑(d m)
7. (∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n)))))
   ∧ no_repeats(ℕ;filter(d;[m, n)))
   ∧ 0 < ||filter(d;[m, n))|| 
   supposing ||filter(d;[m, n))|| = 1 ∈ ℤ
8. ∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n))))
9. no_repeats(ℕ;filter(d;[m, n)))
⊢ 0 < ||filter(d;[m, n))||
BY
{ ((Assert (m ∈ filter(d;[m, n))) BY
          ((BLemma `member_filter`  THENA Auto)
           THEN D 0
           THEN Try (Trivial)
           THEN BLemma `from-upto-member-nat`
           THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜filter(d;[m, n)) = L ∈ (ℕ List)⌝⋅ THENA Auto)
   THEN All Thin
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  m  <  n
5.  \mforall{}j:\mBbbN{}.  (m  <  j  {}\mRightarrow{}  (\muparrow{}(d  j))  {}\mRightarrow{}  (n  \mleq{}  j))
6.  \muparrow{}(d  m)
7.  (\mforall{}[x,y:\mBbbN{}].    (x  =  y)  supposing  ((y  \mmember{}  filter(d;[m,  n)))  and  (x  \mmember{}  filter(d;[m,  n)))))
      \mwedge{}  no\_repeats(\mBbbN{};filter(d;[m,  n)))
      \mwedge{}  0  <  ||filter(d;[m,  n))|| 
      supposing  ||filter(d;[m,  n))||  =  1
8.  \mforall{}[x,y:\mBbbN{}].    (x  =  y)  supposing  ((y  \mmember{}  filter(d;[m,  n)))  and  (x  \mmember{}  filter(d;[m,  n))))
9.  no\_repeats(\mBbbN{};filter(d;[m,  n)))
\mvdash{}  0  <  ||filter(d;[m,  n))||


By

---

Latex:
((Assert  (m  \mmember{}  filter(d;[m,  n)))  BY
                ((BLemma  `member\_filter`    THENA  Auto)
                  THEN  D  0
                  THEN  Try  (Trivial)
                  THEN  BLemma  `from-upto-member-nat`
                  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}filter(d;[m,  n))  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index