---

Step * of Lemma sq-all-large-and

∀[P,Q:ℕ ⟶ ℙ].  (∀large(n).{P[n]} ⇒ ∀large(n).{Q[n]} ⇒ ∀large(n).{P[n] ∧ Q[n]})
BY
{ ((Unfold `sq-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  `sq-all-large`  0  THEN  Auto')
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}imax(N;N1)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  FLemma  `imax\_lb`  [8]
  THEN  Auto)

---

Home Index