![]() |
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 7900 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3151 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-resscn 7900 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: mulrid 7951 recnd 7982 pnfnre 7995 mnfnre 7996 cnegexlem1 8128 cnegexlem2 8129 cnegexlem3 8130 cnegex 8131 renegcl 8214 resubcl 8217 negf1o 8335 mul02lem2 8341 ltaddneg 8377 ltaddnegr 8378 ltaddsub2 8390 leaddsub2 8392 leltadd 8400 ltaddpos 8405 ltaddpos2 8406 posdif 8408 lenegcon1 8419 lenegcon2 8420 addge01 8425 addge02 8426 leaddle0 8430 mullt0 8433 recexre 8531 msqge0 8569 mulge0 8572 aprcl 8599 recexap 8606 rerecapb 8796 ltm1 8799 prodgt02 8806 prodge02 8808 ltmul2 8809 lemul2 8810 lemul2a 8812 ltmulgt12 8818 lemulge12 8820 gt0div 8823 ge0div 8824 ltmuldiv2 8828 ltdivmul 8829 ltdivmul2 8831 ledivmul2 8833 lemuldiv2 8835 negiso 8908 cju 8914 nnge1 8938 halfpos 9146 lt2halves 9150 addltmul 9151 avgle1 9155 avgle2 9156 div4p1lem1div2 9168 nnrecl 9170 elznn0 9264 elznn 9265 nzadd 9301 zmulcl 9302 difgtsumgt 9318 elz2 9320 gtndiv 9344 zeo 9354 supminfex 9593 eqreznegel 9610 negm 9611 irradd 9642 irrmul 9643 divlt1lt 9720 divle1le 9721 xnegneg 9829 rexsub 9849 xnegid 9855 xaddcom 9857 xaddid1 9858 xnegdi 9864 xaddass 9865 xleaddadd 9883 divelunit 9998 fzonmapblen 10182 expgt1 10553 mulexpzap 10555 leexp1a 10570 expubnd 10572 sqgt0ap 10583 lt2sq 10588 le2sq 10589 sqge0 10591 sumsqeq0 10593 bernneq 10635 bernneq2 10636 nn0ltexp2 10683 crre 10859 crim 10860 reim0 10863 mulreap 10866 rere 10867 remul2 10875 redivap 10876 immul2 10882 imdivap 10883 cjre 10884 cjreim 10905 rennim 11004 sqrt0rlem 11005 resqrexlemover 11012 absreimsq 11069 absreim 11070 absnid 11075 leabs 11076 absre 11079 absresq 11080 sqabs 11084 ltabs 11089 absdiflt 11094 absdifle 11095 lenegsq 11097 abssuble0 11105 dfabsmax 11219 max0addsup 11221 negfi 11229 minclpr 11238 reefcl 11669 efgt0 11685 reeftlcl 11690 resinval 11716 recosval 11717 resin4p 11719 recos4p 11720 resincl 11721 recoscl 11722 retanclap 11723 efieq 11736 sinbnd 11753 cosbnd 11754 absefi 11769 odd2np1 11870 infssuzex 11942 remetdval 13910 bl2ioo 13913 ioo2bl 13914 sincosq1sgn 14118 sincosq2sgn 14119 sincosq3sgn 14120 sincosq4sgn 14121 sinq12gt0 14122 relogoprlem 14160 logcxp 14189 rpcxpcl 14195 cxpcom 14228 rprelogbdiv 14246 triap 14637 trirec0 14652 |
Copyright terms: Public domain | W3C validator |