Nuprl Lemma : square-req-self-iff
∀x:ℝ. ((x * x) = x ⇐⇒ (x = r1) ∨ (x = r0))
Proof
Definitions occuring in Statement :
req: x = y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
natural_number: $n
Definitions unfolded in proof :
rev_implies: P ⇐ Q,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
implies: P ⇒ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
all: ∀x:A. B[x],
guard: {T},
or: P ∨ Q,
true: True,
less_than': less_than'(a;b),
squash: ↓T,
less_than: a < b,
uiff: uiff(P;Q),
uimplies: b supposing a,
rneq: x ≠ y,
not: ¬A,
false: False,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
real_wf,
int-to-real_wf,
or_wf,
rmul_wf,
req_wf,
rless-int,
rless-cases,
rmul-rinv,
rmul_functionality,
req_transitivity,
req_functionality,
req_weakening,
rmul-one,
rmul_assoc,
rless_wf,
rinv_wf2,
rmul_preserves_req,
rless_functionality,
rmul_comm,
rmul-zero-both,
rmul_preserves_rless,
rneq_wf,
not-rneq,
square-nonneg,
rleq_functionality,
rless_irreflexivity,
rless_transitivity1,
rleq_weakening,
req_inversion,
rleq_weakening_rless,
rless_transitivity2,
rmul-zero
Rules used in proof :
natural_numberEquality,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
independent_pairFormation,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
inrFormation,
inlFormation,
unionElimination,
baseClosed,
imageMemberEquality,
sqequalRule,
productElimination,
independent_functionElimination,
dependent_functionElimination,
because_Cache,
independent_isectElimination,
voidElimination
Latex:
\mforall{}x:\mBbbR{}. ((x * x) = x \mLeftarrow{}{}\mRightarrow{} (x = r1) \mvee{} (x = r0))
Date html generated:
2017_10_03-AM-08_47_37
Last ObjectModification:
2017_07_31-PM-09_30_41
Theory : reals
Home
Index