---

Step * 1 1 of Lemma mu-property2

.....antecedent..... 
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])
⊢ ∃m:{0...}. (↑isl(d m))
BY
{ TACTIC:ParallelOp -3 }

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 : ℕ
6. P[n]
7. P[mu-ge(d;0)]
8. ∀[i:ℕmu-ge(d;0)]. (¬P[i])
⊢ ↑isl(d n)

---

Latex:

---

Latex:
.....antecedent..... 
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])
\mvdash{}  \mexists{}m:\{0...\}.  (\muparrow{}isl(d  m))


By

---

Latex:
TACTIC:ParallelOp  -3

---

Home Index