Nuprl Lemma : multiply_functionality_wrt_eqmod
∀m,a,a',b,b':ℤ. ((a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ ((a * b) ≡ (a' * b') mod m))
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
all: ∀x:A. B[x],
implies: P ⇒ Q,
multiply: n * m,
int: ℤ
Definitions unfolded in proof :
prop: ℙ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
eqmod: a ≡ b mod m,
top: Top,
subtract: n - m
Lemmas referenced :
istype-int,
subtract_wf,
divides_wf,
divisor_of_mul,
divisor_of_sum,
istype-void,
mul-distributes-right,
add-associates,
minus-one-mul,
mul-associates,
mul-commutes,
add-commutes,
add-mul-special,
zero-mul,
zero-add
Rules used in proof :
Error :inhabitedIsType,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
Error :universeIsType,
Error :lambdaFormation_alt,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution,
because_Cache,
independent_functionElimination,
dependent_functionElimination,
multiplyEquality,
Error :isect_memberEquality_alt,
voidElimination,
minusEquality,
natural_numberEquality
Latex:
\mforall{}m,a,a',b,b':\mBbbZ{}. ((a \mequiv{} a' mod m) {}\mRightarrow{} (b \mequiv{} b' mod m) {}\mRightarrow{} ((a * b) \mequiv{} (a' * b') mod m))
Date html generated:
2019_06_20-PM-02_24_30
Last ObjectModification:
2019_01_15-PM-03_27_14
Theory : num_thy_1
Home
Index