Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
↔ wb 205 ∧
wa 397 ∈ wcel 2107
class class class wbr 5106 ℝ*cxr 11193 <
clt 11194 ≤ cle 11195 |
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-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-br 5107 df-opab 5169 df-xp 5640 df-cnv 5642 df-le 11200 |
This theorem is referenced by: xrletri
13078 qextltlem
13127 xralrple
13130 xltadd1
13181 xsubge0
13186 xposdif
13187 xltmul1
13217 ioo0
13295 ico0
13316 ioc0
13317 snunioo
13401 snunioc
13403 difreicc
13407 hashbnd
14242 limsuplt
15367 pcadd
16766 pcadd2
16767 ramubcl
16895 ramlb
16896 leordtvallem1
22577 leordtvallem2
22578 leordtval2
22579 leordtval
22580 lecldbas
22586 blcld
23877 stdbdbl
23889 tmsxpsval2
23911 iocmnfcld
24148 xrsxmet
24188 metdsge
24228 bndth
24337 ovolgelb
24860 ovolunnul
24880 ioombl
24945 volsup2
24985 mbfmax
25029 ismbf3d
25034 itg2seq
25123 itg2monolem2
25132 itg2monolem3
25133 lhop2
25395 mdegleb
25445 deg1ge
25479 deg1add
25484 ig1pdvds
25557 plypf1
25589 radcnvlt1
25793 upgrfi
28084 xrdifh
31730 xrge00
31926 gsumesum
32715 itg2gt0cn
36179 asindmre
36207 dvasin
36208 radcnvrat
42682 supxrgelem
43658 infrpge
43672 xrlexaddrp
43673 xrltnled
43684 xrpnf
43807 gtnelioc
43815 ltnelicc
43821 gtnelicc
43824 snunioo1
43836 eliccnelico
43853 xrgtnelicc
43862 lptioo2
43958 stoweidlem34
44361 fourierdlem20
44454 fouriersw
44558 nltle2tri
45631 iccelpart
45711 |