Nuprl Lemma : add_wf_int_mod

[n:ℤ]. ∀[x,y:ℤ_n].  (x y ∈ ℤ_n)


Proof




Definitions occuring in Statement :  int_mod: _n uall: [x:A]. B[x] member: t ∈ T add: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_mod: _n quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] implies:  Q prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  eqmod_wf int_mod_wf istype-int quotient-member-eq eqmod_equiv_rel eqmod_refl eqmod_functionality_wrt_eqmod add_functionality_wrt_eqmod eqmod_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality because_Cache hypothesis sqequalRule pertypeElimination promote_hyp thin productElimination equalityTransitivity equalitySymmetry inhabitedIsType lambdaFormation_alt rename universeIsType extract_by_obid isectElimination hypothesisEquality equalityIstype dependent_functionElimination independent_functionElimination productIsType sqequalBase axiomEquality isect_memberEquality_alt isectIsTypeImplies intEquality lambdaEquality_alt independent_isectElimination addEquality

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[x,y:\mBbbZ{}\_n].    (x  +  y  \mmember{}  \mBbbZ{}\_n)



Date html generated: 2020_05_19-PM-10_02_34
Last ObjectModification: 2020_01_01-AM-10_08_12

Theory : num_thy_1


Home Index