Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2106 class class class wbr 5103
(class class class)co 7349 0cc0 10984
+∞cpnf 11119 ℝ*cxr 11121 ≤
cle 11123 [,]cicc 13195 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7662 ax-cnex 11040 ax-resscn 11041 ax-1cn 11042 ax-addrcl 11045 ax-rnegex 11055 ax-cnre 11057 ax-pre-lttri 11058 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5528 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-ov 7352 df-oprab 7353 df-mpo 7354 df-er 8581 df-en 8817 df-dom 8818 df-sdom 8819 df-pnf 11124 df-mnf 11125 df-xr 11126 df-ltxr 11127 df-le 11128 df-icc 13199 |
This theorem is referenced by: xrge0subm
20761 itg2const2
25028 itg2splitlem
25035 itg2split
25036 itg2gt0
25047 itg2cnlem2
25049 itg2cn
25050 iblss
25091 itgle
25096 itgeqa
25100 ibladdlem
25106 iblabs
25115 iblabsr
25116 iblmulc2
25117 bddmulibl
25125 bddiblnc
25128 xrge0infss
31459 xrge00
31671 unitssxrge0
32254 xrge0mulc1cn
32295 esum0
32421 esumpad
32427 esumpad2
32428 esumrnmpt2
32440 esumpinfval
32445 esummulc1
32453 ddemeas
32608 oms0
32670 itg2gt0cn
36028 ibladdnclem
36029 iblabsnc
36037 iblmulc2nc
36038 ftc1anclem7
36052 ftc1anclem8
36053 ftc1anc
36054 iblsplit
43960 gsumge0cl
44365 sge0cl
44375 sge0ss
44406 0ome
44523 ovnf
44557 |