Nuprl Lemma : modulus-equal-iff-eqmod
∀x,y:ℤ. ∀m:ℕ+. ((x mod m) = (y mod m) ∈ ℤ ⇐⇒ x ≡ y mod m)
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
modulus: a mod n,
nat_plus: ℕ+,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
eqmod: a ≡ b mod m
Lemmas referenced :
modulus-equal
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
hypothesis
Latex:
\mforall{}x,y:\mBbbZ{}. \mforall{}m:\mBbbN{}\msupplus{}. ((x mod m) = (y mod m) \mLeftarrow{}{}\mRightarrow{} x \mequiv{} y mod m)
Date html generated:
2016_05_14-PM-04_22_57
Last ObjectModification:
2015_12_26-PM-08_18_41
Theory : num_thy_1
Home
Index