### Nuprl Lemma : rneq-zero

x:ℝ(x ≠ r0 ⇐⇒ rpositive(x) ∨ rpositive(-(x)))

Proof

Definitions occuring in Statement :  rneq: x ≠ y rpositive: rpositive(x) rminus: -(x) int-to-real: r(n) real: all: x:A. B[x] iff: ⇐⇒ Q or: P ∨ Q natural_number: \$n
Definitions unfolded in proof :  rminus: -(x) rpositive: rpositive(x) int-to-real: r(n) rneq: x ≠ y rless: x < y all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q or: P ∨ Q guard: {T} sq_exists: x:{A| B[x]} member: t ∈ T uall: [x:A]. B[x] nat_plus: + real: prop: decidable: Dec(P) false: False less_than: a < b squash: T uiff: uiff(P;Q) uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A top: Top so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q
Lemmas referenced :  real_wf minus-is-int-iff or_wf nat_plus_wf sq_exists_wf false_wf int_formula_prop_wf int_term_value_mul_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_minus_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermMultiply_wf itermAdd_wf itermVar_wf itermMinus_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt add-is-int-iff less_than_wf decidable__lt nat_plus_properties
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation independent_pairFormation sqequalHypSubstitution unionElimination thin cut hypothesis inrFormation setElimination rename introduction dependent_set_memberEquality hypothesisEquality lemma_by_obid isectElimination dependent_functionElimination natural_numberEquality minusEquality applyEquality pointwiseFunctionality equalityTransitivity equalitySymmetry promote_hyp imageElimination productElimination baseApply closedConclusion baseClosed independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll inlFormation addEquality multiplyEquality

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  \mLeftarrow{}{}\mRightarrow{}  rpositive(x)  \mvee{}  rpositive(-(x)))

Date html generated: 2016_05_18-AM-07_10_38
Last ObjectModification: 2016_01_17-AM-01_51_20

Theory : reals

Home Index