Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2105
(class class class)co 7412 ℝcr 11112
/ cdiv 11876 ℝ+crp 12979 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-er 8706 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-rp 12980 |
This theorem is referenced by: iccf1o
13478 xov1plusxeqvd
13480 expmulnbnd
14203 discr
14208 geomulcvg
15827 mertenslem1
15835 retanhcl
16107 bitsfzolem
16380 bitsfzo
16381 bitsmod
16382 odmodnn0
19450 nmoi
24466 nmoleub
24469 icopnfcnv
24688 nmoleub2lem
24862 nmoleub2lem3
24863 pjthlem1
25186 ovolscalem1
25263 ovolscalem2
25264 ovolsca
25265 mbfmulc2lem
25397 itg2const2
25492 dvferm1lem
25734 abelthlem7
26183 logdivlti
26361 logdivle
26363 logcnlem3
26385 logcnlem4
26386 advlogexp
26396 cxpaddle
26493 cxploglim
26715 cxploglim2
26716 lgamgulmlem2
26767 lgamgulmlem3
26768 lgamucov
26775 ftalem1
26810 ftalem2
26811 basellem3
26820 fsumvma2
26950 chpval2
26954 chpchtsum
26955 chpub
26956 logfacrlim
26960 logexprlim
26961 efexple
27017 bposlem9
27028 chebbnd1lem2
27206 chebbnd1lem3
27207 chtppilim
27211 chpchtlim
27215 chpo1ubb
27217 rplogsumlem1
27220 rplogsumlem2
27221 rpvmasumlem
27223 dchrmusum2
27230 dchrvmasumlem2
27234 dchrisum0fno1
27247 dchrisum0lem1b
27251 dchrisum0lem1
27252 dchrisum0lem2a
27253 rplogsum
27263 mulog2sumlem1
27270 mulog2sumlem2
27271 vmalogdivsum2
27274 vmalogdivsum
27275 2vmadivsumlem
27276 log2sumbnd
27280 selberglem2
27282 selbergb
27285 selberg2b
27288 chpdifbndlem1
27289 selberg3lem1
27293 selberg3lem2
27294 selberg3
27295 selberg4lem1
27296 selberg4
27297 pntrsumo1
27301 selberg3r
27305 selberg4r
27306 selberg34r
27307 pntrlog2bndlem1
27313 pntrlog2bndlem2
27314 pntrlog2bndlem3
27315 pntrlog2bndlem4
27316 pntrlog2bndlem5
27317 pntrlog2bndlem6
27319 pntrlog2bnd
27320 pntpbnd1a
27321 pntpbnd2
27323 pntibndlem2
27327 pntibndlem3
27328 pntlemb
27333 pntlemg
27334 pntlemh
27335 pntlemn
27336 pntlemr
27338 pntlemj
27339 pntlemf
27341 pntlemk
27342 pntlemo
27343 pnt
27350 ostth2lem1
27354 ostth2lem4
27372 ostth3
27374 pjhthlem1
30908 esumcst
33356 dya2iocress
33568 dya2iocbrsiga
33569 dya2icobrsiga
33570 sxbrsigalem2
33580 probmeasb
33724 itg2addnclem3
36845 ftc1anclem7
36871 geomcau
36931 cntotbnd
36968 bfplem1
36994 fltnlta
41708 binomcxplemnotnn0
43418 divlt0gt0d
44296 lefldiveq
44302 ltmod
44654 0ellimcdiv
44665 wallispilem5
45085 stirlingr
45106 dirkercncflem1
45119 fourierdlem65
45187 hoiqssbllem2
45639 |