Nuprl Lemma : r-triangle-inequality

[x,y:ℝ].  (|x y| ≤ (|x| |y|))

This theorem is one of freek's list of 100 theorems


Definitions occuring in Statement :  rleq: x ≤ y rabs: |x| radd: b real: uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rleq: x ≤ y iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q rnonneg: rnonneg(x) all: x:A. B[x] le: A ≤ B not: ¬A false: False subtype_rel: A ⊆B real: prop: rsub: y rabs: |x| nat: reg-seq-add: reg-seq-add(x;y) rminus: -(x) rnonneg2: rnonneg2(x) exists: x:A. B[x] nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True so_lambda: λ2x.t[x] int_upper: {i...} guard: {T} uimplies: supposing a so_apply: x[s] decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) rev_uimplies: rev_uimplies(P;Q) ge: i ≥ 
Lemmas referenced :  int-triangle-inequality minus_functionality_wrt_le multiply_functionality_wrt_le le_weakening le_functionality int_term_value_mul_lemma int_formula_prop_and_lemma itermMultiply_wf intformand_wf int_formula_prop_wf int_term_value_minus_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma itermMinus_wf itermVar_wf itermAdd_wf itermConstant_wf intformle_wf intformnot_wf satisfiable-full-omega-tt decidable__le nat_plus_properties int_upper_properties nat_plus_subtype_nat le-add-cancel zero-add add-commutes add_functionality_wrt_le not-lt-2 false_wf decidable__lt less_than_transitivity1 le_wf all_wf int_upper_wf less_than_wf bdd-diff_weakening reg-seq-add_functionality_wrt_bdd-diff reg-seq-add_wf rabs_functionality_wrt_bdd-diff nat_wf absval_wf rminus_functionality_wrt_bdd-diff radd-bdd-diff rminus_wf rnonneg2_functionality nat_plus_wf real_wf less_than'_wf rabs_wf radd_wf rsub_wf rnonneg-iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination independent_functionElimination sqequalRule lambdaEquality dependent_functionElimination independent_pairEquality because_Cache applyEquality setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination addEquality lambdaFormation dependent_pairFormation dependent_set_memberEquality independent_pairFormation imageMemberEquality baseClosed multiplyEquality independent_isectElimination unionElimination voidEquality intEquality int_eqEquality computeAll

\mforall{}[x,y:\mBbbR{}].    (|x  +  y|  \mleq{}  (|x|  +  |y|))

Date html generated: 2016_05_18-AM-07_14_23
Last ObjectModification: 2016_01_17-AM-01_55_03

Theory : reals

Home Index