Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
ℝcr 11051 ℝ*cxr 11189 |
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 2708 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-un 3916 df-in 3918 df-ss 3928 df-xr 11194 |
This theorem is referenced by: rexri
11214 lenlt
11234 ltpnf
13042 mnflt
13045 xrltnsym
13057 xrlttr
13060 xrre
13089 xrre3
13091 max1
13105 max2
13107 min1
13109 min2
13110 maxle
13111 lemin
13112 maxlt
13113 ltmin
13114 max0sub
13116 qbtwnxr
13120 xralrple
13125 alrple
13126 xltnegi
13136 rexadd
13152 xaddnemnf
13156 xaddnepnf
13157 xaddcom
13160 xnegdi
13168 xpncan
13171 xnpcan
13172 xleadd1a
13173 xleadd1
13175 xltadd1
13176 xltadd2
13177 xsubge0
13181 rexmul
13191 xadddilem
13214 xadddir
13216 xrsupsslem
13227 xrinfmsslem
13228 xrub
13232 supxrun
13236 supxrunb1
13239 supxrunb2
13240 supxrbnd1
13241 supxrbnd2
13242 xrsup0
13243 supxrbnd
13248 infmremnf
13263 elioo4g
13325 elioc2
13328 elico2
13329 elicc2
13330 iccss
13333 iooshf
13344 iooneg
13389 icoshft
13391 difreicc
13402 hashbnd
14237 elicc4abs
15205 icodiamlt
15321 limsupgord
15355 pcadd
16762 ramubcl
16891 lt6abl
19673 xrsmcmn
20823 xrs1mnd
20838 xrs10
20839 xrsdsreval
20845 psmetge0
23668 xmetge0
23700 imasdsf1olem
23729 bl2in
23756 blssps
23780 blss
23781 blcld
23864 icopnfcld
24134 iocmnfcld
24135 bl2ioo
24158 blssioo
24161 xrtgioo
24172 xrsblre
24177 iccntr
24187 icccmplem2
24189 icccmp
24191 reconnlem2
24193 xrge0tsms
24200 icoopnst
24305 iocopnst
24306 ovolfioo
24834 ovolicc2lem1
24884 ovolicc2lem5
24888 voliunlem3
24919 icombl1
24930 icombl
24931 iccvolcl
24934 ovolioo
24935 ioovolcl
24937 uniiccdif
24945 volsup2
24972 mbfimasn
24999 ismbf3d
25021 mbfsup
25031 itg2seq
25110 bddiblnc
25209 dvlip2
25362 ply1remlem
25530 abelthlem3
25795 abelth
25803 sincosq2sgn
25859 sincosq3sgn
25860 sinq12ge0
25868 sincos6thpi
25875 sineq0
25883 efif1olem1
25901 efif1olem2
25902 efif1o
25905 eff1o
25908 loglesqrt
26114 basellem1
26433 pntlemo
26958 nmobndi
29720 nmopub2tALT
30854 nmfnleub2
30871 nmopcoadji
31046 rexdiv
31785 xrge0tsmsd
31902 pnfneige0
32535 lmxrge0
32536 hashf2
32686 sxbrsigalem0
32874 orvcgteel
33070 orvclteel
33075 sgnclre
33142 sgnneg
33143 signstfvn
33184 signstfvneq0
33187 signsvfn
33197 ivthALT
34810 icorempo
35825 icoreunrn
35833 iooelexlt
35836 relowlssretop
35837 relowlpssretop
35838 poimir
36114 mblfinlem2
36119 iblabsnclem
36144 ftc1anclem1
36154 ftc1anclem6
36159 areacirclem5
36173 areacirc
36174 blbnd
36249 iocmbl
41550 reabssgn
41915 supxrre3
43566 supxrgere
43574 infrpge
43592 infxrunb2
43609 infxrbnd2
43610 infleinflem2
43612 xrralrecnnle
43624 supxrunb3
43641 supminfxr2
43711 xrpnf
43728 ioomidp
43759 limsupre
43889 limsupub
43952 limsuppnflem
43958 limsupre3lem
43980 liminfgord
44002 liminflelimsuplem
44023 limsupgtlem
44025 limsupub2
44060 xlimpnfxnegmnf
44062 xlimmnfvlem2
44081 xlimmnfv
44082 xlimpnfvlem2
44085 xlimpnfv
44086 icccncfext
44135 volioc
44220 volico
44231 fourierdlem113
44467 meaiuninclem
44728 meaiuninc3v
44732 icoresmbl
44791 ovolval5lem1
44900 mbfresmf
44987 cnfsmf
44988 incsmf
44990 smfconst
44997 decsmf
45015 smfres
45038 smfco
45050 issmfle2d
45057 finfdm
45094 bgoldbtbndlem3
46006 rrxsphere
46841 i0oii
46959 io1ii
46960 |