![]() |
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 . (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
cnelprrecn | ⊢ ℂ ∈ {ℝ, ℂ} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 11233 | . 2 ⊢ ℂ ∈ V | |
2 | 1 | prid2 4767 | 1 ⊢ ℂ ∈ {ℝ, ℂ} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 {cpr 4632 ℂcc 11150 ℝcr 11151 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-cnex 11208 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-un 3967 df-sn 4631 df-pr 4633 |
This theorem is referenced by: dvfcn 25957 dvnres 25981 dvexp 26005 dvrecg 26025 dvexp3 26030 dvef 26032 dvsincos 26033 dvlipcn 26047 dv11cn 26054 dvply1 26339 dvtaylp 26426 pserdvlem2 26486 pige3ALT 26576 dvlog 26707 advlogexp 26711 logtayl 26716 dvcxp1 26796 dvcxp2 26797 dvcncxp1 26799 dvatan 26992 efrlim 27026 efrlimOLD 27027 lgamgulmlem2 27087 logdivsum 27591 log2sumbnd 27602 itgexpif 34599 dvtan 37656 dvasin 37690 dvacos 37691 lcmineqlem7 42016 lcmineqlem8 42017 lcmineqlem12 42021 dvrelogpow2b 42049 aks4d1p1p6 42054 readvrec2 42369 readvrec 42370 lhe4.4ex1a 44324 expgrowthi 44328 expgrowth 44330 binomcxplemdvbinom 44348 binomcxplemnotnn0 44351 dvsinexp 45866 dvsinax 45868 dvasinbx 45875 dvcosax 45881 dvxpaek 45895 itgsincmulx 45929 fourierdlem56 46117 etransclem46 46235 |
Copyright terms: Public domain | W3C validator |