Nuprl Lemma : MachinPi4-positive
r0 < MachinPi4()
Proof
Definitions occuring in Statement :
MachinPi4: MachinPi4(),
rless: x < y,
int-to-real: r(n),
natural_number: $n
Definitions unfolded in proof :
rless: x < y,
sq_exists: ∃x:A [B[x]],
member: t ∈ T,
nat_plus: ℕ+,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
and: P ∧ Q,
uall: ∀[x:A]. B[x],
int-to-real: r(n),
MachinPi4: MachinPi4(),
rsub: x - y,
radd: a + b,
accelerate: accelerate(k;f),
reg-seq-list-add: reg-seq-list-add(L),
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
cons: [a / b],
int-rmul: k1 * a,
atan: atan(a;x),
atan_approx: atan_approx(a;x;M),
atan-log: atan-log(a;M),
gen_log_aux: gen_log_aux(p;c;x;i;n;M),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
bnot: ¬bb,
lt_int: i <z j,
exp: i^n,
primrec: primrec(n;b;c),
primtailrec: primtailrec(n;i;b;f),
subtract: n - m,
bfalse: ff,
btrue: tt,
atan-approx: atan-approx(k;x;N),
poly-approx: poly-approx(a;x;k;N),
rmul: a * b,
int-rdiv: (a)/k1,
imax: imax(a;b),
canonical-bound: canonical-bound(r),
absval: |i|,
reg-seq-mul: reg-seq-mul(x;y),
poly-approx-aux: poly-approx-aux(a;x;xM;M;n;k),
eq_int: (i =z j),
rminus: -(x),
nil: [],
it: ⋅,
subtype_rel: A ⊆r B,
real: ℝ,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a
Lemmas referenced :
istype-less_than,
image-type_wf,
less_than'_wf,
int-to-real_wf,
MachinPi4_wf,
equal-wf-base,
set_subtype_base,
less_than_wf,
istype-int,
int_subtype_base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependent_set_memberFormation_alt,
sqequalRule,
dependent_set_memberEquality_alt,
natural_numberEquality,
cut,
independent_pairFormation,
introduction,
imageMemberEquality,
hypothesisEquality,
thin,
baseClosed,
sqequalHypSubstitution,
hypothesis,
extract_by_obid,
isectElimination,
universeIsType,
productEquality,
addEquality,
applyEquality,
lambdaEquality_alt,
setElimination,
rename,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
intEquality,
baseApply,
closedConclusion,
independent_isectElimination,
because_Cache
Latex:
r0 < MachinPi4()
Date html generated:
2019_10_31-AM-06_06_04
Last ObjectModification:
2019_01_29-PM-03_22_26
Theory : reals_2
Home
Index