Nuprl Lemma : eqmod_refl
∀m,a:ℤ. (a ≡ a mod m)
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
all: ∀x:A. B[x],
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uimplies: b supposing a
Lemmas referenced :
eqmod_weakening,
istype-int
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_isectElimination,
hypothesis,
inhabitedIsType
Latex:
\mforall{}m,a:\mBbbZ{}. (a \mequiv{} a mod m)
Date html generated:
2020_05_19-PM-10_01_03
Last ObjectModification:
2019_12_31-PM-03_26_48
Theory : num_thy_1
Home
Index