Colors of
variables: wff
setvar class |
Syntax hints:
Or wor 5588 ℝ*cxr 11247 <
clt 11248 |
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 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 |
This theorem is referenced by: xrlttri2
13121 xrlttri3
13122 xrltne
13142 xmullem
13243 xmulasslem
13264 supxr
13292 supxrcl
13294 supxrun
13295 supxrmnf
13296 supxrunb1
13298 supxrunb2
13299 supxrub
13303 supxrlub
13304 infxrcl
13312 infxrlb
13313 infxrgelb
13314 xrinf0
13317 infmremnf
13322 limsupval
15418 limsupgval
15420 limsupgre
15425 ramval
16941 ramcl2lem
16942 prdsdsfn
17411 prdsdsval
17424 imasdsfn
17460 imasdsval
17461 prdsmet
23876 xpsdsval
23887 prdsbl
24000 tmsxpsval2
24048 nmoval
24232 xrge0tsms2
24351 metdsval
24363 iccpnfhmeo
24461 xrhmeo
24462 ovolval
24990 ovolf
24999 ovolctb
25007 itg2val
25246 mdegval
25581 mdegldg
25584 mdegxrf
25586 mdegcl
25587 aannenlem2
25842 nmooval
30016 nmoo0
30044 nmopval
31109 nmfnval
31129 nmop0
31239 nmfn0
31240 xrsupssd
31972 xrge0infssd
31974 infxrge0lb
31977 infxrge0glb
31978 infxrge0gelb
31979 xrsclat
32181 xrge0iifiso
32915 esumval
33044 esumnul
33046 esum0
33047 gsumesum
33057 esumsnf
33062 esumpcvgval
33076 esum2d
33091 omsfval
33293 omsf
33295 oms0
33296 omssubaddlem
33298 omssubadd
33299 mblfinlem2
36526 ovoliunnfl
36530 voliunnfl
36532 volsupnfl
36533 itg2addnclem
36539 radcnvrat
43073 infxrglb
44050 xrgtso
44055 infxr
44077 infxrunb2
44078 infxrpnf
44156 limsup0
44410 limsuppnfdlem
44417 limsupequzlem
44438 supcnvlimsup
44456 limsuplt2
44469 liminfval
44475 limsupge
44477 liminfgval
44478 liminfval2
44484 limsup10ex
44489 liminf10ex
44490 liminflelimsuplem
44491 cnrefiisplem
44545 etransclem48
44998 sge0val
45082 sge0z
45091 sge00
45092 sge0sn
45095 sge0tsms
45096 ovnval2
45261 smflimsuplem1
45536 smflimsuplem2
45537 smflimsuplem4
45539 smflimsuplem7
45542 |