Theorem recn 11128

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℝcr 11037

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920

This theorem is referenced by:  mulrid  11142  recnd  11172  pnfnre  11185  mnfnre  11187  mul02  11323  ltaddneg  11361  ltaddnegr  11362  renegcli  11454  resubcl  11457  negn0  11578  negf1o  11579  ltaddsub2  11624  leaddsub2  11626  leltadd  11633  ltaddpos  11639  ltaddpos2  11640  posdif  11642  lenegcon1  11653  lenegcon2  11654  addge01  11659  addge02  11660  leaddle0  11664  mullt0  11668  recex  11781  ltm1  11995  prodgt02  12001  ltmul2  12004  lemul1  12005  lemul2  12006  lemul1a  12007  lemul2a  12008  ltmulgt12  12014  lemulge12  12017  gt0div  12020  ge0div  12021  mulge0b  12024  mulle0b  12025  ltmuldiv2  12028  ltdivmul  12029  ledivmul  12030  ltdivmul2  12031  lt2mul2div  12032  ledivmul2  12033  lemuldiv2  12035  ltdiv2  12040  ltrec1  12041  lerec2  12042  ledivdiv  12043  lediv2  12044  ltdiv23  12045  lediv23  12046  lediv12a  12047  recp1lt1  12052  ledivp1  12056  negfi  12103  infm3lem  12112  supmul  12126  riotaneg  12133  negiso  12134  cju  12153  nnge1  12185  halfpos  12383  lt2halves  12388  addltmul  12389  avgle1  12393  avgle2  12394  avgle  12395  div4p1lem1div2  12408  nnrecl  12411  difgtsumgt  12466  elznn0  12515  elznn  12516  elz2  12518  nzadd  12551  zmulcl  12552  gtndiv  12581  zeo  12590  eqreznegel  12859  supminf  12860  rebtwnz  12872  irradd  12898  irrmul  12899  divlt1lt  12988  divle1le  12989  max0sub  13123  xnegneg  13141  rexsub  13160  xnegid  13165  xaddcom  13167  xaddrid  13168  xnegdi  13175  xaddass  13176  rexmul  13198  xmulasslem3  13213  xadddilem  13221  divelunit  13422  fzonmapblen  13636  ico01fl0  13751  flzadd  13758  ltdifltdiv  13766  dfceil2  13771  intfrac2  13790  fldiv2  13793  flpmodeq  13806  mod0  13808  negmod0  13810  modlt  13812  modfrac  13816  flmod  13817  intfrac  13818  modmulnn  13821  modvalp1  13822  modid  13828  modcyc  13838  modcyc2  13839  modadd1  13840  modaddabs  13843  muladdmodid  13845  muladdmod  13847  negmod  13851  modadd2mod  13856  modmul1  13859  modmulmodr  13872  modaddmulmod  13873  moddi  13874  modsubdir  13875  modirr  13877  addmodlteq  13881  expgt1  14035  mulexpz  14037  sqgt0  14061  lt2sq  14068  le2sq  14069  sqge0  14071  expmordi  14102  leexp1a  14110  expubnd  14113  sumsqeq0  14114  sqlecan  14144  bernneq  14164  bernneq2  14165  expnbnd  14167  digit2  14171  digit1  14172  expnngt1  14176  swrdccatin2  14664  swrdccat3blem  14674  cshweqrep  14756  crre  15049  crim  15050  reim0  15053  mulre  15056  rere  15057  remul2  15065  rediv  15066  immul2  15072  imdiv  15073  cjre  15074  cjreim  15095  rennim  15174  resqrex  15185  resqreu  15187  resqrtcl  15188  resqrtthlem  15189  sqrtneglem  15201  sqrtneg  15202  absreimsq  15227  absreim  15228  absnid  15233  leabs  15234  absre  15236  absresq  15237  sqabs  15242  max0add  15245  absz  15246  absdiflt  15253  absdifle  15254  lenegsq  15256  abssuble0  15264  absmax  15265  rddif  15276  absrdbnd  15277  o1rlimmul  15554  caurcvg2  15613  reefcl  16022  efgt0  16040  reeftlcl  16045  resinval  16072  recosval  16073  resin4p  16075  recos4p  16076  resincl  16077  recoscl  16078  retancl  16079  resinhcl  16093  rpcoshcl  16094  retanhcl  16096  tanhlt1  16097  tanhbnd  16098  efieq  16100  sinbnd  16117  cosbnd  16118  absefi  16133  dvdsaddre2b  16246  odd2np1  16280  bezoutlem1  16478  xrsdsreclb  21380  remulg  21574  resubdrg  21575  remetdval  24745  bl2ioo  24748  ioo2bl  24749  cnperf  24777  icccvx  24916  tcphcph  25205  shft2rab  25477  volsup2  25574  volcn  25575  c1lip1  25970  plyreres  26258  aalioulem3  26310  taylthlem2  26350  taylthlem2OLD  26351  reeff1o  26425  reefgim  26428  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12gt0  26484  pige3ALT  26497  efif1olem4  26522  efifo  26524  relogrn  26538  logrnaddcl  26551  relogoprlem  26568  advlog  26631  advlogexp  26632  logtayl  26637  recxpcl  26652  rpcxpcl  26653  cxpge0  26660  cxpcom  26716  dvcxp1  26717  logreclem  26740  relogbreexp  26753  relogbcxp  26763  angpieqvd  26809  atanre  26863  basellem9  27067  gausslemma2dlem1a  27344  2sqnn0  27417  log2sumbnd  27523  brbtwn2  28990  colinearalglem4  28994  colinearalg  28995  crctcshwlkn0lem1  29895  nvsge0  30751  nmoub3i  30860  nmlnoubi  30883  isblo3i  30888  ipasslem3  30920  ipasslem9  30925  ipasslem11  30927  hmopm  32108  riesz1  32152  leopmuli  32220  leopmul  32221  leopmul2i  32222  leopnmid  32225  nmopleid  32226  cdj1i  32520  cdj3lem1  32521  cdj3i  32528  addltmulALT  32533  sgnneg  32924  dpfrac1  32983  rexdiv  33017  xdivid  33019  xdiv0  33020  lediv2aALT  35890  nndivlub  36671  irrdiff  37575  cos2h  37856  tan2h  37857  poimir  37898  mblfinlem2  37903  mblfinlem4  37905  itg2addnclem  37916  itg2addnclem2  37917  dvasin  37949  areacirclem1  37953  areacirclem2  37954  areacirclem4  37956  areacirclem5  37957  areacirc  37958  lcmineqlem12  42404  dvrelog2b  42430  aks4d1p1p6  42437  retire  42683  readvrec2  42725  readvrec  42726  resubeulem2  42740  renegneg  42776  renegid2  42778  sn-it0e0  42780  sn-negex12  42781  resubeqsub  42794  sn-mullid  42800  sn-mul02  42816  areaquad  43567  reabssgn  43986  radcnvrat  44664  lhe4.4ex1a  44679  expgrowthi  44683  mulltgt0  45376  refsum2cnlem1  45391  infnsuprnmpt  45602  dstregt0  45638  suplesup  45692  infleinflem1  45722  infleinflem2  45723  ltdiv23neg  45746  rexabslelem  45770  supminfrnmpt  45797  supminfxr  45816  fmul01lt1lem1  45938  lptre2pt  45992  cnrefiisplem  46181  dvcosre  46264  itgsin0pilem1  46302  itgsinexplem1  46306  volioc  46324  volico  46335  stoweidlem7  46359  stoweidlem10  46362  stoweidlem19  46371  stoweidlem34  46386  stoweid  46415  dirker2re  46444  dirkerdenne0  46445  dirkerper  46448  dirkertrigeq  46453  dirkeritg  46454  fourierdlem39  46498  fourierdlem42  46501  fourierdlem47  46505  fourierdlem56  46514  fourierdlem57  46515  fourierdlem58  46516  fourierdlem60  46518  fourierdlem61  46519  fourierdlem73  46531  fourierdlem76  46534  fourierdlem77  46535  fourierdlem92  46550  fourierdlem97  46555  etransclem46  46632  volico2  46993  smflimlem4  47126  smfinflem  47169  et-sqrtnegnre  47225  squeezedltsq  47240  2leaddle2  47652  ltsubsubaddltsub  47655  sqrtnegnre  47661  ceildivmod  47693  m1mod0mod1  47708  requad01  47975  requad1  47976  bgoldbtbndlem2  48160  flsubz  48876  rege1logbrege0  48912  nn0digval  48954  rrx2vlinest  49095  line2  49106  line2xlem  49107  line2x  49108  itscnhlc0yqe  49113  itsclc0yqsollem2  49117  itsclc0yqsol  49118  itscnhlc0xyqsol  49119  itschlc0xyqsol1  49120  itsclc0xyqsolr  49123  itsclquadb  49130  reseccl  50106  recsccl  50107  recotcl  50108