Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2105
class class class wbr 5149 (class class class)co 7412
ℝcr 11112 + caddc 11116 ≤ cle 11254 |
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 |
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-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-ov 7415 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 |
This theorem is referenced by: lesub3d
11837 supaddc
12186 eluzadd
12856 rpnnen1lem5
12970 xleadd1a
13237 fzoaddel
13690 fladdz
13795 ltdifltdiv
13804 bernneq3
14199 caucvgrlem
15624 eirrlem
16152 vdwlem3
16921 vdwlem9
16927 vdwlem10
16928 2expltfac
17031 pcoass
24772 trirn
25149 minveclem2
25175 ovolfiniun
25251 ovolshftlem1
25259 unmbl
25287 uniioombllem5
25337 opnmbllem
25351 vitalilem2
25359 itg2split
25500 dvfsumlem2
25777 dvfsumlem4
25779 dvfsum2
25784 fta1glem2
25917 coemullem
25997 fta1lem
26053 leibpi
26680 log2tlbnd
26683 jensenlem2
26725 harmonicubnd
26747 harmonicbnd4
26748 lgamgulmlem5
26770 lgambdd
26774 ppiub
26940 bposlem5
27024 mulog2sumlem2
27271 selberg2lem
27286 chpdifbndlem1
27289 pntrlog2bndlem2
27314 pntpbnd2
27323 pntibndlem2
27327 pntlemg
27334 pntlemk
27342 pntlemo
27343 qabvle
27361 ostth2lem3
27371 minvecolem2
30392 nndiffz1
32261 wrdt2ind
32381 cycpmco2lem6
32557 reofld
32726 dya2icoseg
33571 resconn
34532 gg-dvfsumlem2
35470 poimirlem15
36807 opnmbllem0
36828 itg2addnclem3
36845 bfplem2
36995 lcmineqlem19
41219 aks4d1p1p4
41243 aks4d1p1p7
41246 sticksstones12
41281 metakunt2
41293 pellexlem2
41871 rmygeid
42006 jm3.1lem2
42060 fzisoeu
44310 absnpncan2d
44312 absnpncan3d
44317 leadd12dd
44326 iccshift
44531 fsumnncl
44588 climsuselem1
44623 sumnnodd
44646 climleltrp
44692 dvbdfbdioolem2
44945 ioodvbdlimc1lem1
44947 ioodvbdlimc1lem2
44948 ioodvbdlimc2lem
44950 dvnmul
44959 iblspltprt
44989 itgspltprt
44995 itgiccshift
44996 itgperiod
44997 stoweidlem1
45017 stoweidlem11
45027 stoweidlem14
45030 stoweidlem26
45042 stoweidlem44
45060 stirlinglem11
45100 fourierdlem10
45133 fourierdlem11
45134 fourierdlem15
45138 fourierdlem30
45153 fourierdlem42
45165 fourierdlem68
45190 fourierdlem79
45201 fourierdlem92
45214 sge0xaddlem1
45449 carageniuncllem2
45538 hoidmv1lelem1
45607 ovolval5lem1
45668 smfmullem1
45807 |