[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification int-fac

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
BertrandsPostulateprovedall subs proved bertrand-holds-lower, bertrand-estimate, middle-coef-larger-strongest, bertrand-middle-coef-smaller, bertrand-prime-factors,
bertrand-middle-coef-smallerprovedall subs proved bertrand-small-primes, bertrand-big-primes, bertrand-middle-primes, coef-eq-zero, coef-le-zero,
bertrand-middle-primesprovedall subs proved max_exp-primes-two, max_exp-pos-02, max_exp-pos, middle-coef-max_exp-stronger, prime-product,
prime-productprovedall subs proved prime-product-between,
prime-product-betweenprovedall subs proved coef-le-2pot, coef-product-le,
bertrand-small-primesprovedall subs proved max_exp-def, max_exp-pos, middle-coef-max_exp-stronger, product-pot-no-dups,
middle-coef-larger-strongerprovedall subs proved coef-zero, middle-coef-larger-strongest,
middle-coef-largerprovedall subs proved coef-le-zero, coef-nls-zero, coef-zero, middle-coef-larger-strongest,
coef-le-2potprovedall subs proved fac-zero-02, binom-def, coef-nls-zero, Binom-theorem-countFun,
middle-coef-max_exp-strongerprovedall subs proved middle-coef-max_exp-le,
bertrand-big-primesprovedall subs proved middle-coef-not-one-01, max_exp-def, middle-coef-max_exp-big-primes,
middle-coef-larger-strongestprovedall subs proved middle-coef-largest, middle-coef-not-one-01, middle-coef-not-one, coef-same, coef-zero, Binom-theorem-countFun,
Binom-theoremprovedall subs proved Binom-theorem-countFun, binomlist-def2,
middle-coef-max_exp-leprovedall subs proved middle-coef-max_exp-equality,
middle-coef-not-oneprovedall subs proved middle-coef-not-one-01,
middle-coef-max_exp-big-primesprovedall subs proved est-4-big, middle-coef-max_exp-equality,
Binom-theorem-countFunprovedall subs proved countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-same, coef-zero,
middle-coef-max_exp-equalityprovedall subs proved max_exp-fac-gen-stronger, max_exp-mult, fac-le-zero, fac-pos-01, max_exp-div, fac-divides, binom-def,
middle-coef-largestprovedall subs proved coef-switch, middle-coef-largest-01,
middle-coef-not-one-01provedall subs proved middle-coef-largest-01, coef-one,
countFun-addprovedall subs proved coef-same-01, coef-pred-01, coef-rec-add-02,
middle-coef-max_expprovedall subs proved max_exp-fac-gen-stronger, max_exp-mult, fac-le-zero, fac-pos-01, max_exp-div, fac-divides, binom-def, max_exp-pos-02,
max_exp-fac-gen-strongerprovedall subs proved max_exp-fac-gen,
middle-coef-largest-01provedall subs proved fac-not-neg, fac-ls-zero, fac-pos-01, fac-le-zero, coef-sub,
coef-rec-add-02provedall subs proved coef-rec-add-01,
coef-rec-lowerprovedall subs proved coef-neg, coef-zero, coef-mult-rec-lower,
coef-recprovedall subs proved coef-zero, coef-neg, coef-mult-rec,
coef-neg-03provedall subs proved coef-neg,
coef-gcdprovedall subs proved coef-zero, coef-neg, coef-mult-rec,
coef-product-leprovedall subs proved coef-eq-zero, coef-le-zero, prime-divides-coef, primes-divide,
coef-subprovedall subs proved fac-zero-02, coef-sub-mult,
max_exp-fac-genprovedall subs proved max_exp-fac-smaller, max_exp-fac-rec,
coef-rec-add-01provedall subs proved fac-one, fac-not-zero, fac-rec, coef-fac-divides, fac-pos-01, fac-le-zero, fac-not-neg, coef-eq-zero, fac-zero-02, fac-zero, binom-def,
coef-negprovedall subs proved coef-eq-zero,
bertrand-prime-factorsprovedall subs proved middle-coef-divides-not,
coef-divides-rec-lowerprovedall subs proved coef-mult-rec-lower,
coef-divides-recprovedall subs proved coef-mult-rec,
max_exp-fac-recprovedall subs proved prime-fac-divides-not, max_exp-zero-02, max_exp-one, fac-zero, max_exp-same, fac-pos-01, max_exp-mult, fac-rec, max_exp-fac-add,
coef-sub-multprovedall subs proved fac-rec, fac-zero-02, fac-not-zero, fac-divides, binom-def,
prime-divides-coefprovedall subs proved prime-fac-divides, prime-fac-divides-01, prime-fac-divides-not, fac-not-zero, binom-def, fac-divides,
coef-mult-rec-lowerprovedall subs proved fac-zero-02, fac-rec, fac-not-zero, binom-def, fac-divides,
coef-mult-recprovedall subs proved fac-zero-02, fac-zero, fac-divides, fac-not-zero, fac-rec, binom-def,
middle-coef-divides-notprovedall subs proved prime-fac-divides-not, fac-not-zero, fac-divides, binom-def,
coef-eq-zeroprovedall subs proved fac-zero-02, fac-divides, fac-not-zero, binom-def, binom-less,
max_exp-fac-01provedall subs proved max_exp-zero, fac-pos-01, max_exp-mult, fac-rec, max_exp-fac-same,
max_exp-divprovedall subs proved max_exp-mult,
max_exp-fac-addprovedall subs proved max_exp-zero-02, fac-pos-01, max_exp-mult, fac-add,
max_exp-fac-smallerprovedall subs proved fac-zero, max_exp-zero-02, max_exp-smaller, fac-pos-01, max_exp-mult, fac-rec,
max_exp-fac-sameprovedall subs proved prime-fac-divides-not, max_exp-zero-02, max_exp-same, fac-pos-01, max_exp-mult, max_exp-one, fac-zero, fac-rec,
fac-dividesprovedall subs proved fac-zero, coef-fac-divides,
max_exp-multprovedall subs proved max_exp-mult-01,
coef-same-01provedall subs proved coef-same,
coef-fac-dividesprovedall subs proved coef-fac-divides-h, fac-rec, fac-one, fac-zero,
coef-oneprovedall subs proved fac-zero-02, fac-rec, fac-one, binom-def,
max_exp-mult-01provedall subs proved max_exp-not-div, max_exp-zero-01, max_exp-zero-02, max_exp-pos-04, max_exp-rec,
max_exp-smallerprovedall subs proved max_exp-zero-02,
max_exp-oneprovedall subs proved max_exp-zero-02,
fac-addprovedall subs proved fac-zero, fac-rec, fac-zero-02,
coef-pred-01provedall subs proved fac-zero-02, fac-rec, fac-one, binom-def,
coef-fac-divides-hprovedall subs proved fac-zero, fac-zero-02, fac-rec,
fac-not-zeroprovedall subs proved fac-zero-02,
coef-le-zeroprovedall subs proved coef-nls-zero,
coef-zeroprovedall subs proved fac-zero-02, fac-zero, binom-def,
coef-sameprovedall subs proved fac-zero-02, fac-zero, binom-def,
coef-succprovedall subs proved fac-zero-02, fac-rec, fac-one, binom-def,
max_exp-zero-02provedall subs proved max_exp-not-neg, max_exp-rec, max_exp-zero-01,
coef-nls-zeroprovedall subs proved fac-pos-01, fac-le-zero, fac-not-neg, binom-def, binom-less,
fac-zero-02provedall subs proved fac-pos,
max_exp-pos-03provedall subs proved max_exp-pos-04, max_exp-pos-01, max_exp-pos,
max_exp-lezprovedall subs proved max_exp-pos-02, max_exp-pos-04,
fac-leprovedall subs proved fac-not-neg, fac-le-zero, fac-one, fac-le-one, fac-zero, fac-rec,
prime-fac-dividesprovedall subs proved fac-zero, prime-fac-divides-01, fac-rec,
est-4-bigprovedall subs proved est-4-big-01,
fac-ls-zeroprovedall subs proved fac-not-neg, fac-pos-01,
max_exp-not-negprovedall subs proved max_exp-pos-04,
max_exp-pos-01provedall subs proved max_exp-pos,
max_exp-not-divprovedall subs proved max_exp-zero-01, max_exp-pos-04, max_exp-rec,
fac-posprovedall subs proved fac-pos-01,
fac-le-oneprovedall subs proved fac-one, fac-zero, fac-pos-01, fac-rec,
fac-le-zeroprovedall subs proved fac-pos-01, fac-not-neg,
max_exp-pos-02provedall subs proved max_exp-pos-04,
max_exp-div-notprovedall subs proved max_exp-zero-01, max_exp-same, max_exp-rec,
prime-fac-divides-01provedall subs proved fac-rec,
coef-switchprovedall subs proved binom-def,
max_exp-pos-04provedall subs proved max_exp-def,
prime-fac-divides-notprovedall subs proved fac-zero, fac-rec,
max_exp-zeroprovedall subs proved max_exp-def,
max_exp-recprovedall subs proved max_exp-def,
max_exp-sameprovedall subs proved max_exp-def,
max_exp-zero-01provedall subs proved max_exp-def,
est-4-big-01provedall subs proved est-4-big-02,
fac-not-negprovedall subs proved fac-zero, fac-rec,
fac-pos-01provedall subs proved fac-zero, fac-rec,
fac-oneprovedall subs proved fac-zero, fac-rec,
product-pot-no-dupsprovedall subs proved product-pot-rec,
max_exp-posprovedall subs proved max_exp-def,
max_exp-primes-twoprovedall subs proved max_exp-def,
bertrand-holds-lowerprovedall subs proved small-primes,
prime-divides-potprovedall subs proved prime-divides-pot-01,
max_exp-dividesprovedall subs proved product-pot-rec, max_exp-def,
fac-zero-01provedall subs proved fac-zero,
prime-divides-pot-01provedall subs proved
product-pot-recprovedall subs proved
est-4-big-02provedall subs proved
primes-divideprovedall subs proved
fac-zeroaxiom
fac-recaxiom
binom-lessaxiom
binom-defaxiom
small-primesprovedall subs proved
max_exp-defaxiom
countFun-potprovedall subs proved
countFun-pot-01provedall subs proved
countFun-shiftprovedall subs proved
binomlist-def2axiom
bertrand-estimateprovedall subs proved