Nuprl Lemma : subtype_rel_int_mod
∀[a,b:ℤ]. ((a | b) ⇒ (ℤ_b ⊆r ℤ_a))
Proof
Definitions occuring in Statement :
int_mod: ℤ_n,
divides: b | a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
int_mod: ℤ_n,
quotient: x,y:A//B[x; y],
and: P ∧ Q,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
all: ∀x:A. B[x],
guard: {T}
Lemmas referenced :
divides_wf,
int_mod_wf,
quotient-member-eq,
eqmod_wf,
eqmod_equiv_rel,
equal-wf-base,
eqmod-divides-implies
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
sqequalRule,
lambdaEquality,
dependent_functionElimination,
axiomEquality,
intEquality,
isect_memberEquality,
because_Cache,
pointwiseFunctionalityForEquality,
pertypeElimination,
productElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
productEquality
Latex:
\mforall{}[a,b:\mBbbZ{}]. ((a | b) {}\mRightarrow{} (\mBbbZ{}\_b \msubseteq{}r \mBbbZ{}\_a))
Date html generated:
2016_05_14-PM-09_27_12
Last ObjectModification:
2015_12_26-PM-08_01_21
Theory : num_thy_1
Home
Index