Nuprl Lemma : rleq-ratbound
∀[x:ℤ × ℕ+]. (|ratreal(x)| ≤ r(ratbound(x)))
Proof
Definitions occuring in Statement :
ratbound: ratbound(x),
ratreal: ratreal(r),
rleq: x ≤ y,
rabs: |x|,
int-to-real: r(n),
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
product: x:A × B[x],
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
nat_plus: ℕ+,
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
sq_stable__rleq,
ratbound_wf,
rabs_wf,
ratreal_wf,
int-to-real_wf,
istype-int,
nat_plus_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
inhabitedIsType,
lambdaFormation_alt,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
because_Cache,
setElimination,
rename,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
productIsType,
universeIsType
Latex:
\mforall{}[x:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}]. (|ratreal(x)| \mleq{} r(ratbound(x)))
Date html generated:
2019_10_30-AM-09_33_54
Last ObjectModification:
2019_01_11-PM-01_29_00
Theory : reals
Home
Index