Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Vcvv 3448
∪ cun 3913 {cpr 4593
ℝcr 11057 +∞cpnf 11193 -∞cmnf 11194
ℝ*cxr 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 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 ax-un 7677 ax-cnex 11114 ax-resscn 11115 |
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 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-sn 4592 df-pr 4594 df-uni 4871 df-xr 11200 |
This theorem is referenced by: ixxval
13279 ixxf
13281 ixxex
13282 limsuple
15367 limsuplt
15368 limsupbnd1
15371 prdsds
17353 letsr
18489 xrsbas
20829 xrsadd
20830 xrsmul
20831 xrsle
20833 xrs1mnd
20851 xrs10
20852 xrs1cmn
20853 xrge0subm
20854 xrge0cmn
20855 xrsds
20856 znle
20955 leordtval2
22579 lecldbas
22586 ispsmet
23673 isxmet
23693 imasdsf1olem
23742 blfvalps
23752 nmoffn
24091 nmofval
24094 xrsxmet
24188 xrge0gsumle
24212 xrge0tsms
24213 xrlimcnp
26334 xrge00
31919 xrge0tsmsd
31941 xrhval
32639 icof
43514 elicores
43845 fuzxrpmcn
44143 gsumge0cl
44686 ovnval2b
44867 volicorescl
44868 ovnsubaddlem1
44885 |