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 10629 | . 2 ⊢ 1 ∈ ℝ | |
2 | 1 | rexri 10687 | 1 ⊢ 1 ∈ ℝ* |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 1c1 10526 ℝ*cxr 10662 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-mulcl 10587 ax-mulrcl 10588 ax-i2m1 10593 ax-1ne0 10594 ax-rrecex 10597 ax-cnre 10598 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 df-xr 10667 |
This theorem is referenced by: xmulid1 12660 xmulid2 12661 xmulm1 12662 x2times 12680 xov1plusxeqvd 12872 ico01fl0 13177 hashge1 13738 hashgt12el 13771 hashgt12el2 13772 hashgt23el 13773 sgn1 14439 fprodge1 15337 halfleoddlt 15699 isnzr2hash 19965 0ringnnzr 19970 xrsnsgrp 20509 leordtval2 21748 unirnblps 22956 unirnbl 22957 mopnex 23056 dscopn 23110 nmoid 23278 xrsmopn 23347 zdis 23351 metnrmlem1a 23393 metnrmlem1 23394 icopnfcnv 23473 icopnfhmeo 23474 iccpnfcnv 23475 iccpnfhmeo 23476 cncmet 23852 itg2monolem1 24278 itg2monolem3 24280 abelthlem2 24947 abelthlem3 24948 abelthlem5 24950 abelthlem7 24953 abelth 24956 dvlog2lem 25162 dvlog2 25163 logtayl 25170 logtayl2 25172 scvxcvx 25490 pntibndlem1 26092 pntibndlem2 26094 pntibnd 26096 pntlemc 26098 pnt 26117 padicabvf 26134 padicabvcxp 26135 elntg2 26698 nmopun 29718 pjnmopi 29852 xlt2addrd 30408 xdivrec 30530 xrsmulgzz 30592 xrnarchi 30740 unitssxrge0 31042 xrge0iifcnv 31075 xrge0iifiso 31077 xrge0iifhom 31079 hasheuni 31243 ddemeas 31394 omssubadd 31457 prob01 31570 lfuhgr2 32262 dnizeq0 33711 broucube 34807 asindmre 34858 dvasin 34859 areacirclem1 34863 imo72b2 40403 cvgdvgrat 40522 supxrgelem 41481 xrlexaddrp 41496 infxr 41511 infleinflem2 41515 limsup10exlem 41929 limsup10ex 41930 liminf10ex 41931 salexct2 42499 salgencntex 42503 ovn0lem 42724 expnegico01 44501 regt1loggt0 44524 rege1logbrege0 44546 rege1logbzge0 44547 dignnld 44591 eenglngeehlnmlem1 44652 eenglngeehlnmlem2 44653 |
Copyright terms: Public domain | W3C validator |