Theorem recn 11150

Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)

Assertion

Ref	Expression
recn	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn

Step	Hyp	Ref	Expression
1		ax-resscn 11117	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 3943	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11058  ℝcr 11059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-resscn 11117

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  mulrid  11162  recnd  11192  pnfnre  11205  mnfnre  11207  mul02  11342  ltaddneg  11379  ltaddnegr  11380  renegcli  11471  resubcl  11474  negn0  11593  negf1o  11594  ltaddsub2  11639  leaddsub2  11641  leltadd  11648  ltaddpos  11654  ltaddpos2  11655  posdif  11657  lenegcon1  11668  lenegcon2  11669  addge01  11674  addge02  11675  leaddle0  11679  mullt0  11683  recex  11796  ltm1  12006  prodgt02  12012  ltmul2  12015  lemul1  12016  lemul2  12017  lemul1a  12018  lemul2a  12019  ltmulgt12  12025  lemulge12  12027  gt0div  12030  ge0div  12031  mulge0b  12034  mulle0b  12035  ltmuldiv2  12038  ltdivmul  12039  ledivmul  12040  ltdivmul2  12041  lt2mul2div  12042  ledivmul2  12043  lemuldiv2  12045  ltdiv2  12050  ltrec1  12051  lerec2  12052  ledivdiv  12053  lediv2  12054  ltdiv23  12055  lediv23  12056  lediv12a  12057  recp1lt1  12062  ledivp1  12066  negfi  12113  infm3lem  12122  supmul  12136  riotaneg  12143  negiso  12144  cju  12158  nnge1  12190  halfpos  12392  lt2halves  12397  addltmul  12398  avgle1  12402  avgle2  12403  avgle  12404  div4p1lem1div2  12417  nnrecl  12420  difgtsumgt  12475  elznn0  12523  elznn  12524  elz2  12526  nzadd  12560  zmulcl  12561  gtndiv  12589  zeo  12598  eqreznegel  12868  supminf  12869  rebtwnz  12881  irradd  12907  irrmul  12908  divlt1lt  12993  divle1le  12994  max0sub  13125  xnegneg  13143  rexsub  13162  xnegid  13167  xaddcom  13169  xaddrid  13170  xnegdi  13177  xaddass  13178  rexmul  13200  xmulasslem3  13215  xadddilem  13223  divelunit  13421  fzonmapblen  13628  ico01fl0  13734  flzadd  13741  ltdifltdiv  13749  dfceil2  13754  intfrac2  13773  fldiv2  13776  flpmodeq  13789  mod0  13791  negmod0  13793  modlt  13795  modfrac  13799  flmod  13800  intfrac  13801  modmulnn  13804  modvalp1  13805  modid  13811  modcyc  13821  modcyc2  13822  modadd1  13823  modaddabs  13824  muladdmodid  13826  negmod  13831  modadd2mod  13836  modmul1  13839  modmulmodr  13852  modaddmulmod  13853  moddi  13854  modsubdir  13855  modirr  13857  addmodlteq  13861  expgt1  14016  mulexpz  14018  sqgt0  14041  lt2sq  14048  le2sq  14049  sqge0  14051  expmordi  14082  leexp1a  14090  expubnd  14092  sumsqeq0  14093  sqlecan  14123  bernneq  14142  bernneq2  14143  expnbnd  14145  digit2  14149  digit1  14150  expnngt1  14154  swrdccatin2  14629  swrdccat3blem  14639  cshweqrep  14721  crre  15011  crim  15012  reim0  15015  mulre  15018  rere  15019  remul2  15027  rediv  15028  immul2  15034  imdiv  15035  cjre  15036  cjreim  15057  rennim  15136  resqrex  15147  resqreu  15149  resqrtcl  15150  resqrtthlem  15151  sqrtneglem  15163  sqrtneg  15164  absreimsq  15189  absreim  15190  absnid  15195  leabs  15196  absre  15198  absresq  15199  sqabs  15204  max0add  15207  absz  15208  absdiflt  15214  absdifle  15215  lenegsq  15217  abssuble0  15225  absmax  15226  rddif  15237  absrdbnd  15238  o1rlimmul  15513  caurcvg2  15574  reefcl  15980  efgt0  15996  reeftlcl  16001  resinval  16028  recosval  16029  resin4p  16031  recos4p  16032  resincl  16033  recoscl  16034  retancl  16035  resinhcl  16049  rpcoshcl  16050  retanhcl  16052  tanhlt1  16053  tanhbnd  16054  efieq  16056  sinbnd  16073  cosbnd  16074  absefi  16089  dvdsaddre2b  16200  odd2np1  16234  bezoutlem1  16431  xrsdsreclb  20881  remulg  21048  resubdrg  21049  remetdval  24189  bl2ioo  24192  ioo2bl  24193  cnperf  24220  icccvx  24350  tcphcph  24638  shft2rab  24909  volsup2  25006  volcn  25007  c1lip1  25398  plyreres  25680  aalioulem3  25731  taylthlem2  25770  reeff1o  25843  reefgim  25846  sincosq1sgn  25892  sincosq2sgn  25893  sincosq3sgn  25894  sincosq4sgn  25895  sinq12gt0  25901  pige3ALT  25913  efif1olem4  25938  efifo  25940  relogrn  25954  logrnaddcl  25967  relogoprlem  25983  advlog  26046  advlogexp  26047  logtayl  26052  recxpcl  26067  rpcxpcl  26068  cxpge0  26075  cxpcom  26129  dvcxp1  26130  logreclem  26149  relogbreexp  26162  relogbcxp  26172  angpieqvd  26218  atanre  26272  basellem9  26475  gausslemma2dlem1a  26750  2sqnn0  26823  log2sumbnd  26929  brbtwn2  27917  colinearalglem4  27921  colinearalg  27922  crctcshwlkn0lem1  28818  nvsge0  29669  nmoub3i  29778  nmlnoubi  29801  isblo3i  29806  ipasslem3  29838  ipasslem9  29843  ipasslem11  29845  hmopm  31026  riesz1  31070  leopmuli  31138  leopmul  31139  leopmul2i  31140  leopnmid  31143  nmopleid  31144  cdj1i  31438  cdj3lem1  31439  cdj3i  31446  addltmulALT  31451  dpfrac1  31818  rexdiv  31852  xdivid  31854  xdiv0  31855  rmulccn  32598  sgnneg  33229  lediv2aALT  34352  nndivlub  35006  irrdiff  35870  cos2h  36142  tan2h  36143  poimir  36184  mblfinlem2  36189  mblfinlem4  36191  itg2addnclem  36202  itg2addnclem2  36203  dvasin  36235  areacirclem1  36239  areacirclem2  36240  areacirclem4  36242  areacirclem5  36243  areacirc  36244  lcmineqlem12  40570  dvrelog2b  40596  aks4d1p1p6  40603  2xp3dxp2ge1d  40687  resubeulem2  40903  renegneg  40938  renegid2  40940  sn-it0e0  40942  sn-negex12  40943  resubeqsub  40956  sn-mullid  40962  sn-mul02  40967  areaquad  41608  reabssgn  42030  radcnvrat  42716  lhe4.4ex1a  42731  expgrowthi  42735  mulltgt0  43349  refsum2cnlem1  43364  infnsuprnmpt  43599  dstregt0  43636  suplesup  43694  infleinflem1  43725  infleinflem2  43726  ltdiv23neg  43749  rexabslelem  43773  supminfrnmpt  43800  supminfxr  43819  fmul01lt1lem1  43945  lptre2pt  44001  cnrefiisplem  44190  dvcosre  44273  itgsin0pilem1  44311  itgsinexplem1  44315  volioc  44333  volico  44344  stoweidlem7  44368  stoweidlem10  44371  stoweidlem19  44380  stoweidlem34  44395  stoweid  44424  dirker2re  44453  dirkerdenne0  44454  dirkerper  44457  dirkertrigeq  44462  dirkeritg  44463  fourierdlem39  44507  fourierdlem42  44510  fourierdlem47  44514  fourierdlem56  44523  fourierdlem57  44524  fourierdlem58  44525  fourierdlem60  44527  fourierdlem61  44528  fourierdlem73  44540  fourierdlem76  44543  fourierdlem77  44544  fourierdlem92  44559  fourierdlem97  44564  etransclem46  44641  volico2  45002  smflimlem4  45135  smfinflem  45178  et-sqrtnegnre  45234  2leaddle2  45650  ltsubsubaddltsub  45653  sqrtnegnre  45659  m1mod0mod1  45681  requad01  45933  requad1  45934  bgoldbtbndlem2  46118  flsubz  46723  rege1logbrege0  46764  nn0digval  46806  rrx2vlinest  46947  line2  46958  line2xlem  46959  line2x  46960  itscnhlc0yqe  46965  itsclc0yqsollem2  46969  itsclc0yqsol  46970  itscnhlc0xyqsol  46971  itschlc0xyqsol1  46972  itsclc0xyqsolr  46975  itsclquadb  46982  reseccl  47318  recsccl  47319  recotcl  47320