Nuprl Lemma : rminus-nonneg

[x:ℝ]. (x r0) supposing (rnonneg(-(x)) and rnonneg(x))


Definitions occuring in Statement :  rnonneg: rnonneg(x) req: y rminus: -(x) int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rminus: -(x) rnonneg: rnonneg(x) req: y all: x:A. B[x] int-to-real: r(n) implies:  Q prop: subtype_rel: A ⊆B real: nat_plus: + top: Top bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q less_than: a < b less_than': less_than'(a;b) true: True squash: T not: ¬A false: False le: A ≤ B decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb ifthenelse: if then else fi  assert: b subtract: m
Lemmas referenced :  nat_plus_wf req_witness int-to-real_wf rnonneg_wf rminus_wf real_wf absval_unfold lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf nat_plus_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf itermConstant_wf itermMinus_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_constant_lemma int_term_value_minus_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot minus-one-mul mul-associates mul-commutes zero-mul add-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule lambdaFormation extract_by_obid hypothesis isectElimination thin hypothesisEquality natural_numberEquality independent_functionElimination applyEquality lambdaEquality setElimination rename isect_memberEquality because_Cache equalityTransitivity equalitySymmetry multiplyEquality voidElimination voidEquality dependent_functionElimination minusEquality unionElimination equalityElimination productElimination independent_isectElimination lessCases sqequalAxiom independent_pairFormation imageMemberEquality baseClosed imageElimination dependent_set_memberEquality dependent_pairFormation int_eqEquality intEquality computeAll promote_hyp instantiate cumulativity

\mforall{}[x:\mBbbR{}].  (x  =  r0)  supposing  (rnonneg(-(x))  and  rnonneg(x))

Date html generated: 2017_10_03-AM-08_24_15
Last ObjectModification: 2017_07_28-AM-07_23_13

Theory : reals

Home Index