![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnelprrecn | Structured version Visualization version Unicode version |
Description: Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
cnelprrecn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 9651 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | prid2 4094 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-cnex 9626 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-un 3421 df-sn 3981 df-pr 3983 |
This theorem is referenced by: dvfcn 22919 dvnres 22941 dvexp 22963 dvexp3 22986 dvef 22988 dvsincos 22989 dvlipcn 23002 dv11cn 23009 dvply1 23293 dvtaylp 23381 pserdvlem2 23439 pige3 23528 dvlog 23652 advlogexp 23656 logtayl 23661 dvcxp1 23736 dvcxp2 23737 dvcncxp1 23739 dvatan 23917 efrlim 23951 lgamgulmlem2 24011 logdivsum 24427 log2sumbnd 24438 dvtan 32038 dvasin 32074 dvacos 32075 lhe4.4ex1a 36723 expgrowthi 36727 expgrowth 36729 binomcxplemdvbinom 36747 binomcxplemnotnn0 36750 dvsinexp 37866 dvrecg 37868 dvsinax 37869 dvasinbx 37878 dvcosax 37884 dvxpaek 37901 itgsincmulx 37937 fourierdlem56 38127 etransclem46 38246 |
Copyright terms: Public domain | W3C validator |