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