Nuprl Lemma : eqmod_cancellation
∀m,x,a,b:ℤ. (CoPrime(x,m) ⇒ ((x * a) ≡ (x * b) mod m) ⇒ (a ≡ b mod m))
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
coprime: CoPrime(a,b),
all: ∀x:A. B[x],
implies: P ⇒ Q,
multiply: n * m,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
eqmod: a ≡ b mod m,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
subtract: n - m,
top: Top,
coprime: CoPrime(a,b)
Lemmas referenced :
eqmod_wf,
coprime_wf,
istype-int,
coprime_divides_prod,
subtract_wf,
mul-distributes,
istype-void,
minus-one-mul,
mul-commutes,
mul-swap,
gcd_p_sym
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
sqequalHypSubstitution,
Error :universeIsType,
cut,
introduction,
extract_by_obid,
isectElimination,
thin,
hypothesisEquality,
multiplyEquality,
hypothesis,
Error :inhabitedIsType,
dependent_functionElimination,
independent_functionElimination,
sqequalRule,
Error :isect_memberEquality_alt,
voidElimination,
because_Cache,
natural_numberEquality
Latex:
\mforall{}m,x,a,b:\mBbbZ{}. (CoPrime(x,m) {}\mRightarrow{} ((x * a) \mequiv{} (x * b) mod m) {}\mRightarrow{} (a \mequiv{} b mod m))
Date html generated:
2019_06_20-PM-02_24_33
Last ObjectModification:
2018_10_17-AM-10_43_36
Theory : num_thy_1
Home
Index