### Nuprl Lemma : reg-seq-mul-regular

`∀[x,y:ℝ].  ∀k:ℕ+. k + 1-regular-seq(reg-seq-mul(x;y)) supposing ∀n:ℕ+. ((|x n| ≤ (n * k)) ∧ (|y n| ≤ (n * k)))`

Proof

Definitions occuring in Statement :  reg-seq-mul: `reg-seq-mul(x;y)` real: `ℝ` regular-int-seq: `k-regular-seq(f)` absval: `|i|` nat_plus: `ℕ+` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` multiply: `n * m` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` nat_plus: `ℕ+` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` and: `P ∧ Q` prop: `ℙ` regular-int-seq: `k-regular-seq(f)` subtype_rel: `A ⊆r B` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` le: `A ≤ B` real: `ℝ` nat: `ℕ` less_than': `less_than'(a;b)` guard: `{T}` ge: `i ≥ j ` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  reg-seq-mul-regular-eventually nat_plus_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf istype-less_than istype-int_upper subtype_rel_sets_simple less_than_wf le_wf decidable__le intformle_wf int_formula_prop_le_lemma le_witness_for_triv istype-le absval_wf nat_plus_wf real_wf int_upper_properties mul_preserves_le upper_subtype_nat istype-false subtract_wf add_nat_wf multiply_nat_wf nat_properties itermMultiply_wf intformeq_wf int_term_value_mul_lemma int_formula_prop_eq_lemma itermSubtract_wf int_term_value_subtract_lemma le_functionality multiply_functionality_wrt_le le_weakening add_functionality_wrt_le
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination dependent_set_memberEquality_alt addEquality setElimination rename hypothesis natural_numberEquality unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType inhabitedIsType applyEquality intEquality because_Cache productElimination equalityTransitivity equalitySymmetry functionIsTypeImplies functionIsType productIsType multiplyEquality isectIsTypeImplies applyLambdaEquality equalityIstype

Latex:
\mforall{}[x,y:\mBbbR{}].
\mforall{}k:\mBbbN{}\msupplus{}
k  +  1-regular-seq(reg-seq-mul(x;y))  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  ((|x  n|  \mleq{}  (n  *  k))  \mwedge{}  (|y  n|  \mleq{}  (n  *  k)))

Date html generated: 2019_10_16-PM-03_06_27
Last ObjectModification: 2019_02_14-PM-06_37_56

Theory : reals

Home Index