---

Step * of Lemma all-large-and

∀[P,Q:ℕ ⟶ ℙ].  (∀large(n).P[n] ⇒ ∀large(n).Q[n] ⇒ ∀large(n).P[n] ∧ Q[n])
BY
{ ((Unfold `all-large` 0 THEN Auto')
   THEN ExRepD
   THEN InstConcl [⌜imax(N;N1)⌝]⋅
   THEN Auto
   THEN (FLemma `imax_lb` [8] THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].    (\mforall{}large(n).P[n]  {}\mRightarrow{}  \mforall{}large(n).Q[n]  {}\mRightarrow{}  \mforall{}large(n).P[n]  \mwedge{}  Q[n])


By

---

Latex:
((Unfold  `all-large`  0  THEN  Auto')
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}imax(N;N1)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (FLemma  `imax\_lb`  [8]  THEN  Auto)\mcdot{})

---

Home Index