Nuprl Lemma : rneq-cases
∀x,y:ℝ. (x ≠ y ⇒ (∀z:ℝ. (x ≠ z ∨ y ≠ z)))
Proof
Definitions occuring in Statement :
rneq: x ≠ y,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
rneq: x ≠ y,
or: P ∨ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
guard: {T}
Lemmas referenced :
real_wf,
rneq_wf,
rless-cases,
rless_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
unionElimination,
thin,
cut,
introduction,
extract_by_obid,
hypothesis,
isectElimination,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination,
inlFormation,
sqequalRule,
inrFormation
Latex:
\mforall{}x,y:\mBbbR{}. (x \mneq{} y {}\mRightarrow{} (\mforall{}z:\mBbbR{}. (x \mneq{} z \mvee{} y \mneq{} z)))
Date html generated:
2016_10_26-AM-09_11_38
Last ObjectModification:
2016_10_14-PM-05_49_18
Theory : reals
Home
Index