### Nuprl Lemma : not-all-int_seg2

`∀i,j:ℤ.  ∀[P,Q:{i..j-} ⟶ ℙ].  ((∀x:{i..j-}. (P[x] ∨ Q[x])) `` (¬(∀x:{i..j-}. P[x])) `` (∃x:{i..j-}. Q[x]))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  le: `A ≤ B` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` label: `...\$L... t` guard: `{T}` decidable: `Dec(P)` top: `Top` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` not: `¬A` nat: `ℕ` or: `P ∨ Q` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` so_lambda: `λ2x.t[x]` prop: `ℙ` member: `t ∈ T` implies: `P `` Q` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]`
Lemmas referenced :  le_wf iff_weakening_equal int_formula_prop_eq_lemma intformeq_wf decidable__equal_int subtype_rel_self int_seg_subtype subtype_rel_dep_function lelt_wf decidable__le int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf decidable__lt int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma itermConstant_wf itermAdd_wf intformle_wf itermVar_wf intformless_wf intformand_wf satisfiable-full-omega-tt int_seg_properties nat_wf primrec-wf2 set_wf exists_wf uall_wf subtract_wf less_than_wf or_wf int_seg_wf all_wf not_wf
Rules used in proof :  equalitySymmetry equalityTransitivity dependent_set_memberEquality unionElimination computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality dependent_functionElimination int_eqEquality dependent_pairFormation independent_isectElimination productElimination independent_functionElimination natural_numberEquality addEquality because_Cache instantiate setElimination rename intEquality universeEquality cumulativity functionEquality functionExtensionality applyEquality lambdaEquality sqequalRule hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut isect_memberFormation lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}i,j:\mBbbZ{}.
\mforall{}[P,Q:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:\{i..j\msupminus{}\}.  (P[x]  \mvee{}  Q[x]))  {}\mRightarrow{}  (\mneg{}(\mforall{}x:\{i..j\msupminus{}\}.  P[x]))  {}\mRightarrow{}  (\mexists{}x:\{i..j\msupminus{}\}.  Q[x]))

Date html generated: 2016_10_21-AM-09_59_24
Last ObjectModification: 2016_09_26-PM-01_35_50

Theory : int_2

Home Index