---

Step * 1 2 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. [%5] : ∃n:ℕ. P[n]
6. P[mu-ge(d;0)]
7. ∀[i:ℕmu-ge(d;0)]. (¬P[i])
8. mu-ge(d;0) ∈ {0...}
⊢ ∀i:ℕ. ¬P[i] supposing i < mu-ge(d;0)
BY
{ TACTIC:RepeatFor 2 ((D 0 THENA Auto)) }

1
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]

---

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.  [\%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...\}
\mvdash{}  \mforall{}i:\mBbbN{}.  \mneg{}P[i]  supposing  i  <  mu-ge(d;0)


By

---

Latex:
TACTIC:RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index