---

Step * 1 1 1 1 1 of Lemma uniform-continuity-pi-search-prop2


1. P : ℕ ⟶ ℙ
2. m : ℤ
3. x : ℕ
4. ∃n:{x..(x + 0) + 1-}. P[n]
5. G : ∀m:ℕx + 0. Dec(P[m])
6. (x + 0) ≤ x
⊢ x + 0 ∈ {k:{x..(x + 0) + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..(x + 0) + 1-}. (P[m] ⇒ (k ≤ m)))} 
BY
{ (ExRepD
   THEN (D (-4) THENA Auto)
   THEN (Subst ⌜n ~ x⌝ (-3)⋅ THENA Auto)
   THEN (Subst ⌜x + 0 ~ x⌝ 0⋅ THENA Auto)
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  m  :  \mBbbZ{}
3.  x  :  \mBbbN{}
4.  \mexists{}n:\{x..(x  +  0)  +  1\msupminus{}\}.  P[n]
5.  G  :  \mforall{}m:\mBbbN{}x  +  0.  Dec(P[m])
6.  (x  +  0)  \mleq{}  x
\mvdash{}  x  +  0  \mmember{}  \{k:\{x..(x  +  0)  +  1\msupminus{}\}| 
                      P[k]  \mwedge{}  (\mforall{}m:\{x..k\msupminus{}\}.  (\mneg{}P[m]))  \mwedge{}  (\mforall{}m:\{x..(x  +  0)  +  1\msupminus{}\}.  (P[m]  {}\mRightarrow{}  (k  \mleq{}  m)))\} 


By

---

Latex:
(ExRepD
  THEN  (D  (-4)  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}n  \msim{}  x\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}x  +  0  \msim{}  x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index