### Nuprl Lemma : pos_mul_arg_bounds

`∀a,b:ℤ.  ((a * b) > 0 `⇐⇒` ((a > 0) ∧ (b > 0)) ∨ (a < 0 ∧ b < 0))`

Proof

Definitions occuring in Statement :  less_than: `a < b` gt: `i > j` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` and: `P ∧ Q` multiply: `n * m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` gt: `i > j` or: `P ∨ Q` cand: `A c∧ B` decidable: `Dec(P)` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` nat_plus: `ℕ+` squash: `↓T` label: `...\$L... t` true: `True` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  gt_wf or_wf less_than_wf int_trichot decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermMultiply_wf itermMinus_wf itermVar_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_mul_lemma int_term_value_minus_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf mul_cancel_in_lt mul_bounds_1b squash_wf true_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin multiplyEquality hypothesisEquality natural_numberEquality hypothesis productEquality intEquality dependent_functionElimination unionElimination inrFormation minusEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll dependent_set_memberEquality because_Cache equalitySymmetry hyp_replacement Error :applyLambdaEquality,  inlFormation productElimination applyEquality imageElimination equalityTransitivity imageMemberEquality baseClosed universeEquality independent_functionElimination

Latex:
\mforall{}a,b:\mBbbZ{}.    ((a  *  b)  >  0  \mLeftarrow{}{}\mRightarrow{}  ((a  >  0)  \mwedge{}  (b  >  0))  \mvee{}  (a  <  0  \mwedge{}  b  <  0))

Date html generated: 2016_10_21-AM-09_58_35
Last ObjectModification: 2016_07_12-AM-05_12_30

Theory : int_2

Home Index