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 7889 | . 2 | |
2 | ax-rnegex 7853 | . 2 | |
3 | readdcl 7870 | . . . . 5 | |
4 | 1, 3 | mpan 421 | . . . 4 |
5 | eleq1 2227 | . . . 4 | |
6 | 4, 5 | syl5ibcom 154 | . . 3 |
7 | 6 | rexlimiv 2575 | . 2 |
8 | 1, 2, 7 | mp2b 8 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1342 wcel 2135 wrex 2443 (class class class)co 5836 cr 7743 cc0 7744 c1 7745 caddc 7747 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 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-nf 1448 df-cleq 2157 df-clel 2160 df-ral 2447 df-rex 2448 |
This theorem is referenced by: 0red 7891 0xr 7936 axmulgt0 7961 gtso 7968 0lt1 8016 ine0 8283 ltaddneg 8313 addgt0 8337 addgegt0 8338 addgtge0 8339 addge0 8340 ltaddpos 8341 ltneg 8351 leneg 8354 lt0neg1 8357 lt0neg2 8358 le0neg1 8359 le0neg2 8360 addge01 8361 suble0 8365 0le1 8370 gt0ne0i 8375 gt0ne0d 8401 lt0ne0d 8402 recexre 8467 recexgt0 8469 inelr 8473 rimul 8474 1ap0 8479 reapmul1 8484 apsqgt0 8490 msqge0 8505 mulge0 8508 recexaplem2 8540 recexap 8541 rerecclap 8617 ltm1 8732 recgt0 8736 ltmul12a 8746 lemul12a 8748 mulgt1 8749 gt0div 8756 ge0div 8757 recgt1i 8784 recreclt 8786 sup3exmid 8843 crap0 8844 nnge1 8871 nngt0 8873 nnrecgt0 8886 0ne1 8915 0le0 8937 neg1lt0 8956 halfge0 9064 iap0 9071 nn0ssre 9109 nn0ge0 9130 nn0nlt0 9131 nn0le0eq0 9133 0mnnnnn0 9137 elnnnn0b 9149 elnnnn0c 9150 elnnz 9192 0z 9193 elnnz1 9205 nn0lt10b 9262 recnz 9275 gtndiv 9277 fnn0ind 9298 rpge0 9593 rpnegap 9613 0nrp 9616 0ltpnf 9709 mnflt0 9711 xneg0 9758 xaddid1 9789 xnn0xadd0 9794 xposdif 9809 elrege0 9903 0e0icopnf 9906 0elunit 9913 1elunit 9914 divelunit 9929 lincmb01cmp 9930 iccf1o 9931 unitssre 9932 fz0to4untppr 10049 modqelico 10259 modqmuladdim 10292 addmodid 10297 expubnd 10502 le2sq2 10520 bernneq2 10565 expnbnd 10567 expnlbnd 10568 faclbnd 10643 faclbnd3 10645 faclbnd6 10646 bcval4 10654 bcpasc 10668 reim0 10789 re0 10823 im0 10824 rei 10827 imi 10828 cj0 10829 caucvgre 10909 rennim 10930 sqrt0rlem 10931 sqrt0 10932 resqrexlemdecn 10940 resqrexlemnm 10946 resqrexlemgt0 10948 sqrt00 10968 sqrt9 10976 sqrt2gt1lt2 10977 leabs 11002 ltabs 11015 sqrtpclii 11058 max0addsup 11147 fimaxre2 11154 climge0 11252 iserge0 11270 fsum00 11389 arisum2 11426 0.999... 11448 fprodge0 11564 cos0 11657 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 cos2bnd 11687 sin01gt0 11688 cos01gt0 11689 sincos2sgn 11692 sin4lt0 11693 absef 11696 absefib 11697 efieq1re 11698 epos 11707 flodddiv4 11856 gcdn0gt0 11896 nn0seqcvgd 11952 algcvgblem 11960 algcvga 11962 pythagtriplem12 12186 pythagtriplem13 12187 pythagtriplem14 12188 pythagtriplem16 12190 ssblps 12972 ssbl 12973 xmeter 12983 cnbl0 13081 reeff1olem 13239 pilem3 13251 pipos 13256 sinhalfpilem 13259 sincosq1sgn 13294 sincosq2sgn 13295 sinq34lt0t 13299 coseq0q4123 13302 coseq00topi 13303 coseq0negpitopi 13304 tangtx 13306 sincos4thpi 13308 sincos6thpi 13310 cosordlem 13317 cosq34lt1 13318 cos02pilt1 13319 cos0pilt1 13320 cos11 13321 ioocosf1o 13322 log1 13334 logrpap0b 13344 logdivlti 13349 rpabscxpbnd 13406 ex-gcd 13455 trilpolemclim 13756 trilpolemcl 13757 trilpolemisumle 13758 trilpolemeq1 13760 trilpolemlt1 13761 trirec0 13764 apdiff 13768 redc0 13777 reap0 13778 dceqnconst 13779 dcapnconst 13780 nconstwlpolemgt0 13783 |
Copyright terms: Public domain | W3C validator |