Theorem recn 11274

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  ℝcr 11183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  mulrid  11288  recnd  11318  pnfnre  11331  mnfnre  11333  mul02  11468  ltaddneg  11505  ltaddnegr  11506  renegcli  11597  resubcl  11600  negn0  11719  negf1o  11720  ltaddsub2  11765  leaddsub2  11767  leltadd  11774  ltaddpos  11780  ltaddpos2  11781  posdif  11783  lenegcon1  11794  lenegcon2  11795  addge01  11800  addge02  11801  leaddle0  11805  mullt0  11809  recex  11922  ltm1  12136  prodgt02  12142  ltmul2  12145  lemul1  12146  lemul2  12147  lemul1a  12148  lemul2a  12149  ltmulgt12  12155  lemulge12  12158  gt0div  12161  ge0div  12162  mulge0b  12165  mulle0b  12166  ltmuldiv2  12169  ltdivmul  12170  ledivmul  12171  ltdivmul2  12172  lt2mul2div  12173  ledivmul2  12174  lemuldiv2  12176  ltdiv2  12181  ltrec1  12182  lerec2  12183  ledivdiv  12184  lediv2  12185  ltdiv23  12186  lediv23  12187  lediv12a  12188  recp1lt1  12193  ledivp1  12197  negfi  12244  infm3lem  12253  supmul  12267  riotaneg  12274  negiso  12275  cju  12289  nnge1  12321  halfpos  12523  lt2halves  12528  addltmul  12529  avgle1  12533  avgle2  12534  avgle  12535  div4p1lem1div2  12548  nnrecl  12551  difgtsumgt  12606  elznn0  12654  elznn  12655  elz2  12657  nzadd  12691  zmulcl  12692  gtndiv  12720  zeo  12729  eqreznegel  12999  supminf  13000  rebtwnz  13012  irradd  13038  irrmul  13039  divlt1lt  13126  divle1le  13127  max0sub  13258  xnegneg  13276  rexsub  13295  xnegid  13300  xaddcom  13302  xaddrid  13303  xnegdi  13310  xaddass  13311  rexmul  13333  xmulasslem3  13348  xadddilem  13356  divelunit  13554  fzonmapblen  13762  ico01fl0  13870  flzadd  13877  ltdifltdiv  13885  dfceil2  13890  intfrac2  13909  fldiv2  13912  flpmodeq  13925  mod0  13927  negmod0  13929  modlt  13931  modfrac  13935  flmod  13936  intfrac  13937  modmulnn  13940  modvalp1  13941  modid  13947  modcyc  13957  modcyc2  13958  modadd1  13959  modaddabs  13960  muladdmodid  13962  negmod  13967  modadd2mod  13972  modmul1  13975  modmulmodr  13988  modaddmulmod  13989  moddi  13990  modsubdir  13991  modirr  13993  addmodlteq  13997  expgt1  14151  mulexpz  14153  sqgt0  14176  lt2sq  14183  le2sq  14184  sqge0  14186  expmordi  14217  leexp1a  14225  expubnd  14227  sumsqeq0  14228  sqlecan  14258  bernneq  14278  bernneq2  14279  expnbnd  14281  digit2  14285  digit1  14286  expnngt1  14290  swrdccatin2  14777  swrdccat3blem  14787  cshweqrep  14869  crre  15163  crim  15164  reim0  15167  mulre  15170  rere  15171  remul2  15179  rediv  15180  immul2  15186  imdiv  15187  cjre  15188  cjreim  15209  rennim  15288  resqrex  15299  resqreu  15301  resqrtcl  15302  resqrtthlem  15303  sqrtneglem  15315  sqrtneg  15316  absreimsq  15341  absreim  15342  absnid  15347  leabs  15348  absre  15350  absresq  15351  sqabs  15356  max0add  15359  absz  15360  absdiflt  15366  absdifle  15367  lenegsq  15369  abssuble0  15377  absmax  15378  rddif  15389  absrdbnd  15390  o1rlimmul  15665  caurcvg2  15726  reefcl  16135  efgt0  16151  reeftlcl  16156  resinval  16183  recosval  16184  resin4p  16186  recos4p  16187  resincl  16188  recoscl  16189  retancl  16190  resinhcl  16204  rpcoshcl  16205  retanhcl  16207  tanhlt1  16208  tanhbnd  16209  efieq  16211  sinbnd  16228  cosbnd  16229  absefi  16244  dvdsaddre2b  16355  odd2np1  16389  bezoutlem1  16586  xrsdsreclb  21454  remulg  21648  resubdrg  21649  remetdval  24830  bl2ioo  24833  ioo2bl  24834  cnperf  24861  icccvx  25000  tcphcph  25290  shft2rab  25562  volsup2  25659  volcn  25660  c1lip1  26056  plyreres  26342  aalioulem3  26394  taylthlem2  26434  taylthlem2OLD  26435  reeff1o  26509  reefgim  26512  sincosq1sgn  26558  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  sinq12gt0  26567  pige3ALT  26580  efif1olem4  26605  efifo  26607  relogrn  26621  logrnaddcl  26634  relogoprlem  26651  advlog  26714  advlogexp  26715  logtayl  26720  recxpcl  26735  rpcxpcl  26736  cxpge0  26743  cxpcom  26799  dvcxp1  26800  logreclem  26823  relogbreexp  26836  relogbcxp  26846  angpieqvd  26892  atanre  26946  basellem9  27150  gausslemma2dlem1a  27427  2sqnn0  27500  log2sumbnd  27606  brbtwn2  28938  colinearalglem4  28942  colinearalg  28943  crctcshwlkn0lem1  29843  nvsge0  30696  nmoub3i  30805  nmlnoubi  30828  isblo3i  30833  ipasslem3  30865  ipasslem9  30870  ipasslem11  30872  hmopm  32053  riesz1  32097  leopmuli  32165  leopmul  32166  leopmul2i  32167  leopnmid  32170  nmopleid  32171  cdj1i  32465  cdj3lem1  32466  cdj3i  32473  addltmulALT  32478  dpfrac1  32856  rexdiv  32890  xdivid  32892  xdiv0  32893  sgnneg  34505  lediv2aALT  35645  nndivlub  36424  irrdiff  37292  cos2h  37571  tan2h  37572  poimir  37613  mblfinlem2  37618  mblfinlem4  37620  itg2addnclem  37631  itg2addnclem2  37632  dvasin  37664  areacirclem1  37668  areacirclem2  37669  areacirclem4  37671  areacirclem5  37672  areacirc  37673  lcmineqlem12  41997  dvrelog2b  42023  aks4d1p1p6  42030  2xp3dxp2ge1d  42198  retire  42308  resubeulem2  42352  renegneg  42387  renegid2  42389  sn-it0e0  42391  sn-negex12  42392  resubeqsub  42405  sn-mullid  42411  sn-mul02  42416  areaquad  43177  reabssgn  43598  radcnvrat  44283  lhe4.4ex1a  44298  expgrowthi  44302  mulltgt0  44922  refsum2cnlem1  44937  infnsuprnmpt  45159  dstregt0  45196  suplesup  45254  infleinflem1  45285  infleinflem2  45286  ltdiv23neg  45309  rexabslelem  45333  supminfrnmpt  45360  supminfxr  45379  fmul01lt1lem1  45505  lptre2pt  45561  cnrefiisplem  45750  dvcosre  45833  itgsin0pilem1  45871  itgsinexplem1  45875  volioc  45893  volico  45904  stoweidlem7  45928  stoweidlem10  45931  stoweidlem19  45940  stoweidlem34  45955  stoweid  45984  dirker2re  46013  dirkerdenne0  46014  dirkerper  46017  dirkertrigeq  46022  dirkeritg  46023  fourierdlem39  46067  fourierdlem42  46070  fourierdlem47  46074  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem60  46087  fourierdlem61  46088  fourierdlem73  46100  fourierdlem76  46103  fourierdlem77  46104  fourierdlem92  46119  fourierdlem97  46124  etransclem46  46201  volico2  46562  smflimlem4  46695  smfinflem  46738  et-sqrtnegnre  46794  2leaddle2  47213  ltsubsubaddltsub  47216  sqrtnegnre  47222  m1mod0mod1  47243  requad01  47495  requad1  47496  bgoldbtbndlem2  47680  flsubz  48251  rege1logbrege0  48292  nn0digval  48334  rrx2vlinest  48475  line2  48486  line2xlem  48487  line2x  48488  itscnhlc0yqe  48493  itsclc0yqsollem2  48497  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itsclc0xyqsolr  48503  itsclquadb  48510  reseccl  48845  recsccl  48846  recotcl  48847