Nuprl Lemma : zero_ann_b
∀[a,b:ℤ]. (¬(a = 0 ∈ ℤ)) ∧ (¬(b = 0 ∈ ℤ)) supposing ¬((a * b) = 0 ∈ ℤ)
Proof
Definitions occuring in Statement :
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
and: P ∧ Q,
multiply: n * m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
not: ¬A,
implies: P ⇒ Q,
false: False,
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
prop: ℙ,
uimplies: b supposing a,
and: P ∧ Q,
top: Top
Lemmas referenced :
equal-wf-base,
int_subtype_base,
not_wf,
zero-mul,
mul-commutes
Rules used in proof :
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
independent_functionElimination,
thin,
voidElimination,
cut,
introduction,
extract_by_obid,
isectElimination,
intEquality,
hypothesisEquality,
applyEquality,
hypothesis,
sqequalRule,
baseClosed,
because_Cache,
baseApply,
closedConclusion,
isect_memberFormation,
independent_pairFormation,
lambdaFormation,
productElimination,
independent_pairEquality,
lambdaEquality,
dependent_functionElimination,
isect_memberEquality,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
hyp_replacement,
Error :applyLambdaEquality,
voidEquality
Latex:
\mforall{}[a,b:\mBbbZ{}]. (\mneg{}(a = 0)) \mwedge{} (\mneg{}(b = 0)) supposing \mneg{}((a * b) = 0)
Date html generated:
2016_10_21-AM-09_37_25
Last ObjectModification:
2016_07_12-AM-05_00_44
Theory : arithmetic
Home
Index