### Nuprl Lemma : mul_positive_iff

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

Proof

Definitions occuring in Statement :  less_than: `a < b` 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` decidable: `Dec(P)` or: `P ∨ Q` cand: `A c∧ B` not: `¬A` false: `False` nat_plus: `ℕ+` uimplies: `b supposing a` uiff: `uiff(P;Q)` subtract: `n - m` subtype_rel: `A ⊆r B` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` sq_type: `SQType(T)` guard: `{T}`
Lemmas referenced :  less_than_wf or_wf decidable__lt less-trichotomy mul_preserves_lt less-iff-le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top mul-commutes zero-mul add_functionality_wrt_le add-associates add-zero add-commutes le-add-cancel subtype_base_sq int_subtype_base minus-zero mul_positive add_functionality_wrt_lt le_reflexive add-inverse mul-associates mul-swap one-mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality multiplyEquality hypothesisEquality hypothesis productEquality intEquality dependent_functionElimination unionElimination because_Cache inlFormation independent_functionElimination voidElimination dependent_set_memberEquality independent_isectElimination productElimination addEquality sqequalRule applyEquality lambdaEquality isect_memberEquality voidEquality minusEquality instantiate cumulativity equalityTransitivity equalitySymmetry inrFormation

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

Date html generated: 2019_06_20-AM-11_23_27
Last ObjectModification: 2018_08_20-AM-11_00_40

Theory : arithmetic

Home Index