### Nuprl Lemma : zero_ann_a

`∀[a,b:ℤ].  (a * b) = 0 ∈ ℤ supposing (a = 0 ∈ ℤ) ∨ (b = 0 ∈ ℤ)`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` uall: `∀[x:A]. B[x]` or: `P ∨ Q` multiply: `n * m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` or: `P ∨ Q` prop: `ℙ` subtype_rel: `A ⊆r B` top: `Top`
Lemmas referenced :  zero-mul equal-wf-base int_subtype_base mul-commutes or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution unionElimination thin hypothesis sqequalRule extract_by_obid isectElimination hypothesisEquality natural_numberEquality hyp_replacement equalitySymmetry Error :applyLambdaEquality,  because_Cache baseApply closedConclusion baseClosed applyEquality lambdaEquality isect_memberEquality voidElimination voidEquality intEquality axiomEquality equalityTransitivity

Latex:
\mforall{}[a,b:\mBbbZ{}].    (a  *  b)  =  0  supposing  (a  =  0)  \mvee{}  (b  =  0)

Date html generated: 2016_10_21-AM-09_37_22
Last ObjectModification: 2016_07_12-AM-05_00_40

Theory : arithmetic

Home Index