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

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

Proof of Theorem reelprrecn
StepHypRef Expression
1 reex 9979 . 2 ℝ ∈ V
21prid1 4272 1 ℝ ∈ {ℝ, ℂ}
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  {cpr 4155  cc 9886  cr 9887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-cnex 9944  ax-resscn 9945
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-un 3564  df-in 3566  df-ss 3573  df-sn 4154  df-pr 4156
This theorem is referenced by:  dvf  23594  dvmptcj  23654  dvmptre  23655  dvmptim  23656  rolle  23674  cmvth  23675  mvth  23676  dvlip  23677  dvlipcn  23678  dvle  23691  dvivthlem1  23692  dvivth  23694  lhop2  23699  dvcnvre  23703  dvfsumle  23705  dvfsumge  23706  dvfsumabs  23707  dvfsumlem2  23711  dvfsum2  23718  ftc2  23728  itgparts  23731  itgsubstlem  23732  aalioulem3  24010  taylthlem2  24049  taylth  24050  efcvx  24124  pige3  24190  dvrelog  24300  advlog  24317  advlogexp  24318  logccv  24326  dvcxp1  24398  loglesqrt  24416  divsqrtsumlem  24623  lgamgulmlem2  24673  logexprlim  24867  logdivsum  25139  log2sumbnd  25150  itgexpif  30475  ftc2nc  33161  dvreasin  33165  dvreacos  33166  areacirclem1  33167  itgpowd  37316  lhe4.4ex1a  38045  dvcosre  39457  dvcnre  39462  dvmptresicc  39467  itgsin0pilem1  39498  itgsinexplem1  39502  itgcoscmulx  39518  itgiccshift  39529  itgperiod  39530  itgsbtaddcnst  39531  dirkeritg  39652  dirkercncflem2  39654  fourierdlem28  39685  fourierdlem39  39696  fourierdlem56  39712  fourierdlem57  39713  fourierdlem58  39714  fourierdlem59  39715  fourierdlem60  39716  fourierdlem61  39717  fourierdlem62  39718  fourierdlem68  39724  fourierdlem72  39728  fouriersw  39781  etransclem2  39786  etransclem23  39807  etransclem35  39819  etransclem38  39822  etransclem39  39823  etransclem44  39828  etransclem45  39829  etransclem46  39830  etransclem47  39831
  Copyright terms: Public domain W3C validator