Nuprl Lemma : mul_wf_nzero

[a,b:ℤ-o].  (a b ∈ ℤ-o)


Proof




Definitions occuring in Statement :  int_nzero: -o uall: [x:A]. B[x] member: t ∈ T multiply: m
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_nzero: -o uimplies: supposing a nequal: a ≠ b ∈  not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False all: x:A. B[x] top: Top and: P ∧ Q prop:
Lemmas referenced :  int_nzero_wf nequal_wf equal_wf int_formula_prop_wf int_formula_prop_not_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformnot_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt int_nzero_properties int_entire_a
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality multiplyEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality lemma_by_obid isectElimination independent_isectElimination hypothesis lambdaFormation natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll axiomEquality equalityTransitivity equalitySymmetry because_Cache

Latex:
\mforall{}[a,b:\mBbbZ{}\msupminus{}\msupzero{}].    (a  *  b  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{})



Date html generated: 2016_05_14-PM-04_27_30
Last ObjectModification: 2016_01_14-PM-11_34_58

Theory : num_thy_1


Home Index