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 10798 | . 2 ⊢ 1 ∈ ℝ | |
2 | 1 | rexri 10856 | 1 ⊢ 1 ∈ ℝ* |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2112 1c1 10695 ℝ*cxr 10831 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-1cn 10752 ax-icn 10753 ax-addcl 10754 ax-mulcl 10756 ax-mulrcl 10757 ax-i2m1 10762 ax-1ne0 10763 ax-rrecex 10766 ax-cnre 10767 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ne 2933 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-iota 6316 df-fv 6366 df-ov 7194 df-xr 10836 |
This theorem is referenced by: xmulid1 12834 xmulid2 12835 xmulm1 12836 x2times 12854 xov1plusxeqvd 13051 ico01fl0 13359 hashge1 13921 hashgt12el 13954 hashgt12el2 13955 hashgt23el 13956 sgn1 14620 fprodge1 15520 halfleoddlt 15886 isnzr2hash 20256 0ringnnzr 20261 xrsnsgrp 20353 leordtval2 22063 unirnblps 23271 unirnbl 23272 mopnex 23371 dscopn 23425 nmoid 23594 xrsmopn 23663 zdis 23667 metnrmlem1a 23709 metnrmlem1 23710 icopnfcnv 23793 icopnfhmeo 23794 iccpnfcnv 23795 iccpnfhmeo 23796 cncmet 24173 itg2monolem1 24602 itg2monolem3 24604 abelthlem2 25278 abelthlem3 25279 abelthlem5 25281 abelthlem7 25284 abelth 25287 dvlog2lem 25494 dvlog2 25495 logtayl 25502 logtayl2 25504 scvxcvx 25822 pntibndlem1 26424 pntibndlem2 26426 pntibnd 26428 pntlemc 26430 pnt 26449 padicabvf 26466 padicabvcxp 26467 elntg2 27030 nmopun 30049 pjnmopi 30183 xlt2addrd 30755 xdivrec 30875 xrsmulgzz 30960 xrnarchi 31111 unitssxrge0 31518 xrge0iifcnv 31551 xrge0iifiso 31553 xrge0iifhom 31555 hasheuni 31719 ddemeas 31870 omssubadd 31933 prob01 32046 lfuhgr2 32747 dnizeq0 34341 iccioo01 35181 broucube 35497 asindmre 35546 dvasin 35547 areacirclem1 35551 imo72b2 41402 cvgdvgrat 41545 supxrgelem 42490 xrlexaddrp 42505 infxr 42520 infleinflem2 42524 limsup10exlem 42931 limsup10ex 42932 liminf10ex 42933 salexct2 43496 salgencntex 43500 ovn0lem 43721 expnegico01 45475 regt1loggt0 45498 rege1logbrege0 45520 rege1logbzge0 45521 dignnld 45565 eenglngeehlnmlem1 45699 eenglngeehlnmlem2 45700 iooii 45827 i0oii 45829 sepfsepc 45837 seppcld 45839 |
Copyright terms: Public domain | W3C validator |