![]() |
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 11187 | . 2 ⊢ ℂ ∈ V | |
2 | 1 | prid2 4766 | 1 ⊢ ℂ ∈ {ℝ, ℂ} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 {cpr 4629 ℂcc 11104 ℝcr 11105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-cnex 11162 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3952 df-sn 4628 df-pr 4630 |
This theorem is referenced by: dvfcn 25407 dvnres 25430 dvexp 25452 dvrecg 25472 dvexp3 25477 dvef 25479 dvsincos 25480 dvlipcn 25493 dv11cn 25500 dvply1 25779 dvtaylp 25864 pserdvlem2 25922 pige3ALT 26011 dvlog 26141 advlogexp 26145 logtayl 26150 dvcxp1 26228 dvcxp2 26229 dvcncxp1 26231 dvatan 26420 efrlim 26454 lgamgulmlem2 26514 logdivsum 27016 log2sumbnd 27027 itgexpif 33556 dvtan 36476 dvasin 36510 dvacos 36511 lcmineqlem7 40838 lcmineqlem8 40839 lcmineqlem12 40843 dvrelogpow2b 40871 aks4d1p1p6 40876 lhe4.4ex1a 43021 expgrowthi 43025 expgrowth 43027 binomcxplemdvbinom 43045 binomcxplemnotnn0 43048 dvsinexp 44562 dvsinax 44564 dvasinbx 44571 dvcosax 44577 dvxpaek 44591 itgsincmulx 44625 fourierdlem56 44813 etransclem46 44931 |
Copyright terms: Public domain | W3C validator |