Nuprl Lemma : small-ctrex1_wf
small-ctrex1() ∈ ℝ
Proof
Definitions occuring in Statement :
small-ctrex1: small-ctrex1(),
real: ℝ,
member: t ∈ T
Definitions unfolded in proof :
small-ctrex1: small-ctrex1(),
uiff: uiff(P;Q),
nat_plus: ℕ+,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
or: P ∨ Q,
rneq: x ≠ y,
guard: {T},
all: ∀x:A. B[x],
sq_type: SQType(T),
uimplies: b supposing a,
nequal: a ≠ b ∈ T ,
int_nzero: ℤ-o,
prop: ℙ,
implies: P ⇒ Q,
not: ¬A,
false: False,
le: A ≤ B,
nat: ℕ,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
member: t ∈ T,
true: True,
efficient-exp-ext,
fastexp: i^n,
less_than': less_than'(a;b),
squash: ↓T,
less_than: a < b,
rev_uimplies: rev_uimplies(P;Q),
subtype_rel: A ⊆r B,
exists: ∃x:A. B[x],
reg-seq-mul: reg-seq-mul(x;y),
lt_int: i <z j,
bnot: ¬bb,
le_int: i ≤z j,
rroot-odd: rroot-odd(i;x),
canonical-bound: canonical-bound(r),
imax: imax(a;b),
bfalse: ff,
rmul: a * b,
rminus: -(x),
genrec-ap: genrec-ap,
primrec: primrec(n;b;c),
exp: i^n,
integer-nth-root-ext,
iroot: iroot(n;x),
it: ⋅,
nil: [],
int-rdiv: (a)/k1,
absval: |i|,
rabs: |x|,
subtract: n - m,
rroot-abs: rroot-abs(i;x),
btrue: tt,
modulus: a mod n,
eq_int: (i =z j),
isEven: isEven(n),
ifthenelse: if b then t else f fi ,
rroot: rroot(i;x),
rsub: x - y,
cons: [a / b],
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
reg-seq-list-add: reg-seq-list-add(L),
accelerate: accelerate(k;f),
radd: a + b,
un-ctrex1: un-ctrex1(x),
int-to-real: r(n)
Lemmas referenced :
efficient-exp-ext,
integer-nth-root-ext,
equal-wf-base,
rless-iff2,
rleq_weakening_rless,
int-rdiv-req,
req_weakening,
rleq_functionality,
fastexp_wf,
false_wf,
le_wf,
un-ctrex1_wf,
int-rdiv_wf,
subtype_base_sq,
int_subtype_base,
true_wf,
nequal_wf,
rleq_wf,
int-to-real_wf,
rdiv_wf,
rless-int,
rless_wf,
rleq-int-fractions2,
less_than_wf
Rules used in proof :
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
multiplyEquality,
productElimination,
inrFormation,
minusEquality,
voidElimination,
independent_functionElimination,
equalitySymmetry,
equalityTransitivity,
dependent_functionElimination,
independent_isectElimination,
intEquality,
cumulativity,
instantiate,
addLevel,
because_Cache,
baseClosed,
imageMemberEquality,
introduction,
hypothesisEquality,
hypothesis,
lambdaFormation,
dependent_set_memberEquality,
thin,
isectElimination,
sqequalHypSubstitution,
lemma_by_obid,
natural_numberEquality,
independent_pairFormation,
sqequalRule,
cut,
applyEquality,
addEquality,
dependent_pairFormation
Latex:
small-ctrex1() \mmember{} \mBbbR{}
Date html generated:
2016_05_18-AM-10_48_15
Last ObjectModification:
2016_01_17-AM-00_25_40
Theory : reals
Home
Index