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 10689 | . 2 ⊢ ℂ ∈ V | |
2 | 1 | prid2 4651 | 1 ⊢ ℂ ∈ {ℝ, ℂ} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 {cpr 4515 ℂcc 10606 ℝcr 10607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-cnex 10664 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-un 3846 df-sn 4514 df-pr 4516 |
This theorem is referenced by: dvfcn 24652 dvnres 24675 dvexp 24697 dvrecg 24717 dvexp3 24722 dvef 24724 dvsincos 24725 dvlipcn 24738 dv11cn 24745 dvply1 25024 dvtaylp 25109 pserdvlem2 25167 pige3ALT 25256 dvlog 25386 advlogexp 25390 logtayl 25395 dvcxp1 25473 dvcxp2 25474 dvcncxp1 25476 dvatan 25665 efrlim 25699 lgamgulmlem2 25759 logdivsum 26261 log2sumbnd 26272 itgexpif 32148 dvtan 35439 dvasin 35473 dvacos 35474 lcmineqlem7 39652 lcmineqlem8 39653 lcmineqlem12 39657 dvrelogpow2b 39684 aks4d1p1p6 39689 lhe4.4ex1a 41469 expgrowthi 41473 expgrowth 41475 binomcxplemdvbinom 41493 binomcxplemnotnn0 41496 dvsinexp 42978 dvsinax 42980 dvasinbx 42987 dvcosax 42993 dvxpaek 43007 itgsincmulx 43041 fourierdlem56 43229 etransclem46 43347 |
Copyright terms: Public domain | W3C validator |