![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0xr | Unicode version |
Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
Ref | Expression |
---|---|
0xr |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr 8000 |
. 2
![]() ![]() ![]() ![]() | |
2 | 0re 7956 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | sselii 3152 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-1re 7904 ax-addrcl 7907 ax-rnegex 7919 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2739 df-un 3133 df-in 3135 df-ss 3142 df-xr 7995 |
This theorem is referenced by: 0lepnf 9789 ge0gtmnf 9822 xlt0neg1 9837 xlt0neg2 9838 xle0neg1 9839 xle0neg2 9840 xaddf 9843 xaddval 9844 xaddid1 9861 xaddid2 9862 xnn0xadd0 9866 xaddge0 9877 xsubge0 9880 xposdif 9881 ioopos 9949 elxrge0 9977 0e0iccpnf 9979 dfrp2 10263 xrmaxadd 11268 xrminrpcl 11281 xrbdtri 11283 fprodge0 11644 ef01bndlem 11763 sin01bnd 11764 cos01bnd 11765 cos1bnd 11766 sin01gt0 11768 cos01gt0 11769 sin02gt0 11770 sincos1sgn 11771 sincos2sgn 11772 cos12dec 11774 halfleoddlt 11898 psmetge0 13767 isxmet2d 13784 xmetge0 13801 blgt0 13838 xblss2ps 13840 xblss2 13841 xblm 13853 bdxmet 13937 bdmet 13938 bdmopn 13940 xmetxp 13943 cnblcld 13971 blssioo 13981 reeff1oleme 14129 reeff1o 14130 sin0pilem1 14138 sin0pilem2 14139 pilem3 14140 sinhalfpilem 14148 sincosq1lem 14182 sincosq1sgn 14183 sincosq2sgn 14184 sinq12gt0 14187 cosq14gt0 14189 tangtx 14195 sincos4thpi 14197 pigt3 14201 cosordlem 14206 cosq34lt1 14207 cos02pilt1 14208 cos0pilt1 14209 iooref1o 14718 taupi 14756 |
Copyright terms: Public domain | W3C validator |