Nuprl Lemma : mul_preserves_le
∀[a,b:ℤ]. ∀[n:ℕ]. (n * a) ≤ (n * b) supposing a ≤ b
Proof
Definitions occuring in Statement :
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
le: A ≤ B,
multiply: n * m,
int: ℤ
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat: ℕ,
prop: ℙ,
uimplies: b supposing a,
le: A ≤ B,
and: P ∧ Q,
not: ¬A,
implies: P ⇒ Q,
false: False,
all: ∀x:A. B[x],
uiff: uiff(P;Q),
ge: i ≥ j ,
or: P ∨ Q,
subtype_rel: A ⊆r B,
guard: {T},
top: Top,
sq_type: SQType(T),
less_than': less_than'(a;b)
Lemmas referenced :
less_than'_wf,
le_wf,
nat_wf,
nat_properties,
le-iff-less-or-equal,
equal-wf-base,
int_subtype_base,
less_than_wf,
add_functionality_wrt_lt,
le_reflexive,
minus-one-mul,
add-mul-special,
add-commutes,
zero-mul,
mul_positive,
minus-one-mul-top,
mul-distributes,
add-associates,
mul-commutes,
mul-swap,
zero-add,
subtype_base_sq,
false_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
multiplyEquality,
setElimination,
rename,
hypothesisEquality,
hypothesis,
because_Cache,
intEquality,
isect_memberFormation,
sqequalRule,
productElimination,
independent_pairEquality,
lambdaEquality,
dependent_functionElimination,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
voidElimination,
natural_numberEquality,
independent_isectElimination,
unionElimination,
inlFormation,
baseApply,
closedConclusion,
baseClosed,
applyEquality,
inrFormation,
minusEquality,
voidEquality,
addEquality,
independent_functionElimination,
instantiate,
cumulativity,
independent_pairFormation,
lambdaFormation
Latex:
\mforall{}[a,b:\mBbbZ{}]. \mforall{}[n:\mBbbN{}]. (n * a) \mleq{} (n * b) supposing a \mleq{} b
Date html generated:
2019_06_20-AM-11_23_18
Last ObjectModification:
2018_08_17-PM-00_10_56
Theory : arithmetic
Home
Index