![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexr | Structured version Visualization version GIF version |
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
rexr | ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr 10246 | . 2 ⊢ ℝ ⊆ ℝ* | |
2 | 1 | sseli 3728 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2127 ℝcr 10098 ℝ*cxr 10236 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-v 3330 df-un 3708 df-in 3710 df-ss 3717 df-xr 10241 |
This theorem is referenced by: rexri 10260 lenlt 10279 ltpnf 12118 mnflt 12121 xrltnsym 12134 xrlttr 12137 xrre 12164 xrre3 12166 max1 12180 max2 12182 min1 12184 min2 12185 maxle 12186 lemin 12187 maxlt 12188 ltmin 12189 max0sub 12191 qbtwnxr 12195 xralrple 12200 alrple 12201 xltnegi 12211 rexadd 12227 xaddnemnf 12231 xaddnepnf 12232 xaddcom 12235 xnegdi 12242 xpncan 12245 xnpcan 12246 xleadd1a 12247 xleadd1 12249 xltadd1 12250 xltadd2 12251 xsubge0 12255 rexmul 12265 xadddilem 12288 xadddir 12290 xrsupsslem 12301 xrinfmsslem 12302 xrub 12306 supxrun 12310 supxrunb1 12313 supxrunb2 12314 supxrbnd1 12315 supxrbnd2 12316 xrsup0 12317 supxrbnd 12322 infmremnf 12337 elioo4g 12398 elioc2 12400 elico2 12401 elicc2 12402 iccss 12405 iooshf 12416 iooneg 12456 icoshft 12458 difreicc 12468 hashbnd 13288 elicc4abs 14229 icodiamlt 14344 limsupgord 14373 pcadd 15766 ramubcl 15895 lt6abl 18467 xrsmcmn 19942 xrs1mnd 19957 xrs10 19958 xrsdsreval 19964 psmetge0 22289 xmetge0 22321 imasdsf1olem 22350 bl2in 22377 blssps 22401 blss 22402 blcld 22482 icopnfcld 22743 iocmnfcld 22744 bl2ioo 22767 blssioo 22770 xrtgioo 22781 xrsblre 22786 iccntr 22796 icccmplem2 22798 icccmp 22800 reconnlem2 22802 xrge0tsms 22809 icoopnst 22910 iocopnst 22911 ovolfioo 23407 ovolicc2lem1 23456 ovolicc2lem5 23460 voliunlem3 23491 icombl1 23502 icombl 23503 iccvolcl 23506 ovolioo 23507 ioovolcl 23509 uniiccdif 23517 volsup2 23544 mbfimasn 23571 ismbf3d 23591 mbfsup 23601 itg2seq 23679 dvlip2 23928 ply1remlem 24092 abelthlem3 24357 abelth 24365 sincosq2sgn 24421 sincosq3sgn 24422 sinq12ge0 24430 sincos6thpi 24437 sineq0 24443 efif1olem1 24458 efif1olem2 24459 efif1o 24462 eff1o 24465 loglesqrt 24669 basellem1 24977 pntlemo 25466 nmobndi 27910 nmopub2tALT 29048 nmfnleub2 29065 nmopcoadji 29240 rexdiv 29914 xrge0tsmsd 30065 pnfneige0 30277 lmxrge0 30278 hashf2 30426 sxbrsigalem0 30613 omssubadd 30642 orvcgteel 30809 orvclteel 30814 sgnclre 30881 sgnneg 30882 signstfvneq0 30929 ivthALT 32607 icorempt2 33481 icoreunrn 33489 iooelexlt 33492 relowlssretop 33493 relowlpssretop 33494 poimir 33724 mblfinlem2 33729 iblabsnclem 33755 bddiblnc 33762 ftc1anclem1 33767 ftc1anclem6 33772 areacirclem5 33786 areacirc 33787 blbnd 33868 iocmbl 38269 supxrre3 40008 supxrgere 40016 infrpge 40034 infxrunb2 40051 infxrbnd2 40052 infleinflem2 40054 xrralrecnnle 40069 supxrunb3 40090 supminfxr2 40166 xrpnf 40183 ioomidp 40212 limsupre 40345 limsupub 40408 limsuppnflem 40414 limsupre3lem 40436 liminfgord 40458 liminflelimsuplem 40479 limsupgtlem 40481 xlimmnfvlem2 40531 xlimmnfv 40532 xlimpnfvlem2 40535 xlimpnfv 40536 icccncfext 40572 volioc 40660 volico 40672 fourierdlem113 40908 meaiuninclem 41169 meaiuninc3v 41173 icoresmbl 41232 ovolval5lem1 41341 mbfresmf 41423 cnfsmf 41424 incsmf 41426 smfconst 41433 decsmf 41450 smfres 41472 smfco 41484 issmfle2d 41490 bgoldbtbndlem3 42174 |
Copyright terms: Public domain | W3C validator |