### 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