Colors of
variables: wff
setvar class |
Syntax hints:
โ wcel 2104 (class class class)co 7303
ยท cmul 10918 โ0cn0 12275 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7616 ax-resscn 10970 ax-1cn 10971 ax-icn 10972 ax-addcl 10973 ax-addrcl 10974 ax-mulcl 10975 ax-mulrcl 10976 ax-mulcom 10977 ax-addass 10978 ax-mulass 10979 ax-distr 10980 ax-i2m1 10981 ax-1ne0 10982 ax-1rid 10983 ax-rnegex 10984 ax-rrecex 10985 ax-cnre 10986 ax-pre-lttri 10987 ax-pre-lttrn 10988 ax-pre-ltadd 10989 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5496 df-eprel 5502 df-po 5510 df-so 5511 df-fr 5551 df-we 5553 df-xp 5602 df-rel 5603 df-cnv 5604 df-co 5605 df-dm 5606 df-rn 5607 df-res 5608 df-ima 5609 df-pred 6213 df-ord 6280 df-on 6281 df-lim 6282 df-suc 6283 df-iota 6406 df-fun 6456 df-fn 6457 df-f 6458 df-f1 6459 df-fo 6460 df-f1o 6461 df-fv 6462 df-ov 7306 df-om 7741 df-2nd 7860 df-frecs 8124 df-wrecs 8155 df-recs 8229 df-rdg 8268 df-er 8525 df-en 8761 df-dom 8762 df-sdom 8763 df-pnf 11053 df-mnf 11054 df-ltxr 11056 df-nn 12016 df-n0 12276 |
This theorem is referenced by: numnncl
12489 num0u
12490 numcl
12492 numsuc
12493 numlt
12504 decle
12513 decrmanc
12536 decsubi
12542 decmul1
12543 decmulnc
12546 decmul10add
12548 expnass
13966 nn0opthlem1
14024 faclbnd4lem1
14049 dec2dvds
16805 dec5dvds
16806 gcdi
16815 decexp2
16817 decsplit
16825 log2ublem1
26137 log2ublem2
26138 log2ublem3
26139 log2ub
26140 bclbnd
26469 dpmul
31228 sqn5i
40349 decpmulnc
40351 decpmul
40352 sqdeccom12
40353 |