Nuprl Lemma : rv-between-small-expand

∀n:ℕ⁺. ∀a,c:ℝ^n. ∀k:ℕ⁺. (a ≠ c ⇒ (r(k + 1)/r(k))*a + (r(-1)/r(k))*c-a-(r(k + 1)/r(k))*c + (r(-1)/r(k))*a)

Proof

Definitions occuring in Statement : rv-between: a-b-c, real-vec-sep: a ≠ b, real-vec-mul: a*X, real-vec-add: X + Y, real-vec: ℝ^n, rdiv: (x/y), int-to-real: r(n), nat_plus: ℕ⁺, all: ∀x:A. B[x], implies: P ⇒ Q, add: n + m, minus: -n, natural_number: $n
Definitions unfolded in proof : all: ∀x:A. B[x], implies: P ⇒ Q, member: t ∈ T, prop: ℙ, uall: ∀[x:A]. B[x], subtype_rel: A ⊆r B, top: Top, and: P ∧ Q, cand: A c∧ B, nat_plus: ℕ⁺, decidable: Dec(P), or: P ∨ Q, iff: P ⇐⇒ Q, not: ¬A, rev_implies: P ⇐ Q, false: False, uiff: uiff(P;Q), uimplies: b supposing a, subtract: n - m, le: A ≤ B, less_than': less_than'(a;b), true: True, real-vec-sep: a ≠ b, rless: x < y, sq_exists: ∃x:{A| B[x]}, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], real-vec-between: a-b-c, rneq: x ≠ y, guard: {T}, real-vec-mul: a*X, real-vec-add: X + Y, req-vec: req-vec(n;x;y), rev_uimplies: rev_uimplies(P;Q), int_seg: {i..j^-}, lelt: i ≤ j < k, itermConstant: "const", req_int_terms: t1 ≡ t2, rdiv: (x/y), real-vec: ℝ^n, nequal: a ≠ b ∈ T , squash: ↓T, rv-between: a-b-c, rge: x ≥ y, real-vec-dist: d(x;y), real-vec-sub: X - Y, rsub: x - y, sq_stable: SqStable(P), real: ℝ
Lemmas referenced : real-vec-sep_wf, nat_plus_subtype_nat, nat_plus_wf, real-vec_wf, member_rooint_lemma, rless-int-fractions2, decidable__lt, false_wf, not-lt-2, less-iff-le, condition-implies-le, minus-add, minus-one-mul, zero-add, minus-one-mul-top, add-commutes, add_functionality_wrt_le, add-associates, add-zero, add-swap, le-add-cancel, less_than_wf, nat_plus_properties, satisfiable-full-omega-tt, intformand_wf, intformnot_wf, intformless_wf, itermMultiply_wf, itermConstant_wf, itermAdd_wf, itermVar_wf, int_formula_prop_and_lemma, int_formula_prop_not_lemma, int_formula_prop_less_lemma, int_term_value_mul_lemma, int_term_value_constant_lemma, int_term_value_add_lemma, int_term_value_var_lemma, int_formula_prop_wf, rless-int-fractions3, rdiv_wf, int-to-real_wf, rless-int, rless_wf, i-member_wf, rooint_wf, req-vec_wf, real-vec-add_wf, real-vec-mul_wf, rsub_wf, int_seg_wf, rmul_preserves_req, req_wf, rmul_wf, rinv_wf2, int_seg_properties, radd_wf, rminus_wf, real_term_polynomial, itermSubtract_wf, itermMinus_wf, real_term_value_const_lemma, real_term_value_sub_lemma, real_term_value_add_lemma, real_term_value_minus_lemma, real_term_value_var_lemma, req-iff-rsub-is-0, uiff_transitivity, req_functionality, req_transitivity, real_term_value_mul_lemma, radd_functionality, rminus_functionality, rmul_functionality, req_weakening, rmul-rinv, req_inversion, radd-int, rneq_functionality, rmul-int, rneq-int, int_entire_a, intformeq_wf, int_formula_prop_eq_lemma, equal-wf-base, int_subtype_base, equal-wf-T-base, rmul-rinv3, rminus-int, uiff_transitivity3, squash_wf, true_wf, real_wf, rneq_wf, mul_bounds_1b, rsub_functionality, rmul-int-fractions, rdiv_functionality, rinv-of-rmul, req-int, equal_wf, radd-preserves-req, real-vec-dist-between, real-vec-dist_wf, rleq_wf, rless_functionality, real-vec-dist-nonneg, rless_functionality_wrt_implies, rleq_weakening_equal, radd_functionality_wrt_rleq, real-vec-dist_functionality, req-vec_weakening, real-vec-add_functionality, real-vec-mul_functionality, rinv-as-rdiv, rmul-one-both, rmul-distrib, rmul-rdiv-cancel2, uiff_transitivity2, rmul_over_rminus, radd-rminus-assoc, radd-ac, radd_comm, radd-assoc, rmul_comm, real-vec-norm_functionality, real-vec-sub_wf, real-vec-norm_wf, real-vec-norm-mul, rabs_wf, rabs-of-nonneg, int_formula_prop_le_lemma, intformle_wf, decidable__le, sq_stable__less_than, rleq-int-fractions2, rmul-rdiv-cancel, rmul-ac, rmul-assoc, rmul_preserves_rless
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation, cut, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, hypothesisEquality, applyEquality, hypothesis, sqequalRule, because_Cache, dependent_functionElimination, isect_memberEquality, voidElimination, voidEquality, natural_numberEquality, addEquality, setElimination, rename, dependent_set_memberEquality, unionElimination, independent_pairFormation, productElimination, independent_functionElimination, independent_isectElimination, lambdaEquality, intEquality, minusEquality, multiplyEquality, dependent_pairFormation, int_eqEquality, computeAll, inrFormation, productEquality, baseApply, closedConclusion, baseClosed, equalitySymmetry, imageElimination, equalityTransitivity, imageMemberEquality, setEquality, addLevel, levelHypothesis

Latex:
\mforall{}n:\mBbbN{}\msupplus{}. \mforall{}a,c:\mBbbR{}\^{}n. \mforall{}k:\mBbbN{}\msupplus{}. (a \mneq{} c {}\mRightarrow{} (r(k + 1)/r(k))*a + (r(-1)/r(k))*c-a-(r(k + 1)/r(k))*c + (r(-1)/r(k))*a) Date html generated: 2017_10_03-AM-11_14_08 Last ObjectModification: 2017_07_28-AM-08_24_23 Theory : reals Home Index