Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Vcvv 3475
∪ cun 3947 {cpr 4631
ℝcr 11109 +∞cpnf 11245 -∞cmnf 11246
ℝ*cxr 11247 |
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 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-sn 4630 df-pr 4632 df-uni 4910 df-xr 11252 |
This theorem is referenced by: ixxval
13332 ixxf
13334 ixxex
13335 limsuple
15422 limsuplt
15423 limsupbnd1
15426 prdsds
17410 letsr
18546 xrsbas
20961 xrsadd
20962 xrsmul
20963 xrsle
20965 xrs1mnd
20983 xrs10
20984 xrs1cmn
20985 xrge0subm
20986 xrge0cmn
20987 xrsds
20988 znle
21088 leordtval2
22716 lecldbas
22723 ispsmet
23810 isxmet
23830 imasdsf1olem
23879 blfvalps
23889 nmoffn
24228 nmofval
24231 xrsxmet
24325 xrge0gsumle
24349 xrge0tsms
24350 xrlimcnp
26473 xrge00
32187 xrge0tsmsd
32209 xrhval
32998 icof
43918 elicores
44246 fuzxrpmcn
44544 gsumge0cl
45087 ovnval2b
45268 volicorescl
45269 ovnsubaddlem1
45286 |