Theorem recn 11217

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 11184	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 3954	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  ℝcr 11126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-ss 3943

This theorem is referenced by:  mulrid  11231  recnd  11261  pnfnre  11274  mnfnre  11276  mul02  11411  ltaddneg  11449  ltaddnegr  11450  renegcli  11542  resubcl  11545  negn0  11664  negf1o  11665  ltaddsub2  11710  leaddsub2  11712  leltadd  11719  ltaddpos  11725  ltaddpos2  11726  posdif  11728  lenegcon1  11739  lenegcon2  11740  addge01  11745  addge02  11746  leaddle0  11750  mullt0  11754  recex  11867  ltm1  12081  prodgt02  12087  ltmul2  12090  lemul1  12091  lemul2  12092  lemul1a  12093  lemul2a  12094  ltmulgt12  12100  lemulge12  12103  gt0div  12106  ge0div  12107  mulge0b  12110  mulle0b  12111  ltmuldiv2  12114  ltdivmul  12115  ledivmul  12116  ltdivmul2  12117  lt2mul2div  12118  ledivmul2  12119  lemuldiv2  12121  ltdiv2  12126  ltrec1  12127  lerec2  12128  ledivdiv  12129  lediv2  12130  ltdiv23  12131  lediv23  12132  lediv12a  12133  recp1lt1  12138  ledivp1  12142  negfi  12189  infm3lem  12198  supmul  12212  riotaneg  12219  negiso  12220  cju  12234  nnge1  12266  halfpos  12469  lt2halves  12474  addltmul  12475  avgle1  12479  avgle2  12480  avgle  12481  div4p1lem1div2  12494  nnrecl  12497  difgtsumgt  12552  elznn0  12601  elznn  12602  elz2  12604  nzadd  12638  zmulcl  12639  gtndiv  12668  zeo  12677  eqreznegel  12948  supminf  12949  rebtwnz  12961  irradd  12987  irrmul  12988  divlt1lt  13076  divle1le  13077  max0sub  13210  xnegneg  13228  rexsub  13247  xnegid  13252  xaddcom  13254  xaddrid  13255  xnegdi  13262  xaddass  13263  rexmul  13285  xmulasslem3  13300  xadddilem  13308  divelunit  13509  fzonmapblen  13723  ico01fl0  13834  flzadd  13841  ltdifltdiv  13849  dfceil2  13854  intfrac2  13873  fldiv2  13876  flpmodeq  13889  mod0  13891  negmod0  13893  modlt  13895  modfrac  13899  flmod  13900  intfrac  13901  modmulnn  13904  modvalp1  13905  modid  13911  modcyc  13921  modcyc2  13922  modadd1  13923  modaddabs  13924  muladdmodid  13926  muladdmod  13928  negmod  13932  modadd2mod  13937  modmul1  13940  modmulmodr  13953  modaddmulmod  13954  moddi  13955  modsubdir  13956  modirr  13958  addmodlteq  13962  expgt1  14116  mulexpz  14118  sqgt0  14142  lt2sq  14149  le2sq  14150  sqge0  14152  expmordi  14183  leexp1a  14191  expubnd  14194  sumsqeq0  14195  sqlecan  14225  bernneq  14245  bernneq2  14246  expnbnd  14248  digit2  14252  digit1  14253  expnngt1  14257  swrdccatin2  14745  swrdccat3blem  14755  cshweqrep  14837  crre  15131  crim  15132  reim0  15135  mulre  15138  rere  15139  remul2  15147  rediv  15148  immul2  15154  imdiv  15155  cjre  15156  cjreim  15177  rennim  15256  resqrex  15267  resqreu  15269  resqrtcl  15270  resqrtthlem  15271  sqrtneglem  15283  sqrtneg  15284  absreimsq  15309  absreim  15310  absnid  15315  leabs  15316  absre  15318  absresq  15319  sqabs  15324  max0add  15327  absz  15328  absdiflt  15334  absdifle  15335  lenegsq  15337  abssuble0  15345  absmax  15346  rddif  15357  absrdbnd  15358  o1rlimmul  15633  caurcvg2  15692  reefcl  16101  efgt0  16119  reeftlcl  16124  resinval  16151  recosval  16152  resin4p  16154  recos4p  16155  resincl  16156  recoscl  16157  retancl  16158  resinhcl  16172  rpcoshcl  16173  retanhcl  16175  tanhlt1  16176  tanhbnd  16177  efieq  16179  sinbnd  16196  cosbnd  16197  absefi  16212  dvdsaddre2b  16324  odd2np1  16358  bezoutlem1  16556  xrsdsreclb  21379  remulg  21565  resubdrg  21566  remetdval  24726  bl2ioo  24729  ioo2bl  24730  cnperf  24758  icccvx  24897  tcphcph  25187  shft2rab  25459  volsup2  25556  volcn  25557  c1lip1  25952  plyreres  26240  aalioulem3  26292  taylthlem2  26332  taylthlem2OLD  26333  reeff1o  26407  reefgim  26410  sincosq1sgn  26457  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  sinq12gt0  26466  pige3ALT  26479  efif1olem4  26504  efifo  26506  relogrn  26520  logrnaddcl  26533  relogoprlem  26550  advlog  26613  advlogexp  26614  logtayl  26619  recxpcl  26634  rpcxpcl  26635  cxpge0  26642  cxpcom  26698  dvcxp1  26699  logreclem  26722  relogbreexp  26735  relogbcxp  26745  angpieqvd  26791  atanre  26845  basellem9  27049  gausslemma2dlem1a  27326  2sqnn0  27399  log2sumbnd  27505  brbtwn2  28830  colinearalglem4  28834  colinearalg  28835  crctcshwlkn0lem1  29738  nvsge0  30591  nmoub3i  30700  nmlnoubi  30723  isblo3i  30728  ipasslem3  30760  ipasslem9  30765  ipasslem11  30767  hmopm  31948  riesz1  31992  leopmuli  32060  leopmul  32061  leopmul2i  32062  leopnmid  32065  nmopleid  32066  cdj1i  32360  cdj3lem1  32361  cdj3i  32368  addltmulALT  32373  sgnneg  32758  dpfrac1  32812  rexdiv  32846  xdivid  32848  xdiv0  32849  lediv2aALT  35645  nndivlub  36422  irrdiff  37290  cos2h  37581  tan2h  37582  poimir  37623  mblfinlem2  37628  mblfinlem4  37630  itg2addnclem  37641  itg2addnclem2  37642  dvasin  37674  areacirclem1  37678  areacirclem2  37679  areacirclem4  37681  areacirclem5  37682  areacirc  37683  lcmineqlem12  41999  dvrelog2b  42025  aks4d1p1p6  42032  2xp3dxp2ge1d  42200  retire  42315  readvrec2  42351  readvrec  42352  resubeulem2  42366  renegneg  42401  renegid2  42403  sn-it0e0  42405  sn-negex12  42406  resubeqsub  42419  sn-mullid  42425  sn-mul02  42430  areaquad  43187  reabssgn  43607  radcnvrat  44286  lhe4.4ex1a  44301  expgrowthi  44305  mulltgt0  44994  refsum2cnlem1  45009  infnsuprnmpt  45222  dstregt0  45258  suplesup  45314  infleinflem1  45345  infleinflem2  45346  ltdiv23neg  45369  rexabslelem  45393  supminfrnmpt  45420  supminfxr  45439  fmul01lt1lem1  45561  lptre2pt  45617  cnrefiisplem  45806  dvcosre  45889  itgsin0pilem1  45927  itgsinexplem1  45931  volioc  45949  volico  45960  stoweidlem7  45984  stoweidlem10  45987  stoweidlem19  45996  stoweidlem34  46011  stoweid  46040  dirker2re  46069  dirkerdenne0  46070  dirkerper  46073  dirkertrigeq  46078  dirkeritg  46079  fourierdlem39  46123  fourierdlem42  46126  fourierdlem47  46130  fourierdlem56  46139  fourierdlem57  46140  fourierdlem58  46141  fourierdlem60  46143  fourierdlem61  46144  fourierdlem73  46156  fourierdlem76  46159  fourierdlem77  46160  fourierdlem92  46175  fourierdlem97  46180  etransclem46  46257  volico2  46618  smflimlem4  46751  smfinflem  46794  et-sqrtnegnre  46850  squeezedltsq  46866  2leaddle2  47275  ltsubsubaddltsub  47278  sqrtnegnre  47284  ceildivmod  47316  m1mod0mod1  47331  requad01  47583  requad1  47584  bgoldbtbndlem2  47768  flsubz  48446  rege1logbrege0  48486  nn0digval  48528  rrx2vlinest  48669  line2  48680  line2xlem  48681  line2x  48682  itscnhlc0yqe  48687  itsclc0yqsollem2  48691  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itsclc0xyqsolr  48697  itsclquadb  48704  reseccl  49565  recsccl  49566  recotcl  49567