### Nuprl Lemma : canonical-bound_wf

`∀[r:ℝ]. (canonical-bound(r) ∈ {k:{2...}| ∀n:ℕ+. (|r n| ≤ ((2 * n) * k))} )`

Proof

Definitions occuring in Statement :  canonical-bound: `canonical-bound(r)` real: `ℝ` absval: `|i|` int_upper: `{i...}` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` multiply: `n * m` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` squash: `↓T` real: `ℝ` nat_plus: `ℕ+` guard: `{T}` int_upper: `{i...}` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` prop: `ℙ` false: `False` subtype_rel: `A ⊆r B` nat: `ℕ` int_nzero: `ℤ-o` true: `True` nequal: `a ≠ b ∈ T ` sq_type: `SQType(T)` ge: `i ≥ j ` uiff: `uiff(P;Q)` and: `P ∧ Q` canonical-bound: `canonical-bound(r)` less_than: `a < b` rev_uimplies: `rev_uimplies(P;Q)` canon-bnd: `canon-bnd(x)`
Lemmas referenced :  canon-bnd_wf div_rem_sum absval_wf int_upper_properties decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than subtype_base_sq int_subtype_base nequal_wf rem_bounds_1 add_nat_wf decidable__le intformle_wf int_formula_prop_le_lemma istype-le nat_properties add-is-int-iff intformand_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma false_wf multiply-is-int-iff itermMultiply_wf int_term_value_mul_lemma mul_preserves_le nat_plus_subtype_nat nat_plus_wf real_wf nat_plus_properties le_functionality le_weakening
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality applyLambdaEquality setElimination rename sqequalRule imageMemberEquality baseClosed imageElimination addEquality applyEquality dependent_set_memberEquality_alt natural_numberEquality equalityTransitivity equalitySymmetry dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt isect_memberEquality_alt voidElimination universeIsType inhabitedIsType lambdaFormation_alt instantiate cumulativity intEquality equalityIstype sqequalBase because_Cache pointwiseFunctionality promote_hyp baseApply closedConclusion productElimination int_eqEquality independent_pairFormation divideEquality multiplyEquality functionIsType

Latex:
\mforall{}[r:\mBbbR{}].  (canonical-bound(r)  \mmember{}  \{k:\{2...\}|  \mforall{}n:\mBbbN{}\msupplus{}.  (|r  n|  \mleq{}  ((2  *  n)  *  k))\}  )

Date html generated: 2019_10_16-PM-03_06_42
Last ObjectModification: 2019_01_31-PM-04_38_30

Theory : reals

Home Index