Nuprl Lemma : rmul_preserves_rless
∀x,y,z:ℝ. ((r0 < y) ⇒ (x < z ⇐⇒ (x * y) < (z * y)))
Proof
Definitions occuring in Statement :
rless: x < y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
rneq: x ≠ y,
guard: {T},
or: P ∨ Q,
uimplies: b supposing a
Lemmas referenced :
rless_wf,
rmul_wf,
int-to-real_wf,
real_wf,
rmul_functionality_wrt_rless,
rinv_wf2,
rinv-positive,
rless_functionality,
req_transitivity,
req_inversion,
rmul-assoc,
rmul_functionality,
req_weakening,
rmul-rinv,
rmul-one-both
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
independent_pairFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
natural_numberEquality,
dependent_functionElimination,
independent_functionElimination,
sqequalRule,
inrFormation,
because_Cache,
independent_isectElimination,
productElimination
Latex:
\mforall{}x,y,z:\mBbbR{}. ((r0 < y) {}\mRightarrow{} (x < z \mLeftarrow{}{}\mRightarrow{} (x * y) < (z * y)))
Date html generated:
2016_05_18-AM-07_12_23
Last ObjectModification:
2015_12_28-AM-00_40_30
Theory : reals
Home
Index