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 10952 | . 2 ⊢ ℂ ∈ V | |
2 | 1 | prid2 4699 | 1 ⊢ ℂ ∈ {ℝ, ℂ} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 {cpr 4563 ℂcc 10869 ℝcr 10870 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-cnex 10927 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-un 3892 df-sn 4562 df-pr 4564 |
This theorem is referenced by: dvfcn 25072 dvnres 25095 dvexp 25117 dvrecg 25137 dvexp3 25142 dvef 25144 dvsincos 25145 dvlipcn 25158 dv11cn 25165 dvply1 25444 dvtaylp 25529 pserdvlem2 25587 pige3ALT 25676 dvlog 25806 advlogexp 25810 logtayl 25815 dvcxp1 25893 dvcxp2 25894 dvcncxp1 25896 dvatan 26085 efrlim 26119 lgamgulmlem2 26179 logdivsum 26681 log2sumbnd 26692 itgexpif 32586 dvtan 35827 dvasin 35861 dvacos 35862 lcmineqlem7 40043 lcmineqlem8 40044 lcmineqlem12 40048 dvrelogpow2b 40076 aks4d1p1p6 40081 lhe4.4ex1a 41947 expgrowthi 41951 expgrowth 41953 binomcxplemdvbinom 41971 binomcxplemnotnn0 41974 dvsinexp 43452 dvsinax 43454 dvasinbx 43461 dvcosax 43467 dvxpaek 43481 itgsincmulx 43515 fourierdlem56 43703 etransclem46 43821 |
Copyright terms: Public domain | W3C validator |