Nuprl Lemma : small-real-test_wf
∀[k:ℕ+]. ∀[z:ℝ]. (small-real-test(k;z) ∈ ((r1)/k < z) ∨ (z < (r(4))/k))
Proof
Definitions occuring in Statement :
small-real-test: small-real-test(k;z),
rless: x < y,
int-rdiv: (a)/k1,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
or: P ∨ Q,
member: t ∈ T,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
small-real-test: small-real-test(k;z),
subtype_rel: A ⊆r B,
all: ∀x:A. B[x]
Lemmas referenced :
rless-case_wf,
int-rdiv_wf,
nat_plus_inc_int_nzero,
int-to-real_wf,
real_wf,
nat_plus_wf,
int-rdiv-rless-witness
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
applyEquality,
hypothesis,
closedConclusion,
natural_numberEquality,
because_Cache,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
universeIsType,
isect_memberEquality_alt,
isectIsTypeImplies,
inhabitedIsType,
dependent_functionElimination
Latex:
\mforall{}[k:\mBbbN{}\msupplus{}]. \mforall{}[z:\mBbbR{}]. (small-real-test(k;z) \mmember{} ((r1)/k < z) \mvee{} (z < (r(4))/k))
Date html generated:
2019_10_29-AM-10_05_01
Last ObjectModification:
2019_06_19-PM-05_57_40
Theory : reals
Home
Index