Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 ∧ wa 397
∈ wcel 2107 class class class wbr 5106
(class class class)co 7358 ℝcr 11051
0cc0 11052 +∞cpnf 11187
≤ cle 11191 [,)cico 13267 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 ax-cnex 11108 ax-resscn 11109 ax-1cn 11110 ax-addrcl 11113 ax-rnegex 11123 ax-cnre 11125 ax-pre-lttri 11126 ax-pre-lttrn 11127 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-po 5546 df-so 5547 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-ov 7361 df-oprab 7362 df-mpo 7363 df-er 8649 df-en 8885 df-dom 8886 df-sdom 8887 df-pnf 11192 df-mnf 11193 df-xr 11194 df-ltxr 11195 df-le 11196 df-ico 13271 |
This theorem is referenced by: nn0rp0
13373 rge0ssre
13374 0e0icopnf
13376 ge0addcl
13378 ge0mulcl
13379 fsumge0
15681 fprodge0
15877 isabvd
20282 abvge0
20287 nmolb
24084 nmoge0
24088 nmoi
24095 icopnfcnv
24308 cphsqrtcl
24551 tcphcph
24604 cphsscph
24618 ovolfsf
24838 ovolmge0
24844 ovolunlem1a
24863 ovoliunlem1
24869 ovolicc2lem4
24887 ioombl1lem4
24928 uniioombllem2
24950 uniioombllem6
24955 0plef
25039 i1fpos
25074 mbfi1fseqlem1
25083 mbfi1fseqlem3
25085 mbfi1fseqlem4
25086 mbfi1fseqlem5
25087 mbfi1fseqlem6
25088 mbfi1flimlem
25090 itg2const
25108 itg2const2
25109 itg2mulclem
25114 itg2mulc
25115 itg2monolem1
25118 itg2mono
25121 itg2addlem
25126 itg2gt0
25128 itg2cnlem1
25129 itg2cnlem2
25130 itg2cn
25131 iblconst
25185 itgconst
25186 ibladdlem
25187 itgaddlem1
25190 iblabslem
25195 iblabs
25196 iblmulc2
25198 itgmulc2lem1
25199 bddmulibl
25206 bddiblnc
25209 itggt0
25211 itgcn
25212 dvge0
25373 dvle
25374 dvfsumrlim
25398 cxpcn3lem
26103 cxpcn3
26104 resqrtcn
26105 loglesqrt
26114 areaf
26314 areacl
26315 areage0
26316 rlimcnp3
26320 jensenlem2
26340 jensen
26341 amgmlem
26342 amgm
26343 dchrisumlem3
26842 dchrmusumlema
26844 dchrmusum2
26845 dchrvmasumlem2
26849 dchrvmasumiflem1
26852 dchrisum0lema
26865 dchrisum0lem1b
26866 dchrisum0lem1
26867 dchrisum0lem2
26869 axcontlem2
27917 axcontlem7
27922 axcontlem8
27923 axcontlem10
27925 rge0scvg
32533 esumpcvgval
32680 hasheuni
32687 esumcvg
32688 sibfof
32943 mbfposadd
36128 itg2addnclem2
36133 itg2addnclem3
36134 itg2addnc
36135 itg2gt0cn
36136 ibladdnclem
36137 itgaddnclem1
36139 iblabsnclem
36144 iblabsnc
36145 iblmulc2nc
36146 itgmulc2nclem1
36147 itggt0cn
36151 ftc1anclem3
36156 ftc1anclem4
36157 ftc1anclem5
36158 ftc1anclem6
36159 ftc1anclem7
36160 ftc1anclem8
36161 areacirclem2
36170 sge0iunmptlemfi
44661 digvalnn0
46692 nn0digval
46693 dignn0fr
46694 dig2nn1st
46698 digexp
46700 2sphere
46842 itsclc0
46864 itsclc0b
46865 |