Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > recn | Unicode version |
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Ref | Expression |
---|---|
recn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn 7680 | . 2 | |
2 | 1 | sseli 3063 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cc 7586 cr 7587 |
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-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-resscn 7680 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: mulid1 7731 recnd 7762 pnfnre 7775 mnfnre 7776 cnegexlem1 7905 cnegexlem2 7906 cnegexlem3 7907 cnegex 7908 renegcl 7991 resubcl 7994 negf1o 8112 mul02lem2 8118 ltaddneg 8154 ltaddnegr 8155 ltaddsub2 8167 leaddsub2 8169 leltadd 8177 ltaddpos 8182 ltaddpos2 8183 posdif 8185 lenegcon1 8196 lenegcon2 8197 addge01 8202 addge02 8203 leaddle0 8207 mullt0 8210 recexre 8308 msqge0 8346 mulge0 8349 aprcl 8376 recexap 8382 ltm1 8572 prodgt02 8579 prodge02 8581 ltmul2 8582 lemul2 8583 lemul2a 8585 ltmulgt12 8591 lemulge12 8593 gt0div 8596 ge0div 8597 ltmuldiv2 8601 ltdivmul 8602 ltdivmul2 8604 ledivmul2 8606 lemuldiv2 8608 negiso 8681 cju 8687 nnge1 8711 halfpos 8919 lt2halves 8923 addltmul 8924 avgle1 8928 avgle2 8929 div4p1lem1div2 8941 nnrecl 8943 elznn0 9037 elznn 9038 nzadd 9074 zmulcl 9075 elz2 9090 gtndiv 9114 zeo 9124 supminfex 9360 eqreznegel 9374 negm 9375 irradd 9406 irrmul 9407 divlt1lt 9479 divle1le 9480 xnegneg 9584 rexsub 9604 xnegid 9610 xaddcom 9612 xaddid1 9613 xnegdi 9619 xaddass 9620 xleaddadd 9638 divelunit 9753 fzonmapblen 9932 expgt1 10299 mulexpzap 10301 leexp1a 10316 expubnd 10318 sqgt0ap 10329 lt2sq 10334 le2sq 10335 sqge0 10337 sumsqeq0 10339 bernneq 10380 bernneq2 10381 crre 10597 crim 10598 reim0 10601 mulreap 10604 rere 10605 remul2 10613 redivap 10614 immul2 10620 imdivap 10621 cjre 10622 cjreim 10643 rennim 10742 sqrt0rlem 10743 resqrexlemover 10750 absreimsq 10807 absreim 10808 absnid 10813 leabs 10814 absre 10817 absresq 10818 sqabs 10822 ltabs 10827 absdiflt 10832 absdifle 10833 lenegsq 10835 abssuble0 10843 dfabsmax 10957 max0addsup 10959 negfi 10967 minclpr 10976 reefcl 11301 efgt0 11317 reeftlcl 11322 resinval 11349 recosval 11350 resin4p 11352 recos4p 11353 resincl 11354 recoscl 11355 retanclap 11356 efieq 11369 sinbnd 11386 cosbnd 11387 absefi 11402 odd2np1 11497 infssuzex 11569 remetdval 12635 bl2ioo 12638 ioo2bl 12639 sincosq1sgn 12834 sincosq2sgn 12835 sincosq3sgn 12836 sincosq4sgn 12837 sinq12gt0 12838 triap 13151 |
Copyright terms: Public domain | W3C validator |