Nuprl Lemma : regular-upto-iff

k,b:ℕ+. ∀x:ℕ+ ⟶ ℤ.
  (↑regular-upto(k;b;x)
  ⇐⇒ ∀n,m:ℕ+1.
        let seq-min-upper(k;b;x) in
         let (r((x j) (2 k))/r((2 k) j)) in
         (((r((x n) k)/r((2 k) n)) ≤ z) ∧ (z ≤ (r((x n) (2 k))/r((2 k) n))))
         ∧ ((r((x m) k)/r((2 k) m)) ≤ z)
         ∧ (z ≤ (r((x m) (2 k))/r((2 k) m))))


Proof




Definitions occuring in Statement :  seq-min-upper: seq-min-upper(k;n;f) regular-upto: regular-upto(k;n;f) rdiv: (x/y) rleq: x ≤ y int-to-real: r(n) int_seg: {i..j-} nat_plus: + assert: b let: let all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q apply: a function: x:A ⟶ B[x] multiply: m subtract: m add: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T uall: [x:A]. B[x] nat_plus: + prop: subtype_rel: A ⊆B rev_implies:  Q so_lambda: λ2x.t[x] int_seg: {i..j-} decidable: Dec(P) or: P ∨ Q not: ¬A false: False uiff: uiff(P;Q) uimplies: supposing a lelt: i ≤ j < k top: Top le: A ≤ B less_than': less_than'(a;b) true: True rneq: x ≠ y guard: {T} less_than: a < b squash: T satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] cand: c∧ B so_apply: x[s] nat: let: let bool: 𝔹 unit: Unit it: btrue: tt bfalse: ff sq_type: SQType(T) bnot: ¬bb ifthenelse: if then else fi  assert: b
Lemmas referenced :  int_seg_wf assert_wf regular-upto_wf nat_plus_subtype_nat nat_plus_wf all_wf let_wf real_wf rleq_wf rdiv_wf int-to-real_wf subtract_wf decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel less_than_wf rless-int multiply_nat_plus nat_plus_properties int_seg_properties full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf itermMultiply_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma int_formula_prop_wf equal_wf rless_wf seq-min-upper_wf assert-regular-upto seq-min-upper-property seq-min-upper-le decidable__le intformle_wf int_formula_prop_le_lemma le_wf itermAdd_wf int_term_value_add_lemma lelt_wf rleq-int-fractions mul_nat_plus mul_preserves_le multiply-is-int-iff int_subtype_base subtract-is-int-iff itermSubtract_wf int_term_value_subtract_lemma absval_ubound mul_bounds_1a minus-is-int-iff itermMinus_wf int_term_value_minus_lemma rleq_transitivity absval_unfold bool_wf eqtt_to_assert assert_of_lt_int mul_cancel_in_le add-is-int-iff eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality addEquality setElimination rename hypothesisEquality hypothesis applyEquality sqequalRule because_Cache functionExtensionality lambdaEquality instantiate cumulativity universeEquality productEquality dependent_set_memberEquality dependent_functionElimination unionElimination voidElimination productElimination independent_functionElimination independent_isectElimination isect_memberEquality voidEquality intEquality multiplyEquality inrFormation imageMemberEquality baseClosed equalityTransitivity equalitySymmetry applyLambdaEquality approximateComputation dependent_pairFormation int_eqEquality functionEquality addLevel baseApply closedConclusion pointwiseFunctionality promote_hyp allFunctionality equalityElimination minusEquality lessCases isect_memberFormation sqequalAxiom imageElimination

Latex:
\mforall{}k,b:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.
    (\muparrow{}regular-upto(k;b;x)
    \mLeftarrow{}{}\mRightarrow{}  \mforall{}n,m:\mBbbN{}\msupplus{}b  +  1.
                let  j  =  seq-min-upper(k;b;x)  in
                  let  z  =  (r((x  j)  +  (2  *  k))/r((2  *  k)  *  j))  in
                  (((r((x  n)  -  2  *  k)/r((2  *  k)  *  n))  \mleq{}  z)  \mwedge{}  (z  \mleq{}  (r((x  n)  +  (2  *  k))/r((2  *  k)  *  n))))
                  \mwedge{}  ((r((x  m)  -  2  *  k)/r((2  *  k)  *  m))  \mleq{}  z)
                  \mwedge{}  (z  \mleq{}  (r((x  m)  +  (2  *  k))/r((2  *  k)  *  m))))



Date html generated: 2017_10_03-AM-08_44_27
Last ObjectModification: 2017_09_11-PM-01_08_40

Theory : reals


Home Index