Theorem recn 10970

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  ℝcr 10879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  mulid1  10982  recnd  11012  pnfnre  11025  mnfnre  11027  mul02  11162  ltaddneg  11199  ltaddnegr  11200  renegcli  11291  resubcl  11294  negn0  11413  negf1o  11414  ltaddsub2  11459  leaddsub2  11461  leltadd  11468  ltaddpos  11474  ltaddpos2  11475  posdif  11477  lenegcon1  11488  lenegcon2  11489  addge01  11494  addge02  11495  leaddle0  11499  mullt0  11503  recex  11616  ltm1  11826  prodgt02  11832  ltmul2  11835  lemul1  11836  lemul2  11837  lemul1a  11838  lemul2a  11839  ltmulgt12  11845  lemulge12  11847  gt0div  11850  ge0div  11851  mulge0b  11854  mulle0b  11855  ltmuldiv2  11858  ltdivmul  11859  ledivmul  11860  ltdivmul2  11861  lt2mul2div  11862  ledivmul2  11863  lemuldiv2  11865  ltdiv2  11870  ltrec1  11871  lerec2  11872  ledivdiv  11873  lediv2  11874  ltdiv23  11875  lediv23  11876  lediv12a  11877  recp1lt1  11882  ledivp1  11886  negfi  11933  infm3lem  11942  supmul  11956  riotaneg  11963  negiso  11964  cju  11978  nnge1  12010  halfpos  12212  lt2halves  12217  addltmul  12218  avgle1  12222  avgle2  12223  avgle  12224  div4p1lem1div2  12237  nnrecl  12240  difgtsumgt  12295  elznn0  12343  elznn  12344  elz2  12346  nzadd  12377  zmulcl  12378  gtndiv  12406  zeo  12415  eqreznegel  12683  supminf  12684  rebtwnz  12696  irradd  12722  irrmul  12723  divlt1lt  12808  divle1le  12809  max0sub  12939  xnegneg  12957  rexsub  12976  xnegid  12981  xaddcom  12983  xaddid1  12984  xnegdi  12991  xaddass  12992  rexmul  13014  xmulasslem3  13029  xadddilem  13037  divelunit  13235  fzonmapblen  13442  ico01fl0  13548  flzadd  13555  ltdifltdiv  13563  dfceil2  13568  intfrac2  13587  fldiv2  13590  flpmodeq  13603  mod0  13605  negmod0  13607  modlt  13609  modfrac  13613  flmod  13614  intfrac  13615  modmulnn  13618  modvalp1  13619  modid  13625  modcyc  13635  modcyc2  13636  modadd1  13637  modaddabs  13638  muladdmodid  13640  negmod  13645  modadd2mod  13650  modmul1  13653  modmulmodr  13666  modaddmulmod  13667  moddi  13668  modsubdir  13669  modirr  13671  addmodlteq  13675  expgt1  13830  mulexpz  13832  sqgt0  13854  lt2sq  13861  le2sq  13862  sqge0  13864  expmordi  13894  leexp1a  13902  expubnd  13904  sumsqeq0  13905  sqlecan  13934  bernneq  13953  bernneq2  13954  expnbnd  13956  digit2  13960  digit1  13961  expnngt1  13965  swrdccatin2  14451  swrdccat3blem  14461  cshweqrep  14543  crre  14834  crim  14835  reim0  14838  mulre  14841  rere  14842  remul2  14850  rediv  14851  immul2  14857  imdiv  14858  cjre  14859  cjreim  14880  rennim  14959  resqrex  14971  resqreu  14973  resqrtcl  14974  resqrtthlem  14975  sqrtneglem  14987  sqrtneg  14988  absreimsq  15013  absreim  15014  absnid  15019  leabs  15020  absre  15022  absresq  15023  sqabs  15028  max0add  15031  absz  15032  absdiflt  15038  absdifle  15039  lenegsq  15041  abssuble0  15049  absmax  15050  rddif  15061  absrdbnd  15062  o1rlimmul  15337  caurcvg2  15398  reefcl  15805  efgt0  15821  reeftlcl  15826  resinval  15853  recosval  15854  resin4p  15856  recos4p  15857  resincl  15858  recoscl  15859  retancl  15860  resinhcl  15874  rpcoshcl  15875  retanhcl  15877  tanhlt1  15878  tanhbnd  15879  efieq  15881  sinbnd  15898  cosbnd  15899  absefi  15914  dvdsaddre2b  16025  odd2np1  16059  bezoutlem1  16256  xrsdsreclb  20654  remulg  20821  resubdrg  20822  remetdval  23961  bl2ioo  23964  ioo2bl  23965  cnperf  23992  icccvx  24122  tcphcph  24410  shft2rab  24681  volsup2  24778  volcn  24779  c1lip1  25170  plyreres  25452  aalioulem3  25503  taylthlem2  25542  reeff1o  25615  reefgim  25618  sincosq1sgn  25664  sincosq2sgn  25665  sincosq3sgn  25666  sincosq4sgn  25667  sinq12gt0  25673  pige3ALT  25685  efif1olem4  25710  efifo  25712  relogrn  25726  logrnaddcl  25739  relogoprlem  25755  advlog  25818  advlogexp  25819  logtayl  25824  recxpcl  25839  rpcxpcl  25840  cxpge0  25847  cxpcom  25901  dvcxp1  25902  logreclem  25921  relogbreexp  25934  relogbcxp  25944  angpieqvd  25990  atanre  26044  basellem9  26247  gausslemma2dlem1a  26522  2sqnn0  26595  log2sumbnd  26701  brbtwn2  27282  colinearalglem4  27286  colinearalg  27287  crctcshwlkn0lem1  28184  nvsge0  29035  nmoub3i  29144  nmlnoubi  29167  isblo3i  29172  ipasslem3  29204  ipasslem9  29209  ipasslem11  29211  hmopm  30392  riesz1  30436  leopmuli  30504  leopmul  30505  leopmul2i  30506  leopnmid  30509  nmopleid  30510  cdj1i  30804  cdj3lem1  30805  cdj3i  30812  addltmulALT  30817  dpfrac1  31175  rexdiv  31209  xdivid  31211  xdiv0  31212  rmulccn  31887  sgnneg  32516  lediv2aALT  33644  nndivlub  34656  irrdiff  35506  cos2h  35777  tan2h  35778  poimir  35819  mblfinlem2  35824  mblfinlem4  35826  itg2addnclem  35837  itg2addnclem2  35838  dvasin  35870  areacirclem1  35874  areacirclem2  35875  areacirclem4  35877  areacirclem5  35878  areacirc  35879  lcmineqlem12  40055  dvrelog2b  40081  aks4d1p1p6  40088  2xp3dxp2ge1d  40169  resubeulem2  40366  renegneg  40401  renegid2  40403  sn-it0e0  40404  sn-negex12  40405  resubeqsub  40418  sn-mulid2  40424  sn-mul02  40429  areaquad  41054  reabssgn  41251  radcnvrat  41939  lhe4.4ex1a  41954  expgrowthi  41958  mulltgt0  42572  refsum2cnlem1  42587  infnsuprnmpt  42803  dstregt0  42827  suplesup  42885  infleinflem1  42916  infleinflem2  42917  ltdiv23neg  42941  rexabslelem  42965  supminfrnmpt  42992  supminfxr  43011  fmul01lt1lem1  43132  lptre2pt  43188  cnrefiisplem  43377  dvcosre  43460  itgsin0pilem1  43498  itgsinexplem1  43502  volioc  43520  volico  43531  stoweidlem7  43555  stoweidlem10  43558  stoweidlem19  43567  stoweidlem34  43582  stoweid  43611  dirker2re  43640  dirkerdenne0  43641  dirkerper  43644  dirkertrigeq  43649  dirkeritg  43650  fourierdlem39  43694  fourierdlem42  43697  fourierdlem47  43701  fourierdlem56  43710  fourierdlem57  43711  fourierdlem58  43712  fourierdlem60  43714  fourierdlem61  43715  fourierdlem73  43727  fourierdlem76  43730  fourierdlem77  43731  fourierdlem92  43746  fourierdlem97  43751  etransclem46  43828  volico2  44186  smflimlem4  44319  smfinflem  44361  2leaddle2  44801  ltsubsubaddltsub  44804  sqrtnegnre  44810  m1mod0mod1  44832  requad01  45084  requad1  45085  bgoldbtbndlem2  45269  flsubz  45874  rege1logbrege0  45915  nn0digval  45957  rrx2vlinest  46098  line2  46109  line2xlem  46110  line2x  46111  itscnhlc0yqe  46116  itsclc0yqsollem2  46120  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itsclc0xyqsolr  46126  itsclquadb  46133  reseccl  46466  recsccl  46467  recotcl  46468