Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnelprrecn | Structured version Visualization version GIF 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 10017 | . 2 ⊢ ℂ ∈ V | |
2 | 1 | prid2 4298 | 1 ⊢ ℂ ∈ {ℝ, ℂ} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 {cpr 4179 ℂcc 9934 ℝcr 9935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-cnex 9992 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-sn 4178 df-pr 4180 |
This theorem is referenced by: dvfcn 23672 dvnres 23694 dvexp 23716 dvrecg 23736 dvexp3 23741 dvef 23743 dvsincos 23744 dvlipcn 23757 dv11cn 23764 dvply1 24039 dvtaylp 24124 pserdvlem2 24182 pige3 24269 dvlog 24397 advlogexp 24401 logtayl 24406 dvcxp1 24481 dvcxp2 24482 dvcncxp1 24484 dvatan 24662 efrlim 24696 lgamgulmlem2 24756 logdivsum 25222 log2sumbnd 25233 itgexpif 30684 dvtan 33460 dvasin 33496 dvacos 33497 lhe4.4ex1a 38528 expgrowthi 38532 expgrowth 38534 binomcxplemdvbinom 38552 binomcxplemnotnn0 38555 dvsinexp 40125 dvsinax 40127 dvasinbx 40135 dvcosax 40141 dvxpaek 40155 itgsincmulx 40190 fourierdlem56 40379 etransclem46 40497 |
Copyright terms: Public domain | W3C validator |