Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0re | Unicode version |
Description: is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
0re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7758 | . 2 | |
2 | ax-rnegex 7722 | . 2 | |
3 | readdcl 7739 | . . . . 5 | |
4 | 1, 3 | mpan 420 | . . . 4 |
5 | eleq1 2200 | . . . 4 | |
6 | 4, 5 | syl5ibcom 154 | . . 3 |
7 | 6 | rexlimiv 2541 | . 2 |
8 | 1, 2, 7 | mp2b 8 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1331 wcel 1480 wrex 2415 (class class class)co 5767 cr 7612 cc0 7613 c1 7614 caddc 7616 |
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-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-1re 7707 ax-addrcl 7710 ax-rnegex 7722 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-cleq 2130 df-clel 2133 df-ral 2419 df-rex 2420 |
This theorem is referenced by: 0red 7760 0xr 7805 axmulgt0 7829 gtso 7836 0lt1 7882 ine0 8149 ltaddneg 8179 addgt0 8203 addgegt0 8204 addgtge0 8205 addge0 8206 ltaddpos 8207 ltneg 8217 leneg 8220 lt0neg1 8223 lt0neg2 8224 le0neg1 8225 le0neg2 8226 addge01 8227 suble0 8231 0le1 8236 gt0ne0i 8241 gt0ne0d 8267 lt0ne0d 8268 recexre 8333 recexgt0 8335 inelr 8339 rimul 8340 1ap0 8345 reapmul1 8350 apsqgt0 8356 msqge0 8371 mulge0 8374 recexaplem2 8406 recexap 8407 rerecclap 8483 ltm1 8597 recgt0 8601 ltmul12a 8611 lemul12a 8613 mulgt1 8614 gt0div 8621 ge0div 8622 recgt1i 8649 recreclt 8651 sup3exmid 8708 crap0 8709 nnge1 8736 nngt0 8738 nnrecgt0 8751 0ne1 8780 0le0 8802 neg1lt0 8821 halfge0 8929 iap0 8936 nn0ssre 8974 nn0ge0 8995 nn0nlt0 8996 nn0le0eq0 8998 0mnnnnn0 9002 elnnnn0b 9014 elnnnn0c 9015 elnnz 9057 0z 9058 elnnz1 9070 nn0lt10b 9124 recnz 9137 gtndiv 9139 fnn0ind 9160 rpge0 9447 rpnegap 9467 0nrp 9470 0ltpnf 9561 mnflt0 9563 xneg0 9607 xaddid1 9638 xnn0xadd0 9643 xposdif 9658 elrege0 9752 0e0icopnf 9755 0elunit 9762 1elunit 9763 divelunit 9778 lincmb01cmp 9779 iccf1o 9780 unitssre 9781 modqelico 10100 modqmuladdim 10133 addmodid 10138 expubnd 10343 le2sq2 10361 bernneq2 10406 expnbnd 10408 expnlbnd 10409 faclbnd 10480 faclbnd3 10482 faclbnd6 10483 bcval4 10491 bcpasc 10505 reim0 10626 re0 10660 im0 10661 rei 10664 imi 10665 cj0 10666 caucvgre 10746 rennim 10767 sqrt0rlem 10768 sqrt0 10769 resqrexlemdecn 10777 resqrexlemnm 10783 resqrexlemgt0 10785 sqrt00 10805 sqrt9 10813 sqrt2gt1lt2 10814 leabs 10839 ltabs 10852 sqrtpclii 10895 max0addsup 10984 fimaxre2 10991 climge0 11087 iserge0 11105 fsum00 11224 arisum2 11261 0.999... 11283 cos0 11426 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 cos2bnd 11456 sin01gt0 11457 cos01gt0 11458 sincos2sgn 11461 sin4lt0 11462 absef 11465 absefib 11466 efieq1re 11467 epos 11476 flodddiv4 11620 gcdn0gt0 11655 nn0seqcvgd 11711 algcvgblem 11719 algcvga 11721 ssblps 12583 ssbl 12584 xmeter 12594 cnbl0 12692 pilem3 12853 pipos 12858 sinhalfpilem 12861 sincosq1sgn 12896 sincosq2sgn 12897 sinq34lt0t 12901 coseq0q4123 12904 coseq00topi 12905 coseq0negpitopi 12906 tangtx 12908 sincos4thpi 12910 sincos6thpi 12912 cosordlem 12919 cosq34lt1 12920 cos02pilt1 12921 ex-gcd 12932 trilpolemclim 13218 trilpolemcl 13219 trilpolemisumle 13220 trilpolemeq1 13222 trilpolemlt1 13223 |
Copyright terms: Public domain | W3C validator |