Nuprl Lemma : binomial_q
∀[a,b:ℚ]. ∀[n:ℕ]. (a + b ↑ n = Σ0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> (a ↑ i * b ↑ n - i) ∈ ℚ)
Proof
Definitions occuring in Statement :
qexp: r ↑ n,
qsum: Σa ≤ j < b. E[j],
qrng: <ℚ+*>,
qmul: r * s,
qadd: r + s,
rationals: ℚ,
nat: ℕ,
uall: ∀[x:A]. B[x],
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t ∈ T,
rng_nat_op: n ⋅r e,
choose: choose(n;i)
Definitions unfolded in proof :
qsum: Σa ≤ j < b. E[j],
q-rng-nexp: q-rng-nexp(r;n),
uall: ∀[x:A]. B[x],
member: t ∈ T,
qrng: <ℚ+*>,
rng_car: |r|,
pi1: fst(t),
rng_plus: +r,
pi2: snd(t),
rng_times: *,
infix_ap: x f y,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
rng: Rng,
squash: ↓T,
true: True,
less_than': less_than'(a;b),
le: A ≤ B,
top: Top,
not: ¬A,
false: False,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
or: P ∨ Q,
decidable: Dec(P),
ge: i ≥ j ,
guard: {T},
implies: P ⇒ Q,
all: ∀x:A. B[x],
lelt: i ≤ j < k,
uimplies: b supposing a,
and: P ∧ Q,
prop: ℙ,
so_apply: x[s],
so_lambda: λ2x.t[x],
int_iseg: {i...j},
int_seg: {i..j-},
crng: CRng,
subtype_rel: A ⊆r B,
nat: ℕ
Lemmas referenced :
binomial,
qrng_wf,
rationals_wf,
nat_wf,
iff_weakening_equal,
crng_wf,
qmul_wf,
rng_wf,
rng_car_wf,
rng_nat_op_wf,
qsum_wf,
qexp-eq-q-rng-nexp,
true_wf,
squash_wf,
equal_wf,
int_seg_wf,
int_term_value_subtract_lemma,
itermSubtract_wf,
subtract_wf,
false_wf,
int_seg_subtype_nat,
int_formula_prop_wf,
int_term_value_constant_lemma,
int_term_value_add_lemma,
int_formula_prop_less_lemma,
int_term_value_var_lemma,
int_formula_prop_le_lemma,
int_formula_prop_not_lemma,
int_formula_prop_and_lemma,
itermConstant_wf,
itermAdd_wf,
intformless_wf,
itermVar_wf,
intformle_wf,
intformnot_wf,
intformand_wf,
satisfiable-full-omega-tt,
decidable__le,
nat_properties,
int_seg_properties,
le_wf,
lelt_wf,
subtype_rel_sets,
choose_wf,
qadd_wf
Rules used in proof :
cut,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
hypothesisEquality,
isect_memberFormation,
independent_functionElimination,
baseClosed,
imageMemberEquality,
functionEquality,
universeEquality,
equalitySymmetry,
equalityTransitivity,
imageElimination,
dependent_set_memberEquality,
computeAll,
voidEquality,
voidElimination,
isect_memberEquality,
int_eqEquality,
dependent_pairFormation,
unionElimination,
dependent_functionElimination,
applyLambdaEquality,
independent_pairFormation,
productElimination,
lambdaFormation,
setEquality,
independent_isectElimination,
productEquality,
intEquality,
lambdaEquality,
applyEquality,
rename,
setElimination,
addEquality,
natural_numberEquality,
because_Cache
Latex:
\mforall{}[a,b:\mBbbQ{}]. \mforall{}[n:\mBbbN{}]. (a + b \muparrow{} n = \mSigma{}0 \mleq{} i < n + 1. choose(n;i) \mcdot{}<\mBbbQ{}+*> (a \muparrow{} i * b \muparrow{} n - i))
Date html generated:
2020_05_20-AM-09_25_50
Last ObjectModification:
2020_02_03-PM-02_21_04
Theory : rationals
Home
Index