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 7733 | . 2 | |
2 | ax-rnegex 7697 | . 2 | |
3 | readdcl 7714 | . . . . 5 | |
4 | 1, 3 | mpan 420 | . . . 4 |
5 | eleq1 2180 | . . . 4 | |
6 | 4, 5 | syl5ibcom 154 | . . 3 |
7 | 6 | rexlimiv 2520 | . 2 |
8 | 1, 2, 7 | mp2b 8 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 wcel 1465 wrex 2394 (class class class)co 5742 cr 7587 cc0 7588 c1 7589 caddc 7591 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-1re 7682 ax-addrcl 7685 ax-rnegex 7697 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-cleq 2110 df-clel 2113 df-ral 2398 df-rex 2399 |
This theorem is referenced by: 0red 7735 0xr 7780 axmulgt0 7804 gtso 7811 0lt1 7857 ine0 8124 ltaddneg 8154 addgt0 8178 addgegt0 8179 addgtge0 8180 addge0 8181 ltaddpos 8182 ltneg 8192 leneg 8195 lt0neg1 8198 lt0neg2 8199 le0neg1 8200 le0neg2 8201 addge01 8202 suble0 8206 0le1 8211 gt0ne0i 8216 gt0ne0d 8242 lt0ne0d 8243 recexre 8307 recexgt0 8309 inelr 8313 rimul 8314 1ap0 8319 reapmul1 8324 apsqgt0 8330 msqge0 8345 mulge0 8348 recexaplem2 8380 recexap 8381 rerecclap 8457 ltm1 8568 recgt0 8572 ltmul12a 8582 lemul12a 8584 mulgt1 8585 gt0div 8592 ge0div 8593 recgt1i 8620 recreclt 8622 sup3exmid 8679 crap0 8680 nnge1 8707 nngt0 8709 nnrecgt0 8722 0ne1 8751 0le0 8773 neg1lt0 8792 halfge0 8894 iap0 8901 nn0ssre 8939 nn0ge0 8960 nn0nlt0 8961 nn0le0eq0 8963 0mnnnnn0 8967 elnnnn0b 8979 elnnnn0c 8980 elnnz 9022 0z 9023 elnnz1 9035 nn0lt10b 9089 recnz 9102 gtndiv 9104 fnn0ind 9125 rpge0 9409 rpnegap 9429 0nrp 9432 0ltpnf 9523 mnflt0 9525 xneg0 9569 xaddid1 9600 xnn0xadd0 9605 xposdif 9620 elrege0 9714 0e0icopnf 9717 0elunit 9724 1elunit 9725 divelunit 9740 lincmb01cmp 9741 iccf1o 9742 unitssre 9743 modqelico 10062 modqmuladdim 10095 addmodid 10100 expubnd 10305 le2sq2 10323 bernneq2 10368 expnbnd 10370 expnlbnd 10371 faclbnd 10442 faclbnd3 10444 faclbnd6 10445 bcval4 10453 bcpasc 10467 reim0 10588 re0 10622 im0 10623 rei 10626 imi 10627 cj0 10628 caucvgre 10708 rennim 10729 sqrt0rlem 10730 sqrt0 10731 resqrexlemdecn 10739 resqrexlemnm 10745 resqrexlemgt0 10747 sqrt00 10767 sqrt9 10775 sqrt2gt1lt2 10776 leabs 10801 ltabs 10814 sqrtpclii 10857 max0addsup 10946 fimaxre2 10953 climge0 11049 iserge0 11067 fsum00 11186 arisum2 11223 0.999... 11245 cos0 11351 ef01bndlem 11377 sin01bnd 11378 cos01bnd 11379 cos2bnd 11381 sin01gt0 11382 cos01gt0 11383 sincos2sgn 11386 sin4lt0 11387 absef 11390 absefib 11391 efieq1re 11392 epos 11399 flodddiv4 11543 gcdn0gt0 11578 nn0seqcvgd 11634 algcvgblem 11642 algcvga 11644 ssblps 12505 ssbl 12506 xmeter 12516 cnbl0 12614 pilem3 12775 pipos 12780 sinhalfpilem 12783 sincosq1sgn 12818 sincosq2sgn 12819 sinq34lt0t 12823 coseq0q4123 12826 coseq00topi 12827 coseq0negpitopi 12828 ex-gcd 12839 trilpolemclim 13125 trilpolemcl 13126 trilpolemisumle 13127 trilpolemeq1 13129 trilpolemlt1 13130 |
Copyright terms: Public domain | W3C validator |