Nuprl Lemma : int_entire
∀a,b:ℤ. (a = 0 ∈ ℤ) ∨ (b = 0 ∈ ℤ) supposing (a * b) = 0 ∈ ℤ
Proof
Definitions occuring in Statement :
uimplies: b supposing a,
all: ∀x:A. B[x],
or: P ∨ Q,
multiply: n * m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
decidable: Dec(P),
or: P ∨ Q,
int_nzero: ℤ-o,
nequal: a ≠ b ∈ T ,
top: Top
Lemmas referenced :
equal-wf-base,
int_subtype_base,
decidable__int_equal,
mul_cancel_in_eq,
nequal_wf,
mul-commutes,
zero-mul
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
Error :isect_memberFormation_alt,
cut,
introduction,
axiomEquality,
hypothesis,
thin,
rename,
Error :universeIsType,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
intEquality,
sqequalRule,
baseApply,
closedConclusion,
baseClosed,
hypothesisEquality,
applyEquality,
because_Cache,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
unionElimination,
inrFormation,
inlFormation,
dependent_set_memberEquality,
natural_numberEquality,
independent_isectElimination,
lambdaEquality,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}a,b:\mBbbZ{}. (a = 0) \mvee{} (b = 0) supposing (a * b) = 0
Date html generated:
2019_06_20-AM-11_26_35
Last ObjectModification:
2018_09_26-AM-10_58_31
Theory : arithmetic
Home
Index