| 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 11261 | . 2 ⊢ 1 ∈ ℝ | |
| 2 | 1 | rexri 11319 | 1 ⊢ 1 ∈ ℝ* |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 1c1 11156 ℝ*cxr 11294 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-mulcl 11217 ax-mulrcl 11218 ax-i2m1 11223 ax-1ne0 11224 ax-rrecex 11227 ax-cnre 11228 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 df-xr 11299 |
| This theorem is referenced by: xmulrid 13321 xmullid 13322 xmulm1 13323 x2times 13341 xov1plusxeqvd 13538 ico01fl0 13859 hashge1 14428 hashgt12el 14461 hashgt12el2 14462 hashgt23el 14463 sgn1 15131 fprodge1 16031 halfleoddlt 16399 isnzr2hash 20519 0ringnnzr 20525 xrsnsgrp 21420 leordtval2 23220 unirnblps 24429 unirnbl 24430 mopnex 24532 dscopn 24586 nmoid 24763 xrsmopn 24834 zdis 24838 metnrmlem1a 24880 metnrmlem1 24881 icopnfcnv 24973 icopnfhmeo 24974 iccpnfcnv 24975 iccpnfhmeo 24976 cncmet 25356 itg2monolem1 25785 itg2monolem3 25787 abelthlem2 26476 abelthlem3 26477 abelthlem5 26479 abelthlem7 26482 abelth 26485 dvlog2lem 26694 dvlog2 26695 logtayl 26702 logtayl2 26704 scvxcvx 27029 pntibndlem1 27633 pntibndlem2 27635 pntibnd 27637 pntlemc 27639 pnt 27658 padicabvf 27675 padicabvcxp 27676 elntg2 29000 nmopun 32033 pjnmopi 32167 xlt2addrd 32762 xdivrec 32909 xrsmulgzz 33011 xrnarchi 33191 rtelextdg2lem 33767 unitssxrge0 33899 xrge0iifcnv 33932 xrge0iifiso 33934 xrge0iifhom 33936 hasheuni 34086 ddemeas 34237 omssubadd 34302 prob01 34415 lfuhgr2 35124 dnizeq0 36476 iccioo01 37328 broucube 37661 asindmre 37710 dvasin 37711 areacirclem1 37715 aks6d1c6lem1 42171 imo72b2 44185 cvgdvgrat 44332 supxrgelem 45348 xrlexaddrp 45363 infxr 45378 infleinflem2 45382 limsup10exlem 45787 limsup10ex 45788 liminf10ex 45789 salexct2 46354 salgencntex 46358 ovn0lem 46580 expnegico01 48435 regt1loggt0 48457 rege1logbrege0 48479 rege1logbzge0 48480 dignnld 48524 eenglngeehlnmlem1 48658 eenglngeehlnmlem2 48659 iooii 48815 i0oii 48817 sepfsepc 48825 seppcld 48827 |
| Copyright terms: Public domain | W3C validator |