### Nuprl Lemma : eqmod_equiv_rel

`∀n:ℤ. EquivRel(ℤ;x,y.x ≡ y mod n)`

Proof

Definitions occuring in Statement :  eqmod: `a ≡ b mod m` equiv_rel: `EquivRel(T;x,y.E[x; y])` all: `∀x:A. B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` member: `t ∈ T` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` guard: `{T}` uall: `∀[x:A]. B[x]` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` uimplies: `b supposing a`
Lemmas referenced :  eqmod_inversion eqmod_wf eqmod_transitivity istype-int eqmod_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  independent_pairFormation Error :inhabitedIsType,  hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache independent_functionElimination hypothesis Error :universeIsType,  isectElimination independent_isectElimination

Latex:
\mforall{}n:\mBbbZ{}.  EquivRel(\mBbbZ{};x,y.x  \mequiv{}  y  mod  n)

Date html generated: 2019_06_20-PM-02_24_24
Last ObjectModification: 2018_10_03-AM-10_23_43

Theory : num_thy_1

Home Index