Nuprl Lemma : rdiv-nonzero
∀x,y:ℝ. (y ≠ r0 ⇒ ((x/y) ≠ r0 ⇐⇒ x ≠ r0))
Proof
Definitions occuring in Statement :
rdiv: (x/y),
rneq: x ≠ y,
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,
member: t ∈ T,
uall: ∀[x:A]. B[x],
rdiv: (x/y),
iff: P ⇐⇒ Q,
and: P ∧ Q,
prop: ℙ,
rev_implies: P ⇐ Q,
uimplies: b supposing a,
rneq: x ≠ y,
or: P ∨ Q,
guard: {T},
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True
Lemmas referenced :
rmul-nonzero,
rinv_wf2,
rneq_wf,
int-to-real_wf,
rdiv_wf,
iff_wf,
real_wf,
rmul_reverses_rless_iff,
rless_wf,
rmul_preserves_rless,
rmul_wf,
rmul-zero-both,
rmul_comm,
rless-int,
rless_functionality,
req_transitivity,
rmul-rinv
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
independent_functionElimination,
hypothesis,
productElimination,
independent_pairFormation,
productEquality,
natural_numberEquality,
addLevel,
impliesFunctionality,
independent_isectElimination,
unionElimination,
inlFormation,
because_Cache,
sqequalRule,
inrFormation,
imageMemberEquality,
baseClosed
Latex:
\mforall{}x,y:\mBbbR{}. (y \mneq{} r0 {}\mRightarrow{} ((x/y) \mneq{} r0 \mLeftarrow{}{}\mRightarrow{} x \mneq{} r0))
Date html generated:
2017_10_03-AM-08_50_01
Last ObjectModification:
2017_06_15-PM-03_58_18
Theory : reals
Home
Index