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

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

Proof of Theorem reelprrecn
StepHypRef Expression
1 reex 11149 . 2 ℝ ∈ V
21prid1 4728 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-sep 5261  ax-cnex 11114  ax-resscn 11115
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-rab 3411  df-v 3450  df-un 3920  df-in 3922  df-ss 3932  df-sn 4592  df-pr 4594
This theorem is referenced by:  dvf  25287  dvmptresicc  25296  dvmptcj  25348  dvmptre  25349  dvmptim  25350  rolle  25370  cmvth  25371  mvth  25372  dvlip  25373  dvlipcn  25374  dvle  25387  dvivthlem1  25388  dvivth  25390  lhop2  25395  dvcnvre  25399  dvfsumle  25401  dvfsumge  25402  dvfsumabs  25403  dvfsumlem2  25407  dvfsum2  25414  ftc2  25424  itgparts  25427  itgsubstlem  25428  itgpowd  25430  aalioulem3  25710  taylthlem2  25749  taylth  25750  efcvx  25824  pige3ALT  25892  dvrelog  26008  advlog  26025  advlogexp  26026  logccv  26034  dvcxp1  26109  loglesqrt  26127  divsqrtsumlem  26345  lgamgulmlem2  26395  logexprlim  26589  logdivsum  26897  log2sumbnd  26908  fdvneggt  33253  fdvnegge  33255  itgexpif  33259  logdivsqrle  33303  ftc2nc  36189  dvreasin  36193  dvreacos  36194  areacirclem1  36195  dvrelog2  40550  dvrelog3  40551  dvrelog2b  40552  dvrelogpow2b  40554  aks4d1p1p6  40559  lhe4.4ex1a  42683  dvcosre  44227  dvcnre  44231  itgsin0pilem1  44265  itgsinexplem1  44269  itgcoscmulx  44284  itgiccshift  44295  itgperiod  44296  itgsbtaddcnst  44297  dirkeritg  44417  dirkercncflem2  44419  fourierdlem28  44450  fourierdlem39  44461  fourierdlem56  44477  fourierdlem57  44478  fourierdlem58  44479  fourierdlem59  44480  fourierdlem60  44481  fourierdlem61  44482  fourierdlem62  44483  fourierdlem68  44489  fourierdlem72  44493  fouriersw  44546  etransclem2  44551  etransclem23  44572  etransclem35  44584  etransclem38  44587  etransclem39  44588  etransclem44  44593  etransclem45  44594  etransclem46  44595  etransclem47  44596
  Copyright terms: Public domain W3C validator