Nuprl Lemma : stamps-example

n:ℕ. ∃i:ℕ(∃j:ℕ [((n 8) ((3 i) (5 j)) ∈ ℤ)])


Proof




Definitions occuring in Statement :  nat: all: x:A. B[x] sq_exists: x:A [B[x]] exists: x:A. B[x] multiply: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q exists: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: so_apply: x[s] uimplies: supposing a sq_exists: x:A [B[x]] prop: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A top: Top decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) guard: {T} subtract: m true: True sq_stable: SqStable(P) squash: T sq_type: SQType(T) nat_plus: + less_than: a < b adjust_div: adjust_div(b;a)
Lemmas referenced :  nat_wf sq_exists_wf equal-wf-base int_subtype_base set_subtype_base le_wf istype-int less_than_wf primrec-wf2 exists_wf istype-false zero-add mul-commutes istype-void sq_stable__equal decidable__le subtract_wf set-value-type equal_wf int-value-type not-le-2 le_antisymmetry_iff condition-implies-le minus-add minus-minus minus-one-mul add-swap minus-one-mul-top add-commutes add_functionality_wrt_le add-associates le-add-cancel sq_stable__le add-zero add-mul-special two-mul mul-distributes-right zero-mul one-mul subtype_base_sq decidable__int_equal not-equal-2 mul-associates mul-distributes le-add-cancel2 nat_properties less-iff-le le_reflexive omega-shadow mul-swap divide-le squash_wf true_wf minus-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut thin rename setElimination sqequalRule Error :productIsType,  Error :universeIsType,  introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination Error :lambdaEquality_alt,  intEquality baseApply closedConclusion baseClosed hypothesisEquality applyEquality natural_numberEquality Error :inhabitedIsType,  independent_isectElimination Error :setIsType,  because_Cache Error :dependent_set_memberEquality_alt,  independent_pairFormation Error :isect_memberEquality_alt,  voidElimination Error :equalityIsType4,  Error :dependent_pairFormation_alt,  Error :dependent_set_memberFormation_alt,  productElimination equalityTransitivity equalitySymmetry dependent_functionElimination unionElimination cutEval Error :equalityIsType1,  addEquality independent_functionElimination minusEquality imageMemberEquality imageElimination multiplyEquality promote_hyp instantiate cumulativity hyp_replacement

Latex:
\mforall{}n:\mBbbN{}.  \mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((n  +  8)  =  ((3  *  i)  +  (5  *  j)))])



Date html generated: 2019_06_20-PM-00_26_09
Last ObjectModification: 2018_10_09-AM-09_30_44

Theory : int_1


Home Index