Nuprl Lemma : rmul_preserves_rneq_iff2
∀a,b,x:ℝ. (x ≠ r0 ⇒ (a ≠ b ⇐⇒ a * x ≠ b * x))
Proof
Definitions occuring in Statement :
rneq: 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],
member: t ∈ T,
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
uimplies: b supposing a
Lemmas referenced :
rmul_preserves_rneq_iff,
rneq_wf,
rmul_wf,
int-to-real_wf,
real_wf,
rneq_functionality,
rmul_comm
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
independent_pairFormation,
productElimination,
isectElimination,
natural_numberEquality,
independent_isectElimination
Latex:
\mforall{}a,b,x:\mBbbR{}. (x \mneq{} r0 {}\mRightarrow{} (a \mneq{} b \mLeftarrow{}{}\mRightarrow{} a * x \mneq{} b * x))
Date html generated:
2017_10_03-AM-08_35_23
Last ObjectModification:
2017_06_16-PM-01_02_55
Theory : reals
Home
Index