Nuprl Lemma : prime-mul

x,y:ℤ.  (prime(x y)  ((x 1) ∨ (y 1)))


Proof




Definitions occuring in Statement :  prime: prime(a) assoced: b all: x:A. B[x] implies:  Q or: P ∨ Q multiply: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T and: P ∧ Q prop: uall: [x:A]. B[x] divides: a exists: x:A. B[x] subtype_rel: A ⊆B or: P ∨ Q guard: {T} iff: ⇐⇒ Q rev_implies:  Q int_nzero: -o nequal: a ≠ b ∈  not: ¬A uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top decidable: Dec(P)
Lemmas referenced :  prime_elim prime_wf equal-wf-base int_subtype_base assoced_wf assoced_elim mul_cancel_in_eq full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf itermMultiply_wf intformnot_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_formula_prop_not_lemma int_formula_prop_wf nequal_wf decidable__equal_int itermMinus_wf int_term_value_minus_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin multiplyEquality hypothesisEquality independent_functionElimination hypothesis productElimination isectElimination intEquality dependent_pairFormation sqequalRule baseApply closedConclusion baseClosed applyEquality because_Cache unionElimination inlFormation natural_numberEquality inrFormation dependent_set_memberEquality independent_isectElimination approximateComputation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation minusEquality

Latex:
\mforall{}x,y:\mBbbZ{}.    (prime(x  *  y)  {}\mRightarrow{}  ((x  \msim{}  1)  \mvee{}  (y  \msim{}  1)))



Date html generated: 2019_06_20-PM-02_23_08
Last ObjectModification: 2018_09_22-PM-05_25_11

Theory : num_thy_1


Home Index