![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexr | Structured version Visualization version Unicode version |
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
rexr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr 9702 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3414 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-v 3033 df-un 3395 df-in 3397 df-ss 3404 df-xr 9697 |
This theorem is referenced by: rexri 9711 lenlt 9730 ltpnf 11445 mnflt 11448 xrltnsym 11459 xrlttr 11462 xrre 11487 xrre3 11489 max1 11503 max2 11505 min1 11506 min2 11507 maxle 11508 lemin 11509 maxlt 11510 ltmin 11511 max0sub 11512 qbtwnxr 11516 xralrple 11521 alrple 11522 xltnegi 11532 rexadd 11548 xaddnemnf 11551 xaddnepnf 11552 xaddcom 11555 xnegdi 11559 xpncan 11562 xnpcan 11563 xleadd1a 11564 xleadd1 11566 xltadd1 11567 xltadd2 11568 xsubge0 11572 rexmul 11582 xadddilem 11605 xadddir 11607 xrsupsslem 11617 xrinfmsslem 11618 xrub 11622 supxrun 11626 supxrunb1 11630 supxrunb2 11631 supxrbnd1 11632 supxrbnd2 11633 xrsup0 11634 supxrbnd 11639 infmremnf 11658 elioo4g 11720 elioc2 11722 elico2 11723 elicc2 11724 iccss 11727 iooshf 11738 iooneg 11778 icoshft 11780 difreicc 11790 hashbnd 12559 elicc4abs 13459 icodiamlt 13574 limsupgord 13605 pcadd 14913 ramubcl 15055 lt6abl 17607 xrsmcmn 19068 xrs1mnd 19083 xrs10 19084 xrsdsreval 19090 psmetge0 21406 xmetge0 21437 imasdsf1olem 21466 bl2in 21493 blssps 21517 blss 21518 blcld 21598 icopnfcld 21866 iocmnfcld 21867 bl2ioo 21888 blssioo 21891 xrtgioo 21902 xrsblre 21907 iccntr 21917 icccmplem2 21919 icccmp 21921 reconnlem2 21923 xrge0tsms 21930 icoopnst 22045 iocopnst 22046 ovolfioo 22498 ovolicc2lem1 22548 ovolicc2lem5 22553 voliunlem3 22584 icombl1 22595 icombl 22596 iccvolcl 22599 ovolioo 22600 ioovolcl 22601 uniiccdif 22614 volsup2 22642 mbfimasn 22669 ismbf3d 22689 mbfsup 22699 itg2seq 22779 dvlip2 23026 ply1remlem 23192 abelthlem3 23467 abelth 23475 sincosq2sgn 23533 sincosq3sgn 23534 sinq12ge0 23542 sincos6thpi 23549 sineq0 23555 efif1olem1 23570 efif1olem2 23571 efif1o 23574 eff1o 23577 loglesqrt 23777 basellem1 24086 pntlemo 24524 nmobndi 26497 nmopub2tALT 27643 nmfnleub2 27660 nmopcoadji 27835 rexdiv 28470 xrge0tsmsd 28622 pnfneige0 28831 lmxrge0 28832 hashf2 28979 sxbrsigalem0 29166 omssubadd 29201 omssubaddOLD 29205 orvcgteel 29373 orvclteel 29378 sgnclre 29483 sgnneg 29484 signstfvneq0 29533 ivthALT 31062 icorempt2 31824 icoreunrn 31832 iooelexlt 31835 relowlssretop 31836 relowlpssretop 31837 poimir 32037 mblfinlem2 32042 iblabsnclem 32069 bddiblnc 32076 ftc1anclem1 32081 ftc1anclem6 32086 areacirclem5 32100 areacirc 32101 blbnd 32183 iocmbl 36168 supxrre3 37635 supxrgere 37643 infrpge 37661 infxrunb2 37678 infxrbnd2 37679 infleinflem2 37681 ioomidp 37711 limsupre 37818 limsupreOLD 37819 icccncfext 37862 volioc 37946 volico 37958 fourierdlem113 38195 icoresmbl 38483 ovolval5lem1 38592 bgoldbtbndlem3 39047 |
Copyright terms: Public domain | W3C validator |