| 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 11236 | . 2 ⊢ ℂ ∈ V | |
| 2 | 1 | prid2 4763 | 1 ⊢ ℂ ∈ {ℝ, ℂ} |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 {cpr 4628 ℂcc 11153 ℝcr 11154 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-cnex 11211 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-pr 4629 |
| This theorem is referenced by: dvfcn 25943 dvnres 25967 dvexp 25991 dvrecg 26011 dvexp3 26016 dvef 26018 dvsincos 26019 dvlipcn 26033 dv11cn 26040 dvply1 26325 dvtaylp 26412 pserdvlem2 26472 pige3ALT 26562 dvlog 26693 advlogexp 26697 logtayl 26702 dvcxp1 26782 dvcxp2 26783 dvcncxp1 26785 dvatan 26978 efrlim 27012 efrlimOLD 27013 lgamgulmlem2 27073 logdivsum 27577 log2sumbnd 27588 itgexpif 34621 dvtan 37677 dvasin 37711 dvacos 37712 lcmineqlem7 42036 lcmineqlem8 42037 lcmineqlem12 42041 dvrelogpow2b 42069 aks4d1p1p6 42074 readvrec2 42391 readvrec 42392 lhe4.4ex1a 44348 expgrowthi 44352 expgrowth 44354 binomcxplemdvbinom 44372 binomcxplemnotnn0 44375 dvsinexp 45926 dvsinax 45928 dvasinbx 45935 dvcosax 45941 dvxpaek 45955 itgsincmulx 45989 fourierdlem56 46177 etransclem46 46295 |
| Copyright terms: Public domain | W3C validator |