### Nuprl Lemma : absval-diff-product-bound2

`∀u,v,x,y:ℤ.  (|(u * v) - x * y| ≤ ((|u| * |v - y|) + (|y| * |u - x|)))`

Proof

Definitions occuring in Statement :  absval: `|i|` le: `A ≤ B` all: `∀x:A. B[x]` multiply: `n * m` subtract: `n - m` add: `n + m` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` top: `Top` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` rev_uimplies: `rev_uimplies(P;Q)` ge: `i ≥ j ` subtract: `n - m`
Lemmas referenced :  le_wf squash_wf true_wf absval_wf subtract_wf add_functionality_wrt_eq absval_mul subtype_rel_self iff_weakening_equal istype-int istype-void decidable__le full-omega-unsat intformnot_wf intformle_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf le_functionality le_weakening int-triangle-inequality mul-distributes add-associates minus-one-mul mul-swap mul-commutes add-commutes add-mul-special zero-mul zero-add
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut applyEquality thin Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  because_Cache multiplyEquality setElimination rename Error :inhabitedIsType,  sqequalRule independent_isectElimination natural_numberEquality imageMemberEquality baseClosed instantiate universeEquality productElimination independent_functionElimination addEquality Error :isect_memberEquality_alt,  voidElimination minusEquality dependent_functionElimination unionElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality

Latex:
\mforall{}u,v,x,y:\mBbbZ{}.    (|(u  *  v)  -  x  *  y|  \mleq{}  ((|u|  *  |v  -  y|)  +  (|y|  *  |u  -  x|)))

Date html generated: 2019_06_20-PM-01_13_48
Last ObjectModification: 2019_02_14-PM-00_03_12

Theory : int_2

Home Index