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 7933 | . 2 | |
2 | 0re 7890 | . 2 | |
3 | 1, 2 | sselii 3134 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 cr 7743 cc0 7744 cxr 7923 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-1re 7838 ax-addrcl 7841 ax-rnegex 7853 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rex 2448 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 df-xr 7928 |
This theorem is referenced by: 0lepnf 9717 ge0gtmnf 9750 xlt0neg1 9765 xlt0neg2 9766 xle0neg1 9767 xle0neg2 9768 xaddf 9771 xaddval 9772 xaddid1 9789 xaddid2 9790 xnn0xadd0 9794 xaddge0 9805 xsubge0 9808 xposdif 9809 ioopos 9877 elxrge0 9905 0e0iccpnf 9907 dfrp2 10189 xrmaxadd 11188 xrminrpcl 11201 xrbdtri 11203 fprodge0 11564 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 cos1bnd 11686 sin01gt0 11688 cos01gt0 11689 sin02gt0 11690 sincos1sgn 11691 sincos2sgn 11692 cos12dec 11694 halfleoddlt 11816 psmetge0 12878 isxmet2d 12895 xmetge0 12912 blgt0 12949 xblss2ps 12951 xblss2 12952 xblm 12964 bdxmet 13048 bdmet 13049 bdmopn 13051 xmetxp 13054 cnblcld 13082 blssioo 13092 reeff1oleme 13240 reeff1o 13241 sin0pilem1 13249 sin0pilem2 13250 pilem3 13251 sinhalfpilem 13259 sincosq1lem 13293 sincosq1sgn 13294 sincosq2sgn 13295 sinq12gt0 13298 cosq14gt0 13300 tangtx 13306 sincos4thpi 13308 pigt3 13312 cosordlem 13317 cosq34lt1 13318 cos02pilt1 13319 cos0pilt1 13320 iooref1o 13754 taupi 13790 |
Copyright terms: Public domain | W3C validator |