MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnelprrecn Structured version   Visualization version   GIF version

Theorem cnelprrecn 10622
Description: Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
cnelprrecn ℂ ∈ {ℝ, ℂ}

Proof of Theorem cnelprrecn
StepHypRef Expression
1 cnex 10610 . 2 ℂ ∈ V
21prid2 4691 1 ℂ ∈ {ℝ, ℂ}
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {cpr 4561  cc 10527  cr 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-cnex 10585
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-un 3939  df-sn 4560  df-pr 4562
This theorem is referenced by:  dvfcn  24498  dvnres  24520  dvexp  24542  dvrecg  24562  dvexp3  24567  dvef  24569  dvsincos  24570  dvlipcn  24583  dv11cn  24590  dvply1  24865  dvtaylp  24950  pserdvlem2  25008  pige3ALT  25097  dvlog  25226  advlogexp  25230  logtayl  25235  dvcxp1  25313  dvcxp2  25314  dvcncxp1  25316  dvatan  25505  efrlim  25539  lgamgulmlem2  25599  logdivsum  26101  log2sumbnd  26112  itgexpif  31870  dvtan  34934  dvasin  34970  dvacos  34971  lhe4.4ex1a  40651  expgrowthi  40655  expgrowth  40657  binomcxplemdvbinom  40675  binomcxplemnotnn0  40678  dvsinexp  42184  dvsinax  42186  dvasinbx  42194  dvcosax  42200  dvxpaek  42214  itgsincmulx  42248  fourierdlem56  42437  etransclem46  42555
  Copyright terms: Public domain W3C validator