Theorem recn 11242

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℝcr 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979

This theorem is referenced by:  mulrid  11256  recnd  11286  pnfnre  11299  mnfnre  11301  mul02  11436  ltaddneg  11474  ltaddnegr  11475  renegcli  11567  resubcl  11570  negn0  11689  negf1o  11690  ltaddsub2  11735  leaddsub2  11737  leltadd  11744  ltaddpos  11750  ltaddpos2  11751  posdif  11753  lenegcon1  11764  lenegcon2  11765  addge01  11770  addge02  11771  leaddle0  11775  mullt0  11779  recex  11892  ltm1  12106  prodgt02  12112  ltmul2  12115  lemul1  12116  lemul2  12117  lemul1a  12118  lemul2a  12119  ltmulgt12  12125  lemulge12  12128  gt0div  12131  ge0div  12132  mulge0b  12135  mulle0b  12136  ltmuldiv2  12139  ltdivmul  12140  ledivmul  12141  ltdivmul2  12142  lt2mul2div  12143  ledivmul2  12144  lemuldiv2  12146  ltdiv2  12151  ltrec1  12152  lerec2  12153  ledivdiv  12154  lediv2  12155  ltdiv23  12156  lediv23  12157  lediv12a  12158  recp1lt1  12163  ledivp1  12167  negfi  12214  infm3lem  12223  supmul  12237  riotaneg  12244  negiso  12245  cju  12259  nnge1  12291  halfpos  12493  lt2halves  12498  addltmul  12499  avgle1  12503  avgle2  12504  avgle  12505  div4p1lem1div2  12518  nnrecl  12521  difgtsumgt  12576  elznn0  12625  elznn  12626  elz2  12628  nzadd  12662  zmulcl  12663  gtndiv  12692  zeo  12701  eqreznegel  12973  supminf  12974  rebtwnz  12986  irradd  13012  irrmul  13013  divlt1lt  13101  divle1le  13102  max0sub  13234  xnegneg  13252  rexsub  13271  xnegid  13276  xaddcom  13278  xaddrid  13279  xnegdi  13286  xaddass  13287  rexmul  13309  xmulasslem3  13324  xadddilem  13332  divelunit  13530  fzonmapblen  13744  ico01fl0  13855  flzadd  13862  ltdifltdiv  13870  dfceil2  13875  intfrac2  13894  fldiv2  13897  flpmodeq  13910  mod0  13912  negmod0  13914  modlt  13916  modfrac  13920  flmod  13921  intfrac  13922  modmulnn  13925  modvalp1  13926  modid  13932  modcyc  13942  modcyc2  13943  modadd1  13944  modaddabs  13945  muladdmodid  13947  muladdmod  13949  negmod  13953  modadd2mod  13958  modmul1  13961  modmulmodr  13974  modaddmulmod  13975  moddi  13976  modsubdir  13977  modirr  13979  addmodlteq  13983  expgt1  14137  mulexpz  14139  sqgt0  14162  lt2sq  14169  le2sq  14170  sqge0  14172  expmordi  14203  leexp1a  14211  expubnd  14213  sumsqeq0  14214  sqlecan  14244  bernneq  14264  bernneq2  14265  expnbnd  14267  digit2  14271  digit1  14272  expnngt1  14276  swrdccatin2  14763  swrdccat3blem  14773  cshweqrep  14855  crre  15149  crim  15150  reim0  15153  mulre  15156  rere  15157  remul2  15165  rediv  15166  immul2  15172  imdiv  15173  cjre  15174  cjreim  15195  rennim  15274  resqrex  15285  resqreu  15287  resqrtcl  15288  resqrtthlem  15289  sqrtneglem  15301  sqrtneg  15302  absreimsq  15327  absreim  15328  absnid  15333  leabs  15334  absre  15336  absresq  15337  sqabs  15342  max0add  15345  absz  15346  absdiflt  15352  absdifle  15353  lenegsq  15355  abssuble0  15363  absmax  15364  rddif  15375  absrdbnd  15376  o1rlimmul  15651  caurcvg2  15710  reefcl  16119  efgt0  16135  reeftlcl  16140  resinval  16167  recosval  16168  resin4p  16170  recos4p  16171  resincl  16172  recoscl  16173  retancl  16174  resinhcl  16188  rpcoshcl  16189  retanhcl  16191  tanhlt1  16192  tanhbnd  16193  efieq  16195  sinbnd  16212  cosbnd  16213  absefi  16228  dvdsaddre2b  16340  odd2np1  16374  bezoutlem1  16572  xrsdsreclb  21448  remulg  21642  resubdrg  21643  remetdval  24824  bl2ioo  24827  ioo2bl  24828  cnperf  24855  icccvx  24994  tcphcph  25284  shft2rab  25556  volsup2  25653  volcn  25654  c1lip1  26050  plyreres  26338  aalioulem3  26390  taylthlem2  26430  taylthlem2OLD  26431  reeff1o  26505  reefgim  26508  sincosq1sgn  26554  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  sinq12gt0  26563  pige3ALT  26576  efif1olem4  26601  efifo  26603  relogrn  26617  logrnaddcl  26630  relogoprlem  26647  advlog  26710  advlogexp  26711  logtayl  26716  recxpcl  26731  rpcxpcl  26732  cxpge0  26739  cxpcom  26795  dvcxp1  26796  logreclem  26819  relogbreexp  26832  relogbcxp  26842  angpieqvd  26888  atanre  26942  basellem9  27146  gausslemma2dlem1a  27423  2sqnn0  27496  log2sumbnd  27602  brbtwn2  28934  colinearalglem4  28938  colinearalg  28939  crctcshwlkn0lem1  29839  nvsge0  30692  nmoub3i  30801  nmlnoubi  30824  isblo3i  30829  ipasslem3  30861  ipasslem9  30866  ipasslem11  30868  hmopm  32049  riesz1  32093  leopmuli  32161  leopmul  32162  leopmul2i  32163  leopnmid  32166  nmopleid  32167  cdj1i  32461  cdj3lem1  32462  cdj3i  32469  addltmulALT  32474  dpfrac1  32858  rexdiv  32892  xdivid  32894  xdiv0  32895  sgnneg  34521  lediv2aALT  35661  nndivlub  36440  irrdiff  37308  cos2h  37597  tan2h  37598  poimir  37639  mblfinlem2  37644  mblfinlem4  37646  itg2addnclem  37657  itg2addnclem2  37658  dvasin  37690  areacirclem1  37694  areacirclem2  37695  areacirclem4  37697  areacirclem5  37698  areacirc  37699  lcmineqlem12  42021  dvrelog2b  42047  aks4d1p1p6  42054  2xp3dxp2ge1d  42222  retire  42332  readvrec2  42369  readvrec  42370  resubeulem2  42382  renegneg  42417  renegid2  42419  sn-it0e0  42421  sn-negex12  42422  resubeqsub  42435  sn-mullid  42441  sn-mul02  42446  areaquad  43204  reabssgn  43625  radcnvrat  44309  lhe4.4ex1a  44324  expgrowthi  44328  mulltgt0  44959  refsum2cnlem1  44974  infnsuprnmpt  45194  dstregt0  45231  suplesup  45288  infleinflem1  45319  infleinflem2  45320  ltdiv23neg  45343  rexabslelem  45367  supminfrnmpt  45394  supminfxr  45413  fmul01lt1lem1  45539  lptre2pt  45595  cnrefiisplem  45784  dvcosre  45867  itgsin0pilem1  45905  itgsinexplem1  45909  volioc  45927  volico  45938  stoweidlem7  45962  stoweidlem10  45965  stoweidlem19  45974  stoweidlem34  45989  stoweid  46018  dirker2re  46047  dirkerdenne0  46048  dirkerper  46051  dirkertrigeq  46056  dirkeritg  46057  fourierdlem39  46101  fourierdlem42  46104  fourierdlem47  46108  fourierdlem56  46117  fourierdlem57  46118  fourierdlem58  46119  fourierdlem60  46121  fourierdlem61  46122  fourierdlem73  46134  fourierdlem76  46137  fourierdlem77  46138  fourierdlem92  46153  fourierdlem97  46158  etransclem46  46235  volico2  46596  smflimlem4  46729  smfinflem  46772  et-sqrtnegnre  46828  2leaddle2  47247  ltsubsubaddltsub  47250  sqrtnegnre  47256  ceildivmod  47278  m1mod0mod1  47293  requad01  47545  requad1  47546  bgoldbtbndlem2  47730  flsubz  48367  rege1logbrege0  48407  nn0digval  48449  rrx2vlinest  48590  line2  48601  line2xlem  48602  line2x  48603  itscnhlc0yqe  48608  itsclc0yqsollem2  48612  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itsclc0xyqsolr  48618  itsclquadb  48625  reseccl  48983  recsccl  48984  recotcl  48985