![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-resscn | Unicode version |
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7888. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7839 |
. 2
![]() ![]() | |
2 | cc 7838 |
. 2
![]() ![]() | |
3 | 1, 2 | wss 3144 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: recn 7973 reex 7974 recni 7998 rerecapb 8829 nnsscn 8953 nn0sscn 9210 qsscn 9660 reexpcl 10567 rpexpcl 10569 reexpclzap 10570 expge0 10586 expge1 10587 abscn2 11354 recn2 11356 imcn2 11357 climabs 11359 climre 11361 climim 11362 climcvg1nlem 11388 fsumrecl 11440 fsumrpcl 11443 fsumge0 11498 fsumre 11511 fsumim 11512 fprodrecl 11647 fprodrpcl 11650 fprodreclf 11653 fprodge0 11676 fprodge1 11678 reeff1 11739 remet 14492 tgioo2cntop 14501 abscncf 14524 recncf 14525 imcncf 14526 cnrehmeocntop 14545 limcimolemlt 14585 recnprss 14608 dvcjbr 14624 dvfre 14626 reeff1olem 14644 cosz12 14653 ioocosf1o 14727 |
Copyright terms: Public domain | W3C validator |