### Nuprl Lemma : not-not-all-int_seg-shift

`∀a,b:ℤ. ∀P:{a..b-} ⟶ ℙ.  ((∀i:{a..b-}. (¬¬P[i])) `` (¬¬(∀i:{a..b-}. P[i])))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` not: `¬A` or: `P ∨ Q` false: `False` uall: `∀[x:A]. B[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  not-not-all-int_seg-xmiddle int_seg_wf istype-void subtype_rel_self istype-int
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination unionElimination voidElimination universeIsType isectElimination sqequalRule functionIsType unionIsType applyEquality because_Cache instantiate universeEquality inhabitedIsType

Latex:
\mforall{}a,b:\mBbbZ{}.  \mforall{}P:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}.    ((\mforall{}i:\{a..b\msupminus{}\}.  (\mneg{}\mneg{}P[i]))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mforall{}i:\{a..b\msupminus{}\}.  P[i])))

Date html generated: 2020_05_19-PM-09_36_12
Last ObjectModification: 2019_11_04-PM-02_02_56

Theory : int_1

Home Index