Theorem recn 10627

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  ℝcr 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  mulid1  10639  recnd  10669  pnfnre  10682  mnfnre  10684  mul02  10818  ltaddneg  10855  ltaddnegr  10856  renegcli  10947  resubcl  10950  negn0  11069  negf1o  11070  ltaddsub2  11115  leaddsub2  11117  leltadd  11124  ltaddpos  11130  ltaddpos2  11131  posdif  11133  lenegcon1  11144  lenegcon2  11145  addge01  11150  addge02  11151  leaddle0  11155  mullt0  11159  recex  11272  ltm1  11482  prodgt02  11488  ltmul2  11491  lemul1  11492  lemul2  11493  lemul1a  11494  lemul2a  11495  ltmulgt12  11501  lemulge12  11503  gt0div  11506  ge0div  11507  mulge0b  11510  mulle0b  11511  ltmuldiv2  11514  ltdivmul  11515  ledivmul  11516  ltdivmul2  11517  lt2mul2div  11518  ledivmul2  11519  lemuldiv2  11521  ltdiv2  11526  ltrec1  11527  lerec2  11528  ledivdiv  11529  lediv2  11530  ltdiv23  11531  lediv23  11532  lediv12a  11533  recp1lt1  11538  ledivp1  11542  negfi  11589  fiminreOLD  11590  infm3lem  11599  supmul  11613  riotaneg  11620  negiso  11621  cju  11634  nnge1  11666  halfpos  11868  lt2halves  11873  addltmul  11874  avgle1  11878  avgle2  11879  avgle  11880  div4p1lem1div2  11893  nnrecl  11896  difgtsumgt  11951  elznn0  11997  elznn  11998  elz2  12000  nzadd  12031  zmulcl  12032  gtndiv  12060  zeo  12069  eqreznegel  12335  supminf  12336  rebtwnz  12348  irradd  12373  irrmul  12374  divlt1lt  12459  divle1le  12460  max0sub  12590  xnegneg  12608  rexsub  12627  xnegid  12632  xaddcom  12634  xaddid1  12635  xnegdi  12642  xaddass  12643  rexmul  12665  xmulasslem3  12680  xadddilem  12688  divelunit  12881  fzonmapblen  13084  ico01fl0  13190  flzadd  13197  ltdifltdiv  13205  dfceil2  13210  intfrac2  13227  fldiv2  13230  flpmodeq  13243  mod0  13245  negmod0  13247  modlt  13249  modfrac  13253  flmod  13254  intfrac  13255  modmulnn  13258  modvalp1  13259  modid  13265  modcyc  13275  modcyc2  13276  modadd1  13277  modaddabs  13278  muladdmodid  13280  negmod  13285  modadd2mod  13290  modmul1  13293  modmulmodr  13306  modaddmulmod  13307  moddi  13308  modsubdir  13309  modirr  13311  addmodlteq  13315  expgt1  13468  mulexpz  13470  sqgt0  13492  lt2sq  13499  le2sq  13500  sqge0  13502  expmordi  13532  leexp1a  13540  expubnd  13542  sumsqeq0  13543  sqlecan  13572  bernneq  13591  bernneq2  13592  expnbnd  13594  digit2  13598  digit1  13599  expnngt1  13603  swrdccatin2  14091  swrdccat3blem  14101  cshweqrep  14183  crre  14473  crim  14474  reim0  14477  mulre  14480  rere  14481  remul2  14489  rediv  14490  immul2  14496  imdiv  14497  cjre  14498  cjreim  14519  rennim  14598  resqrex  14610  resqreu  14612  resqrtcl  14613  resqrtthlem  14614  sqrtneglem  14626  sqrtneg  14627  absreimsq  14652  absreim  14653  absnid  14658  leabs  14659  absre  14661  absresq  14662  sqabs  14667  max0add  14670  absz  14671  absdiflt  14677  absdifle  14678  lenegsq  14680  abssuble0  14688  absmax  14689  rddif  14700  absrdbnd  14701  o1rlimmul  14975  caurcvg2  15034  reefcl  15440  efgt0  15456  reeftlcl  15461  resinval  15488  recosval  15489  resin4p  15491  recos4p  15492  resincl  15493  recoscl  15494  retancl  15495  resinhcl  15509  rpcoshcl  15510  retanhcl  15512  tanhlt1  15513  tanhbnd  15514  efieq  15516  sinbnd  15533  cosbnd  15534  absefi  15549  dvdsaddre2b  15657  odd2np1  15690  bezoutlem1  15887  xrsdsreclb  20592  remulg  20751  resubdrg  20752  remetdval  23397  bl2ioo  23400  ioo2bl  23401  cnperf  23428  icccvx  23554  tcphcph  23840  shft2rab  24109  volsup2  24206  volcn  24207  c1lip1  24594  plyreres  24872  aalioulem3  24923  taylthlem2  24962  reeff1o  25035  reefgim  25038  sincosq1sgn  25084  sincosq2sgn  25085  sincosq3sgn  25086  sincosq4sgn  25087  sinq12gt0  25093  pige3ALT  25105  efif1olem4  25129  efifo  25131  relogrn  25145  logrnaddcl  25158  relogoprlem  25174  advlog  25237  advlogexp  25238  logtayl  25243  recxpcl  25258  rpcxpcl  25259  cxpge0  25266  cxpcom  25320  dvcxp1  25321  logreclem  25340  relogbreexp  25353  relogbcxp  25363  angpieqvd  25409  atanre  25463  basellem9  25666  gausslemma2dlem1a  25941  2sqnn0  26014  log2sumbnd  26120  brbtwn2  26691  colinearalglem4  26695  colinearalg  26696  crctcshwlkn0lem1  27588  nvsge0  28441  nmoub3i  28550  nmlnoubi  28573  isblo3i  28578  ipasslem3  28610  ipasslem9  28615  ipasslem11  28617  hmopm  29798  riesz1  29842  leopmuli  29910  leopmul  29911  leopmul2i  29912  leopnmid  29915  nmopleid  29916  cdj1i  30210  cdj3lem1  30211  cdj3i  30218  addltmulALT  30223  dpfrac1  30568  rexdiv  30602  xdivid  30604  xdiv0  30605  rmulccn  31171  sgnneg  31798  lediv2aALT  32920  nndivlub  33806  cos2h  34898  tan2h  34899  poimir  34940  mblfinlem2  34945  mblfinlem4  34947  itg2addnclem  34958  itg2addnclem2  34959  dvasin  34993  areacirclem1  34997  areacirclem2  34998  areacirclem4  35000  areacirclem5  35001  areacirc  35002  2xp3dxp2ge1d  39146  resubeulem2  39255  renegneg  39290  areaquad  39872  radcnvrat  40695  lhe4.4ex1a  40710  expgrowthi  40714  mulltgt0  41328  refsum2cnlem1  41343  infnsuprnmpt  41571  dstregt0  41596  suplesup  41656  infleinflem1  41687  infleinflem2  41688  ltdiv23neg  41715  rexabslelem  41741  supminfrnmpt  41768  supminfxr  41789  fmul01lt1lem1  41914  lptre2pt  41970  cnrefiisplem  42159  dvcosre  42245  itgsin0pilem1  42284  itgsinexplem1  42288  volioc  42306  volico  42317  stoweidlem7  42341  stoweidlem10  42344  stoweidlem19  42353  stoweidlem34  42368  stoweid  42397  dirker2re  42426  dirkerdenne0  42427  dirkerper  42430  dirkertrigeq  42435  dirkeritg  42436  fourierdlem39  42480  fourierdlem42  42483  fourierdlem47  42487  fourierdlem56  42496  fourierdlem57  42497  fourierdlem58  42498  fourierdlem60  42500  fourierdlem61  42501  fourierdlem73  42513  fourierdlem76  42516  fourierdlem77  42517  fourierdlem92  42532  fourierdlem97  42537  etransclem46  42614  volico2  42972  smflimlem4  43099  smfinflem  43140  2leaddle2  43547  ltsubsubaddltsub  43550  sqrtnegnre  43556  m1mod0mod1  43578  requad01  43835  requad1  43836  bgoldbtbndlem2  44020  flsubz  44626  rege1logbrege0  44667  nn0digval  44709  rrx2vlinest  44777  line2  44788  line2xlem  44789  line2x  44790  itscnhlc0yqe  44795  itsclc0yqsollem2  44799  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itsclc0xyqsolr  44805  itsclquadb  44812  reseccl  44901  recsccl  44902  recotcl  44903