Nuprl Lemma : mul_bounds_1b
∀[a,b:ℕ+]. 0 < a * b
Proof
Definitions occuring in Statement :
nat_plus: ℕ+,
less_than: a < b,
uall: ∀[x:A]. B[x],
multiply: n * m,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat_plus: ℕ+,
uimplies: b supposing a,
top: Top,
subtype_rel: A ⊆r B
Lemmas referenced :
member-less_than,
nat_plus_wf,
mul-commutes,
zero-mul,
mul_preserves_lt
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
hypothesis,
Error :inhabitedIsType,
hypothesisEquality,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
extract_by_obid,
natural_numberEquality,
multiplyEquality,
setElimination,
rename,
independent_isectElimination,
Error :universeIsType,
lemma_by_obid,
intEquality,
voidEquality,
voidElimination,
lambdaEquality,
applyEquality
Latex:
\mforall{}[a,b:\mBbbN{}\msupplus{}]. 0 < a * b
Date html generated:
2019_06_20-AM-11_26_43
Last ObjectModification:
2018_09_26-AM-10_58_39
Theory : arithmetic
Home
Index