### Nuprl Lemma : int-prod_wf_absval_1

`∀[n:ℕ]. ∀[f:ℕn ⟶ {s:ℤ| |s| = 1 ∈ ℤ} ].  (Π(f[x] | x < n) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )`

Proof

Definitions occuring in Statement :  int-prod: `Π(f[x] | x < k)` absval: `|i|` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` int_seg: `{i..j-}` sq_type: `SQType(T)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}` uimplies: `b supposing a` true: `True` squash: `↓T` so_apply: `x[s]` all: `∀x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` prop: `ℙ` nat: `ℕ` subtype_rel: `A ⊆r B` int-prod: `Π(f[x] | x < k)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  int_formula_prop_wf int_term_value_constant_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermConstant_wf itermMultiply_wf intformeq_wf intformnot_wf full-omega-unsat decidable__equal_int subtype_base_sq iff_weakening_equal subtype_rel_self absval_mul istype-universe true_wf squash_wf istype-nat int_seg_wf istype-int equal-wf-base int_subtype_base istype-le istype-void absval_pos absval_wf equal_wf primrec_wf
Rules used in proof :  Error :dependent_pairFormation_alt,  approximateComputation unionElimination applyLambdaEquality cumulativity promote_hyp productElimination independent_isectElimination imageMemberEquality universeEquality instantiate imageElimination Error :isectIsTypeImplies,  Error :isect_memberEquality_alt,  Error :universeIsType,  Error :functionIsType,  axiomEquality Error :setIsType,  independent_functionElimination dependent_functionElimination because_Cache multiplyEquality sqequalBase baseClosed baseApply Error :equalityIstype,  voidElimination Error :lambdaFormation_alt,  independent_pairFormation Error :dependent_set_memberEquality_alt,  natural_numberEquality equalitySymmetry equalityTransitivity Error :inhabitedIsType,  rename setElimination Error :lambdaEquality_alt,  applyEquality hypothesis hypothesisEquality intEquality setEquality closedConclusion thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction Error :isect_memberFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \{s:\mBbbZ{}|  |s|  =  1\}  ].    (\mPi{}(f[x]  |  x  <  n)  \mmember{}  \{s:\mBbbZ{}|  |s|  =  1\}  )

Date html generated: 2019_06_20-PM-01_18_30
Last ObjectModification: 2019_06_19-AM-10_34_48

Theory : int_2

Home Index