Nuprl Lemma : int-rmul-is-positive
∀k:ℤ. ∀y:ℝ. (r0 < k * y ⇐⇒ (0 < k ∧ (r0 < y)) ∨ (k < 0 ∧ (y < r0)))
Proof
Definitions occuring in Statement :
rless: x < y,
int-rmul: k1 * a,
int-to-real: r(n),
real: ℝ,
less_than: a < b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
uimplies: b supposing a,
or: P ∨ Q,
rev_implies: P ⇐ Q,
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
member: t ∈ T,
all: ∀x:A. B[x]
Lemmas referenced :
int-rmul-req,
req_weakening,
rless_functionality,
rmul-is-positive,
rless-int,
iff_wf,
int-rmul_wf,
rmul_wf,
int-to-real_wf,
rless_wf,
less_than_wf,
or_wf,
real_wf
Rules used in proof :
impliesLevelFunctionality,
sqequalRule,
levelHypothesis,
independent_isectElimination,
orLevelFunctionality,
andLevelFunctionality,
independent_functionElimination,
dependent_functionElimination,
orFunctionality,
impliesFunctionality,
productElimination,
addLevel,
because_Cache,
hypothesisEquality,
natural_numberEquality,
productEquality,
thin,
isectElimination,
sqequalHypSubstitution,
independent_pairFormation,
intEquality,
hypothesis,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}k:\mBbbZ{}. \mforall{}y:\mBbbR{}. (r0 < k * y \mLeftarrow{}{}\mRightarrow{} (0 < k \mwedge{} (r0 < y)) \mvee{} (k < 0 \mwedge{} (y < r0)))
Date html generated:
2016_11_11-AM-07_11_20
Last ObjectModification:
2016_11_10-PM-06_01_09
Theory : reals
Home
Index