Nuprl Lemma : eqmod_transitivity
∀m,a,b,c:ℤ. ((a ≡ b mod m) ⇒ (b ≡ c mod m) ⇒ (a ≡ c mod m))
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
all: ∀x:A. B[x],
implies: P ⇒ Q,
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,
subtract: n - m,
top: Top
Lemmas referenced :
istype-int,
subtract_wf,
divides_wf,
divisor_of_sum,
minus-one-mul,
add-associates,
istype-void,
add-swap,
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,
dependent_functionElimination,
independent_functionElimination,
Error :isect_memberEquality_alt,
voidElimination,
because_Cache,
multiplyEquality,
minusEquality,
natural_numberEquality
Latex:
\mforall{}m,a,b,c:\mBbbZ{}. ((a \mequiv{} b mod m) {}\mRightarrow{} (b \mequiv{} c mod m) {}\mRightarrow{} (a \mequiv{} c mod m))
Date html generated:
2019_06_20-PM-02_24_12
Last ObjectModification:
2019_01_17-AM-08_47_54
Theory : num_thy_1
Home
Index