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: |
|---|
| square-neq-any | proved | all subs proved
| square-neq-any-pos,
|
| square-neq-any-pos | proved | all subs proved
| square-neq-any-pos-01,
|
| square-neq-any-pos-01 | proved | all subs proved
| div-gcd-not-neg,
gcd-div-gcd,
gcd-zero-03,
gcd-com,
gcd-zero-04,
gcd-div-shift,
square-neq-any-pos-02,
|
| square-neq-prime | proved | all subs proved
| prime-small,
square-neq-pos,
|
| gcd-divides-01 | proved | all subs proved
| gcd-divides-both,
|
| square-neq-pos | proved | all subs proved
| gcd-nls-zero,
div-gcd-not-neg,
gcd-div-gcd,
gcd-zero-03,
gcd-com,
gcd-zero-04,
gcd-div-shift,
square-neq-pos-h,
|
| square-neq-any-pos-02 | proved | all subs proved
| gcd-same-01,
div-zero,
div-mult,
gcd-mult,
prime-divides,
prime-small,
gcd-mult-01,
gcd-abs,
not-less-gcd,
gcd-zero-zero,
gcd-less-eq-zero,
div-gcd-not-neg,
gcd-div-gcd,
gcd-zero-03,
gcd-com,
gcd-zero-04,
gcd-div-shift,
prime-not-neg-01,
prime-not-neg,
prime-one,
prime-abs,
divides,
prime-def-prime,
square-neq-pos-h,
|
| gcd-divides-both | proved | all subs proved
| divides-abs,
div-abs-02,
div-neg,
gcd-same-02,
gcd-com,
gcd-abs-rew-02,
divides-abs-01,
gcd-divides-both-h,
|
| square-neq-pos-h | proved | all subs proved
| div-zero,
div-mult,
prime-divides,
gcd-abs,
prime-abs,
gcd-mult,
prime-small,
gcd-com,
gcd-zero-04,
divides,
|
| gcd-divides-both-h | proved | all subs proved
| gcd-same-01,
div-zero-01,
gcd-com,
gcd-zero-04,
divides-add,
gcd-rec-sub-01,
|
| prime-divides-01 | proved | all subs proved
| div-not-ls,
prime-divides,
divides,
|
| max_prime_divisor-divides-03 | proved | all subs proved
| prime-one,
prime-abs,
max_prime_divisor-prime,
divides-prime,
prime-divides,
max_prime_divisor-not-zero,
divides,
max_prime_divisor-divides,
|
| max_prime_divisor-divides-02 | proved | all subs proved
| prime-divides,
max_prime_divisor-not-zero,
divides,
max_prime_divisor-divides,
|
| gcd-mod-one-01 | proved | all subs proved
| gcd-zero-04,
gcd-mod-one,
|
| gcd-div-gcd | proved | all subs proved
| gcd-abs,
gcd-zero-zero,
gcd-zero-04,
gcd-zero-03,
gcd-div-gcd-pos,
gcd-abs-rew-02,
|
| prime-divides | proved | all subs proved
| divides-mult-01,
gcd-one-prime,
coprime-divides-02,
|
| gcd-mod-one | proved | all subs proved
| gcd-one-01,
divides,
gcd-conq-one,
|
| gcd-rec-sub-01 | proved | all subs proved
| gcd-rec-sub-02,
gcd-same-01,
gcd-neg,
gcd-abs-rew-02,
gcd-zero-03,
gcd-same,
gcd-com,
gcd-zero-04,
gcd-rec-sub,
|
| gcd-rec-sub-03 | proved | all subs proved
| gcd-zero-03,
gcd-zero,
gcd-same,
gcd-zero-04,
gcd-rec-sub,
gcd-com,
gcd-neg,
gcd-abs-rew-02,
gcd-rec-sub-02,
|
| div-gcd-one | proved | all subs proved
| gcd-one-01,
|
| coprime-divides-02 | proved | all subs proved
| coprime-divides-01,
|
| gcd-one-prime | proved | all subs proved
| divides-prime,
gcd-one,
|
| gcd-rec-sub-02 | proved | all subs proved
| gcd-com,
gcd-add,
|
| gcd-div-gcd-pos | proved | all subs proved
| gcd-zero,
div-mult,
gcd-zero-04,
gcd-max,
divides,
gcd-com,
gcd-div-rest,
gcd-zero-zero,
gcd-less-eq-zero,
gcd-one,
|
| gcd-one-01 | proved | all subs proved
| div-not-ls,
gcd-one,
|
| gcdex-smallest-pos | proved | all subs proved
| gcdex-pos,
|
| gcd-primes | proved | all subs proved
| prime-abs,
divides-prime,
gcd-one,
|
| gcd-prime | proved | all subs proved
| div-not-ls,
prime-def,
gcd-one,
|
| gcd-one-eq-02 | proved | all subs proved
| gcd-zero-zero,
gcd-com,
gcd-abs-rew,
gcd-one-eq,
|
| gcd-one-eq-01 | proved | all subs proved
| gcd-zero-zero,
gcd-com,
gcd-abs-rew,
gcd-one-eq,
|
| gcd-negone-eq | proved | all subs proved
| gcd-zero,
gcd-zero-zero,
gcd-pos,
gcd-com,
gcd-neg,
gcd-one-eq,
|
| div-gcd-is-neg-01-01 | proved | all subs proved
| div-gcd-neg-not-zero,
div-gcd-is-neg-01,
div-gcd-is-neg,
|
| coprime-divides-03 | proved | all subs proved
| coprime-divides-01,
|
| coprime-divides | proved | all subs proved
| div-mult,
coprime-divides-01,
|
| gcd-nls-zero | proved | all subs proved
| gcd-zero-02,
gcd-zero-zero,
gcd-less-eq-zero,
|
| gcd-div-shift | proved | all subs proved
| gcd-div-mult-shift,
|
| gcdex-pos | proved | all subs proved
| gcd-zero-04,
gcdex-not-unique,
gcdex,
|
| gcd-add | proved | all subs proved
| gcd-rec-sub,
gcd-com,
|
| gcd-one-eq | proved | all subs proved
| gcd-less-eq-zero,
gcd-zero,
gcd-zero-04,
gcd-div2,
gcd-zero-zero,
div-eq-one,
gcd-pos,
|
| gcd-conq-one | proved | all subs proved
| div-one,
gcd-com,
gcd-zero-04,
div-mult,
div-neg,
gcdex,
|
| gcd-one | proved | all subs proved
| gcd-div2,
gcd-div1,
gcd-zero,
gcd-zero-zero,
gcd-less-eq-zero,
div-one-neg-pos,
div-one-one,
div-zero-01,
gcd-com,
gcd-zero-04,
div-one,
gcd-less,
|
| div-gcd-is-neg-01 | proved | all subs proved
| div-gcd-is-neg,
|
| div-gcd-neg-not-zero | proved | all subs proved
| div-gcd-zero,
gcd-zero-04,
gcd-com,
gcd-zero-03,
abs-gcd-not-less,
|
| coprime-divides-01 | proved | all subs proved
| divides-mult-01,
div-mult,
divides-add,
gcdex,
|
| gcd-mult-pos-01 | proved | all subs proved
| gcd-mult,
|
| gcd-max-prop | proved | all subs proved
| div-abs,
gcd-mult,
divides,
|
| gcd-ge-one | proved | all subs proved
| gcd-zero-zero,
gcd-less-eq-zero,
|
| gcd-div-mult | proved | all subs proved
| gcd-zero-zero,
gcd-div-mult-shift,
|
| gcd-conq-one-01 | proved | all subs proved
| div-mult,
div-neg,
gcdex,
|
| div-gcd-not-neg | proved | all subs proved
| gcd-zero,
gcd-zero-zero,
not-less-gcd,
gcd-pos,
|
| gcd-mult | proved | all subs proved
| gcd-mult-pos,
gcd-abs-rew-02,
gcd-zero-03,
gcd-com,
gcd-zero-04,
gcd-zero,
|
| gcd-div-mult-shift | proved | all subs proved
| gcd-div1,
gcd-zero-zero,
div-mult-shift,
|
| gcd-less-eq-zero | proved | all subs proved
| gcd-zero,
gcd-zero-zero,
gcd-zero-02,
|
| gcd-rec-sub | proved | all subs proved
| gcd-rec-pos,
gcd-com,
|
| div-gcd-zero | proved | all subs proved
| gcd-nls,
gcd-abs,
gcd-zero-zero,
gcd-zero-03,
|
| div-gcd-is-neg | proved | all subs proved
| gcd-zero,
gcd-zero-zero,
gcd-pos,
|
| gcdex | proved | all subs proved
| gcd-com,
gcd-neg,
gcdhex,
gcd-abs-rew-02,
|
| num-gcd-pos | proved | all subs proved
| gcd-rec-pos,
|
| gcd-zero-05 | proved | all subs proved
| gcd-zero,
gcd-zero-zero,
gcd-zero-02,
gcd-pos,
|
| gcd-div-eq | proved | all subs proved
| gcd-div1,
mod-gcd,
gcd-zero-zero,
div-eq,
|
| exgcd-div | proved | all subs proved
| gcd-zero,
gcd-zero-zero,
divides,
gcd-div1,
|
| gcd-mult-01 | proved | all subs proved
| gcd-zero-04,
gcd-zero,
gcd-rec,
gcd-com,
|
| gcdhex | proved | all subs proved
| gcd-zero-03,
gcd-same-01,
gcd-rec,
gcd-zero-04,
|
| gcd-rec-pos | proved | all subs proved
| gcd-com,
gcd-zero-04,
gcd-rec,
|
| gcd-mult-pos | proved | all subs proved
| gcd-zero-04,
gcd-zero,
gcd-rec,
gcd-com,
|
| abs-gcd-not-less | proved | all subs proved
| gcd-com,
gcd-zero-03,
gcd-nls,
not-less-gcd,
|
| gcd-zero-zero | proved | all subs proved
| gcd-com,
gcd-zero-03,
div-zero-zero,
gcd-div1,
gcd-zero,
|
| mod-gcd-01 | proved | all subs proved
| gcd-com,
gcd-zero-03,
divides,
gcd-div1,
mod-gcd,
|
| max_prime_divisor-nle-01 | proved | all subs proved
| prime-one,
prime-not-neg-01,
max_prime_divisor-def,
prime-ex-max,
max_prime_divisor-ge2,
|
| max_prime_divisor-abs | proved | all subs proved
| max_prime_divisor-abs-01,
max_prime_divisor-not-zero,
|
| max_prime_divisor-ge2 | proved | all subs proved
| max_prime_divisor-prime,
max_prime_divisor-nls-zero,
max_prime_divisor-not-zero,
divides,
max_prime_divisor-divides,
|
| max_prime_divisor-abs-01 | proved | all subs proved
| max_prime_divisor-nls-zero,
|
| gcd-rec | proved | all subs proved
| div-mult,
divides-mult-sub,
divides,
gcd-div2,
gcd-div1,
gcd-nls-01,
gcd-com,
gcd-zero-04,
gcd-less,
gcd-abs-rew-02,
|
| gcd-same-01 | proved | all subs proved
| gcd-zero,
gcd-same,
|
| gcd-same-02 | proved | all subs proved
| gcd-zero,
gcd-same,
|
| gcd-zero-03 | proved | all subs proved
| gcd-zero-04,
|
| max_prime_divisor-nle-zero-01 | proved | all subs proved
| max_prime_divisor-nls-01,
max_prime_divisor-nle-zero,
max_prime_divisor-not-zero,
|
| max_prime_divisor-nls-01 | proved | all subs proved
| max_prime_divisor-nle,
|
| max_prime_divisor-nls-zero | proved | all subs proved
| prime-def,
max_prime_divisor-prime,
|
| max_prime_divisor-not-zero | proved | all subs proved
| max_prime_divisor-nle-zero,
|
| gcd-same | proved | all subs proved
| gcd-nls-01,
div-zero,
divides-abs,
gcd-max,
gcd-div1,
gcd-abs-rew-02,
|
| gcd-zero-04 | proved | all subs proved
| gcd-zero,
gcd-nls-01,
div-zero-01,
divides-abs-01,
div-zero,
divides-abs,
gcd-max,
gcd-div1,
gcd-abs-rew-02,
|
| max_prime_divisor-divides-01 | proved | all subs proved
| max_prime_divisor-divides,
div-mod-zero,
|
| max_prime_divisor-nle | proved | all subs proved
| max_prime_divisor-def,
prime-ex-max,
|
| max_prime_divisor-nle-zero | proved | all subs proved
| prime-not-neg-01,
max_prime_divisor-def,
prime-ex-max,
|
| max_prime_divisor-prime | proved | all subs proved
| max_prime_divisor-def,
prime-ex-max,
|
| max_prime_divisor-divides | proved | all subs proved
| max_prime_divisor-def,
prime-ex-max,
|
| gcd-nls-01 | proved | all subs proved
| gcd-nls,
gcd-abs-rew-01,
|
| gcd-div-rest | proved | all subs proved
| gcd-abs,
divides,
gcd-div1,
|
| max_prime_divisor-nls-03 | proved | all subs proved
| prime-one,
div-mult,
divides,
max_prime_divisor-def,
prime-ex-max,
|
| max_prime_divisor-nls-02 | proved | all subs proved
| prime-not-neg,
prime-small,
div-mult,
prime-not-neg-01,
divides,
max_prime_divisor-def,
prime-ex-max,
|
| max_prime_divisor-nls | proved | all subs proved
| prime-not-neg-01,
max_prime_divisor-def,
prime-ex-max,
|
| abs-not-less | proved | all subs proved
| gcd-com,
gcd-nls,
|
| prime-ex-max | proved | all subs proved
| prime-def-prime,
|
| divides-mult-sub | proved | all subs proved
| div-neg,
divides-mult-add,
|
| gcd-abs-rew | proved | all subs proved
| gcd-abs-rew-02,
|
| gcd-abs-rew-01 | proved | all subs proved
| gcd-abs-rew-02,
|
| gcd-neg | proved | all subs proved
| gcd-abs-rew-02,
|
| gcd-abs | proved | all subs proved
| gcd-zero-02,
|
| gcd-nls | proved | all subs proved
| div-not-ls,
gcd-div1,
gcd-abs-rew-02,
|
| prime-def-prime | proved | all subs proved
| divides-mult-01,
div-mult,
divides,
prime-one,
prime-def,
|
| divides-prime | proved | all subs proved
| div-one,
divides-mone,
div-abs-03,
divides-neg,
div-mult,
divides,
prime-def,
|
| div-one-neg-pos | proved | all subs proved
| div-one,
div-one-one-neg,
|
| divides-abs | proved | all subs proved
| divides-abs-01,
div-abs-02,
|
| gcd-abs-rew-02 | proved | all subs proved
| div-abs-02,
gcd-zero,
gcd-div2,
gcd-div1,
div-abs-01,
gcd-max,
|
| gcd-zero-02 | proved | all subs proved
| gcd-pos,
|
| divides-mult-add | proved | all subs proved
| div-mult,
divides-add,
|
| prime-three | proved | all subs proved
| prime-def-mod,
|
| prime-odd-01 | proved | all subs proved
| prime-two,
|
| prime-odd | proved | all subs proved
| prime-two,
prime-not-neg-01,
|
| prime-not-odd | proved | all subs proved
| prime-two,
prime-two-01,
|
| prime-not-four | proved | all subs proved
| prime-def-mod,
|
| prime-divides-one | proved | all subs proved
| prime-not-neg,
prime-one,
div-one-one,
|
| prime-83 | proved | all subs proved
| case-10,
prime-def-mod,
|
| prime-7 | proved | all subs proved
| prime-def-mod,
|
| prime-631 | proved | all subs proved
| case-10,
case-20,
case-30,
prime-def-mod,
|
| prime-5 | proved | all subs proved
| prime-def-mod,
|
| prime-43 | proved | all subs proved
| prime-def-mod,
|
| prime-317 | proved | all subs proved
| case-10,
case-20,
prime-def-mod,
|
| prime-23 | proved | all subs proved
| prime-def-mod,
|
| prime-163 | proved | all subs proved
| case-10,
prime-def-mod,
|
| prime-13 | proved | all subs proved
| prime-def-mod,
|
| prime-1259 | proved | all subs proved
| case-10,
case-20,
case-30,
case-40,
prime-def-mod,
|
| prime-11 | proved | all subs proved
| prime-def-mod,
|
| gcd-divides | proved | all subs proved
| divides-mult-01,
gcd-div1,
|
| div-one-pos | proved | all subs proved
| div-one,
div-one-one,
|
| prime-two | proved | all subs proved
| div-mult,
prime-def,
prime-two-01,
|
| prime-def-mod | proved | all subs proved
| divides,
div-mult,
prime-def,
|
| div-zero-zero | proved | all subs proved
| divides,
div-zero-01,
|
| prime-abs | proved | all subs proved
| prime-not-neg,
|
| div-abs-01 | proved | all subs proved
| div-mult,
divides,
|
| div-abs-03 | proved | all subs proved
| div-zero,
div-neg,
|
| div-abs-02 | proved | all subs proved
| div-abs,
divides,
|
| divides-abs-01 | proved | all subs proved
| div-abs,
divides,
|
| div-one-one | proved | all subs proved
| divides-mone,
div-one,
divides,
|
| div-one-one-neg | proved | all subs proved
| divides-mone,
div-one,
divides,
|
| gcd-pos | proved | all subs proved
| gcd-zero,
div-one,
gcd-max,
|
| divides-add | proved | all subs proved
| div-mult,
divides,
|
| divides-mult-01 | proved | all subs proved
| div-mult,
divides,
|
| not-less-gcd | proved | all subs proved
| div-not-ls,
gcd-div1,
|
| prime-mult-not | proved | all subs proved
| div-mult,
prime-def,
|
| prime-le-2 | proved | all subs proved
| prime-small,
|
| divides-mult-02 | proved | all subs proved
| div-mult,
divides,
|
| divides-minus | proved | all subs proved
| div-neg,
|
| div-mult-01 | proved | all subs proved
| divides-mult,
|
| div-mod-zero-01 | proved | all subs proved
| div-mult,
|
| div-mod | proved | all subs proved
| div-neg,
div-mod-01,
|
| div-abs-04 | proved | all subs proved
| div-zero,
divides,
|
| prime-two-01 | proved | all subs proved
| prime-def,
|
| prime-small | proved | all subs proved
| prime-def,
|
| prime-not-neg | proved | all subs proved
| prime-def,
|
| prime-not-neg-01 | proved | all subs proved
| prime-def,
|
| prime-one | proved | all subs proved
| prime-def,
|
| div-mod-zero | proved | all subs proved
| divides,
|
| div-eq-one | proved | all subs proved
| divides,
|
| gcd-less | proved | all subs proved
| gcd-max,
|
| div-not-ls | proved | all subs proved
| divides,
|
| div-mult-shift | proved | all subs proved
| divides,
|
| div-eq | proved | all subs proved
| divides,
|
| mod-gcd | proved | all subs proved
| divides,
gcd-div1,
|
| divides-neg | proved | all subs proved
| divides,
|
| div-zero-01 | proved | all subs proved
| divides,
|
| divides-mone | proved | all subs proved
| divides,
|
| div-one | proved | all subs proved
| divides,
|
| divides-mult | proved | all subs proved
| divides,
|
| div-mod-01 | proved | all subs proved
| divides,
|
| div-neg | proved | all subs proved
| divides,
|
| div-zero | proved | all subs proved
| divides,
|
| div-abs | proved | all subs proved
| divides,
|
| div-mult | proved | all subs proved
| divides,
|
| gcd-com | proved | all subs proved
| gcd-zero,
gcd-div1,
gcd-div2,
gcd-max,
|
| divides-mod | proved | all subs proved
| divides,
|
| divides-abs-02 | proved | all subs proved
| divides,
|
| div-mult-div | proved | all subs proved
| divides,
|
| div-div-01 | proved | all subs proved
| divides,
|
| div-div | proved | all subs proved
| divides,
|
| case-40 | proved | all subs proved
| |
| case-30 | proved | all subs proved
| |
| case-20 | proved | all subs proved
| |
| case-10 | proved | all subs proved
| |
| max_prime_divisor-def | axiom | | |
| gcdex-not-unique | proved | all subs proved
| |
| gcd-max | axiom | | |
| gcd-div2 | axiom | | |
| gcd-div1 | axiom | | |
| prime-def | axiom | | |
| gcd-zero | axiom | | |
| divides | axiom | | |