---

Step * 1 2 1 of Lemma mu-property2


1. ∀[P:{0...} ⟶ ℙ]. ∀d:∀n:{0...}. Dec(P[n]). {P[mu-ge(d;0)] ∧ (∀[i:ℕmu-ge(d;0)]. (¬P[i]))} supposing ∃m:{0...}. P[m]
2. P : ℕ ⟶ ℙ
3. ∀d:∀n:{0...}. Dec(P[n]). {P[mu-ge(d;0)] ∧ (∀[i:ℕmu-ge(d;0)]. (¬P[i]))} supposing ∃m:{0...}. P[m]
4. d : ∀n:ℕ. Dec(P[n])
5. ∃n:ℕ. P[n]
6. P[mu-ge(d;0)]
7. ∀[i:ℕmu-ge(d;0)]. (¬P[i])
8. mu-ge(d;0) ∈ {0...}
9. i : ℕ
10. i < mu-ge(d;0)
⊢ ¬P[i]
BY
{ TACTIC:(BHyp -4 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[P:\{0...\}  {}\mrightarrow{}  \mBbbP{}]
          \mforall{}d:\mforall{}n:\{0...\}.  Dec(P[n])
              \{P[mu-ge(d;0)]  \mwedge{}  (\mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i]))\}  supposing  \mexists{}m:\{0...\}.  P[m]
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}d:\mforall{}n:\{0...\}.  Dec(P[n]).  \{P[mu-ge(d;0)]  \mwedge{}  (\mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i]))\}  supposing  \mexists{}m:\{0...\}.  P[m]
4.  d  :  \mforall{}n:\mBbbN{}.  Dec(P[n])
5.  \mexists{}n:\mBbbN{}.  P[n]
6.  P[mu-ge(d;0)]
7.  \mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i])
8.  mu-ge(d;0)  \mmember{}  \{0...\}
9.  i  :  \mBbbN{}
10.  i  <  mu-ge(d;0)
\mvdash{}  \mneg{}P[i]


By

---

Latex:
TACTIC:(BHyp  -4  THEN  Auto)

---

Home Index