Nuprl Lemma : dd

Nuprl Lemma : dd_wf

∀d:ℕ⁺. ∀x:ℝ.
  (d decimal digits of x  ∈ {a:Atom| a = "display-as" ∈ Atom}
   × {a:Atom| a = "decimal-rational" ∈ Atom}
   × {z:ℝ| z = x}
   × {n:ℕ⁺| n = d ∈ ℤ}
   × {n:ℤ| |x - (r(n)/r(10^d))| ≤ (r(2)/r(10^d))} )

Proof

Definitions occuring in Statement : dd: n decimal digits of x , rdiv: (x/y), rleq: x ≤ y, rabs: |x|, rsub: x - y, req: x = y, int-to-real: r(n), real: ℝ, fastexp: i^n, nat_plus: ℕ⁺, all: ∀x:A. B[x], member: t ∈ T, set: {x:A| B[x]} , product: x:A × B[x], natural_number: $n, int: ℤ, token: "$token", atom: Atom, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], member: t ∈ T, dd: n decimal digits of x , uall: ∀[x:A]. B[x], nat_plus: ℕ⁺, less_than: a < b, squash: ↓T, less_than': less_than'(a;b), true: True, and: P ∧ Q, implies: P ⇒ Q, has-value: (a)↓, uimplies: b supposing a, so_lambda: λ₂x.t[x], so_apply: x[s], subtype_rel: A ⊆r B, sq_type: SQType(T), guard: {T}, exp: i^n, primrec: primrec(n;b;c), subtract: n - m, nat: ℕ, decidable: Dec(P), or: P ∨ Q, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, top: Top, prop: ℙ, le: A ≤ B, nequal: a ≠ b ∈ T , int_nzero: ℤ^-^o, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, uiff: uiff(P;Q), rational-approx: (x within 1/n), real: ℝ, rneq: x ≠ y, rev_uimplies: rev_uimplies(P;Q), rge: x ≥ y, callbyvalueall: callbyvalueall, has-valueall: has-valueall(a)
Lemmas referenced : exp-fastexp, exp_wf_nat_plus, istype-less_than, real_wf, nat_plus_wf, value-type-has-value, set-value-type, less_than_wf, istype-int, int-value-type, nat_plus_subtype_nat, subtype_base_sq, set_subtype_base, int_subtype_base, nat_plus_properties, primrec-wf-nat-plus, equal-wf-base, decidable__le, full-omega-unsat, intformand_wf, intformnot_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, int_formula_prop_and_lemma, istype-void, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, istype-le, istype-false, decidable__equal_int, intformeq_wf, itermMultiply_wf, int_formula_prop_eq_lemma, int_term_value_mul_lemma, mul-commutes, div-cancel, nequal_wf, equal_wf, squash_wf, true_wf, istype-universe, exp_add, exp1, subtype_rel_self, iff_weakening_equal, rational-approx-property, decidable__lt, multiply-is-int-iff, false_wf, atom_subtype_base, req_weakening, req_wf, rleq_wf, rabs_wf, rsub_wf, int-rdiv_wf, int-to-real_wf, rdiv_wf, rless-int, rless_wf, nat_plus_inc_int_nzero, rleq_functionality, rabs_functionality, rsub_functionality, int-rdiv-req, rleq-int-fractions, rleq_functionality_wrt_implies, rleq_weakening_equal, valueall-type-has-valueall, product-valueall-type, istype-atom, set-valueall-type, atom-valueall-type, real-valueall-type, int-valueall-type, evalall-reduce
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation_alt, cut, sqequalRule, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, natural_numberEquality, because_Cache, hypothesis, dependent_set_memberEquality_alt, independent_pairFormation, imageMemberEquality, hypothesisEquality, baseClosed, inhabitedIsType, equalityIsType1, equalityTransitivity, equalitySymmetry, dependent_functionElimination, independent_functionElimination, universeIsType, callbyvalueReduce, independent_isectElimination, intEquality, lambdaEquality_alt, closedConclusion, applyEquality, instantiate, cumulativity, rename, setElimination, equalityIsType4, baseApply, unionElimination, approximateComputation, dependent_pairFormation_alt, int_eqEquality, isect_memberEquality_alt, voidElimination, multiplyEquality, imageElimination, universeEquality, divideEquality, productElimination, applyLambdaEquality, pointwiseFunctionality, promote_hyp, independent_pairEquality, tokenEquality, inrFormation_alt, productEquality, setEquality, atomEquality, setIsType

Latex:
\mforall{}d:\mBbbN{}\msupplus{}. \mforall{}x:\mBbbR{}. (d decimal digits of x \mmember{} \{a:Atom| a = "display-as"\} \mtimes{} \{a:Atom| a = "decimal-rational"\} \mtimes{} \{z:\mBbbR{}| z = x\} \mtimes{} \{n:\mBbbN{}\msupplus{}| n = d\} \mtimes{} \{n:\mBbbZ{}| |x - (r(n)/r(10\^{}d))| \mleq{} (r(2)/r(10\^{}d))\} ) Date html generated: 2019_10_30-AM-07_52_34 Last ObjectModification: 2018_11_08-PM-02_14_25 Theory : reals Home Index