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

Theorem cnelprrecn 11151
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 11139 . 2 ℂ ∈ V
21prid2 4729 1 ℂ ∈ {ℝ, ℂ}
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {cpr 4593  cc 11056  cr 11057
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 2708  ax-cnex 11114
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 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594
This theorem is referenced by:  dvfcn  25288  dvnres  25311  dvexp  25333  dvrecg  25353  dvexp3  25358  dvef  25360  dvsincos  25361  dvlipcn  25374  dv11cn  25381  dvply1  25660  dvtaylp  25745  pserdvlem2  25803  pige3ALT  25892  dvlog  26022  advlogexp  26026  logtayl  26031  dvcxp1  26109  dvcxp2  26110  dvcncxp1  26112  dvatan  26301  efrlim  26335  lgamgulmlem2  26395  logdivsum  26897  log2sumbnd  26908  itgexpif  33259  dvtan  36157  dvasin  36191  dvacos  36192  lcmineqlem7  40521  lcmineqlem8  40522  lcmineqlem12  40526  dvrelogpow2b  40554  aks4d1p1p6  40559  lhe4.4ex1a  42683  expgrowthi  42687  expgrowth  42689  binomcxplemdvbinom  42707  binomcxplemnotnn0  42710  dvsinexp  44226  dvsinax  44228  dvasinbx  44235  dvcosax  44241  dvxpaek  44255  itgsincmulx  44289  fourierdlem56  44477  etransclem46  44595
  Copyright terms: Public domain W3C validator