Nuprl Lemma : rabs-rmul-rleq

[x,y,a,b:ℝ].  (|x y| ≤ (a b)) supposing ((|y| ≤ b) and (|x| ≤ a))


Definitions occuring in Statement :  rleq: x ≤ y rabs: |x| rmul: b real: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y guard: {T} rleq: x ≤ y rnonneg: rnonneg(x) all: x:A. B[x] le: A ≤ B and: P ∧ Q prop: uiff: uiff(P;Q) or: P ∨ Q cand: c∧ B req_int_terms: t1 ≡ t2 false: False implies:  Q not: ¬A

\mforall{}[x,y,a,b:\mBbbR{}].    (|x  *  y|  \mleq{}  (a  *  b))  supposing  ((|y|  \mleq{}  b)  and  (|x|  \mleq{}  a))

Date html generated: 2020_05_20-AM-10_57_56
Last ObjectModification: 2020_01_06-PM-00_26_57

Theory : reals

Home Index