Nuprl Lemma : multiply_com_int_mod

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


Proof




Definitions occuring in Statement :  int_mod: _n uall: [x:A]. B[x] multiply: m int: equal: t ∈ T
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 mul-commutes eqmod_refl eqmod_functionality_wrt_eqmod multiply_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 isect_memberEquality_alt axiomEquality isectIsTypeImplies intEquality lambdaEquality_alt independent_isectElimination multiplyEquality Error :memTop

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



Date html generated: 2020_05_19-PM-10_02_55
Last ObjectModification: 2020_01_01-AM-10_07_07

Theory : num_thy_1


Home Index