Theorem recn 9905

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  mulid1  9916  recnd  9947  pnfnre  9960  mnfnre  9961  mul02  10093  ltaddneg  10130  ltaddnegr  10131  renegcli  10221  resubcl  10224  negn0  10338  negf1o  10339  ltaddsub2  10382  leaddsub2  10384  leltadd  10391  ltaddpos  10397  ltaddpos2  10398  posdif  10400  lenegcon1  10411  lenegcon2  10412  addge01  10417  addge02  10418  leaddle0  10422  mullt0  10426  recex  10538  ltm1  10742  prodgt02  10748  prodge02  10750  ltmul2  10753  lemul1  10754  lemul2  10755  lemul1a  10756  lemul2a  10757  ltmulgt12  10763  lemulge12  10765  gt0div  10768  ge0div  10769  mulge0b  10772  mulle0b  10773  ltmuldiv2  10776  ltdivmul  10777  ledivmul  10778  ltdivmul2  10779  lt2mul2div  10780  ledivmul2  10781  lemuldiv2  10783  ltdiv2  10788  ltrec1  10789  lerec2  10790  ledivdiv  10791  lediv2  10792  ltdiv23  10793  lediv23  10794  lediv12a  10795  recp1lt1  10800  ledivp1  10804  negfi  10850  fiminre  10851  infm3lem  10860  supmul  10872  riotaneg  10879  negiso  10880  cju  10893  nnge1  10923  halfpos  11139  lt2halves  11144  addltmul  11145  avgle1  11149  avgle2  11150  avgle  11151  div4p1lem1div2  11164  nnrecl  11167  difgtsumgt  11223  elznn0  11269  elznn  11270  elz2  11271  nzadd  11302  zmulcl  11303  gtndiv  11330  zeo  11339  eqreznegel  11650  supminf  11651  rebtwnz  11663  irradd  11688  irrmul  11689  divlt1lt  11775  divle1le  11776  max0sub  11901  xnegneg  11919  rexsub  11938  xnegid  11943  xaddcom  11945  xaddid1  11946  xnegdi  11950  xaddass  11951  rexmul  11973  xmulasslem3  11988  xadddilem  11996  divelunit  12185  fzonmapblen  12381  ico01fl0  12482  flzadd  12489  ltdifltdiv  12497  dfceil2  12502  intfrac2  12519  fldiv2  12522  flpmodeq  12535  mod0  12537  negmod0  12539  modlt  12541  modfrac  12545  flmod  12546  intfrac  12547  modmulnn  12550  modvalp1  12551  modid  12557  modcyc  12567  modcyc2  12568  modadd1  12569  modaddabs  12570  muladdmodid  12572  negmod  12577  modadd2mod  12582  modmul1  12585  modmulmodr  12598  modaddmulmod  12599  moddi  12600  modsubdir  12601  modirr  12603  addmodlteq  12607  expgt1  12760  mulexpz  12762  leexp1a  12781  expubnd  12783  sqgt0  12794  lt2sq  12799  le2sq  12800  sqge0  12802  sumsqeq0  12804  sqlecan  12833  bernneq  12852  bernneq2  12853  expnbnd  12855  digit2  12859  digit1  12860  swrdccatin2  13338  swrdccat3blem  13346  cshweqrep  13418  crre  13702  crim  13703  reim0  13706  mulre  13709  rere  13710  remul2  13718  rediv  13719  immul2  13725  imdiv  13726  cjre  13727  cjreim  13748  rennim  13827  resqrex  13839  resqreu  13841  resqrtcl  13842  resqrtthlem  13843  sqrtneglem  13855  sqrtneg  13856  absreimsq  13880  absreim  13881  absnid  13886  leabs  13887  absre  13889  absresq  13890  sqabs  13895  max0add  13898  absz  13899  absdiflt  13905  absdifle  13906  lenegsq  13908  abssuble0  13916  absmax  13917  rddif  13928  absrdbnd  13929  o1rlimmul  14197  caurcvg2  14256  reefcl  14656  efgt0  14672  reeftlcl  14677  resinval  14704  recosval  14705  resin4p  14707  recos4p  14708  resincl  14709  recoscl  14710  retancl  14711  resinhcl  14725  rpcoshcl  14726  retanhcl  14728  tanhlt1  14729  tanhbnd  14730  efieq  14732  sinbnd  14749  cosbnd  14750  absefi  14765  dvdsaddre2b  14867  odd2np1  14903  bezoutlem1  15094  xrsdsreclb  19612  remulg  19772  resubdrg  19773  remetdval  22400  bl2ioo  22403  ioo2bl  22404  cnperf  22431  icccvx  22557  tchcph  22844  shft2rab  23083  volsup2  23179  volcn  23180  c1lip1  23564  plyreres  23842  aalioulem3  23893  taylthlem2  23932  reeff1o  24005  reefgim  24008  sincosq1sgn  24054  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  sinq12gt0  24063  pige3  24073  efif1olem4  24095  efifo  24097  relogrn  24112  logrnaddcl  24125  relogoprlem  24141  advlog  24200  advlogexp  24201  logtayl  24206  recxpcl  24221  rpcxpcl  24222  cxpge0  24229  dvcxp1  24281  logreclem  24300  relogbreexp  24313  relogbcxp  24323  angpieqvd  24358  atanre  24412  basellem9  24615  gausslemma2dlem1a  24890  log2sumbnd  25033  brbtwn2  25585  colinearalglem4  25589  colinearalg  25590  nvsge0  26903  nmoub3i  27012  nmlnoubi  27035  isblo3i  27040  ipasslem3  27072  ipasslem9  27077  ipasslem11  27079  hmopm  28264  riesz1  28308  leopmuli  28376  leopmul  28377  leopmul2i  28378  leopnmid  28381  nmopleid  28382  cdj1i  28676  cdj3lem1  28677  cdj3i  28684  addltmulALT  28689  rexdiv  28965  xdivid  28967  xdiv0  28968  rmulccn  29302  sgnneg  29929  lediv2aALT  30825  nndivlub  31627  cos2h  32570  tan2h  32571  poimir  32612  mblfinlem2  32617  mblfinlem4  32619  itg2addnclem  32631  itg2addnclem2  32632  dvasin  32666  areacirclem1  32670  areacirclem2  32671  areacirclem4  32673  areacirclem5  32674  areacirc  32675  expmordi  36530  areaquad  36821  radcnvrat  37535  lhe4.4ex1a  37550  expgrowthi  37554  mulltgt0  38204  refsum2cnlem1  38219  dstregt0  38434  suplesup  38496  infleinflem1  38527  infleinflem2  38528  ltdiv23neg  38558  fmul01lt1lem1  38651  lptre2pt  38707  dvcosre  38799  itgsin0pilem1  38841  itgsinexplem1  38845  volioc  38864  volico  38876  stoweidlem7  38900  stoweidlem10  38903  stoweidlem19  38912  stoweidlem34  38927  stoweid  38956  dirker2re  38985  dirkerdenne0  38986  dirkerper  38989  dirkertrigeq  38994  dirkeritg  38995  fourierdlem39  39039  fourierdlem42  39042  fourierdlem47  39046  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem60  39059  fourierdlem61  39060  fourierdlem73  39072  fourierdlem76  39075  fourierdlem77  39076  fourierdlem92  39091  fourierdlem97  39096  etransclem46  39173  volico2  39531  smflimlem4  39660  m1mod0mod1  39949  bgoldbtbndlem2  40222  2leaddle2  40344  ltsubsubaddltsub  40347  crctcsh1wlkn0lem1  41013  flsubz  42106  rege1logbrege0  42150  nn0digval  42192  reseccl  42293  recsccl  42294  recotcl  42295  dpfrac1  42312  dpfrac1OLD  42313