Nuprl Lemma : int_entire_a

[a,b:ℤ].  (a b ≠ 0) supposing (b ≠ and a ≠ 0)


Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] nequal: a ≠ b ∈  multiply: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a nequal: a ≠ b ∈  not: ¬A implies:  Q false: False prop: subtype_rel: A ⊆B all: x:A. B[x] decidable: Dec(P) or: P ∨ Q subtract: m sq_type: SQType(T) guard: {T}
Lemmas referenced :  equal-wf-base int_subtype_base nequal_wf decidable__int_equal int_entire subtract_wf minus-zero zero-add add-zero subtype_base_sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin sqequalHypSubstitution hypothesis independent_functionElimination voidElimination extract_by_obid isectElimination intEquality sqequalRule baseApply closedConclusion baseClosed hypothesisEquality applyEquality because_Cache lambdaEquality dependent_functionElimination natural_numberEquality isect_memberEquality equalityTransitivity equalitySymmetry multiplyEquality unionElimination independent_isectElimination addEquality instantiate cumulativity

\mforall{}[a,b:\mBbbZ{}].    (a  *  b  \mneq{}  0)  supposing  (b  \mneq{}  0  and  a  \mneq{}  0)

Date html generated: 2017_04_14-AM-07_20_33
Last ObjectModification: 2017_02_27-PM-02_53_46

Theory : arithmetic

Home Index