![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1xr | Structured version Visualization version GIF version |
Description: 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
Ref | Expression |
---|---|
1xr | ⊢ 1 ∈ ℝ* |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 11154 | . 2 ⊢ 1 ∈ ℝ | |
2 | 1 | rexri 11212 | 1 ⊢ 1 ∈ ℝ* |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 1c1 11051 ℝ*cxr 11187 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-1cn 11108 ax-icn 11109 ax-addcl 11110 ax-mulcl 11112 ax-mulrcl 11113 ax-i2m1 11118 ax-1ne0 11119 ax-rrecex 11122 ax-cnre 11123 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-iota 6448 df-fv 6504 df-ov 7359 df-xr 11192 |
This theorem is referenced by: xmulid1 13197 xmulid2 13198 xmulm1 13199 x2times 13217 xov1plusxeqvd 13414 ico01fl0 13723 hashge1 14288 hashgt12el 14321 hashgt12el2 14322 hashgt23el 14323 sgn1 14976 fprodge1 15877 halfleoddlt 16243 isnzr2hash 20732 0ringnnzr 20737 xrsnsgrp 20831 leordtval2 22561 unirnblps 23770 unirnbl 23771 mopnex 23873 dscopn 23927 nmoid 24104 xrsmopn 24173 zdis 24177 metnrmlem1a 24219 metnrmlem1 24220 icopnfcnv 24303 icopnfhmeo 24304 iccpnfcnv 24305 iccpnfhmeo 24306 cncmet 24684 itg2monolem1 25113 itg2monolem3 25115 abelthlem2 25789 abelthlem3 25790 abelthlem5 25792 abelthlem7 25795 abelth 25798 dvlog2lem 26005 dvlog2 26006 logtayl 26013 logtayl2 26015 scvxcvx 26333 pntibndlem1 26935 pntibndlem2 26937 pntibnd 26939 pntlemc 26941 pnt 26960 padicabvf 26977 padicabvcxp 26978 elntg2 27932 nmopun 30954 pjnmopi 31088 xlt2addrd 31658 xdivrec 31778 xrsmulgzz 31864 xrnarchi 32015 unitssxrge0 32472 xrge0iifcnv 32505 xrge0iifiso 32507 xrge0iifhom 32509 hasheuni 32675 ddemeas 32826 omssubadd 32891 prob01 33004 lfuhgr2 33703 dnizeq0 34929 iccioo01 35789 broucube 36103 asindmre 36152 dvasin 36153 areacirclem1 36157 imo72b2 42427 cvgdvgrat 42575 supxrgelem 43547 xrlexaddrp 43562 infxr 43577 infleinflem2 43581 limsup10exlem 43985 limsup10ex 43986 liminf10ex 43987 salexct2 44552 salgencntex 44556 ovn0lem 44778 expnegico01 46571 regt1loggt0 46594 rege1logbrege0 46616 rege1logbzge0 46617 dignnld 46661 eenglngeehlnmlem1 46795 eenglngeehlnmlem2 46796 iooii 46922 i0oii 46924 sepfsepc 46932 seppcld 46934 |
Copyright terms: Public domain | W3C validator |