Theorem recn 11160

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 11068  ℝcr 11069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-resscn 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3921

This theorem is referenced by:  mulrid  11176  recnd  11207  pnfnre  11220  mnfnre  11222  mul02  11358  ltaddneg  11396  ltaddnegr  11397  renegcli  11489  resubcl  11492  negn0  11613  negf1o  11614  ltaddsub2  11659  leaddsub2  11661  leltadd  11668  ltaddpos  11674  ltaddpos2  11675  posdif  11677  lenegcon1  11688  lenegcon2  11689  addge01  11694  addge02  11695  leaddle0  11699  mullt0  11703  recex  11816  ltm1  12030  prodgt02  12036  ltmul2  12039  lemul1  12040  lemul2  12041  lemul1a  12042  lemul2a  12043  ltmulgt12  12049  lemulge12  12052  gt0div  12055  ge0div  12056  mulge0b  12059  mulle0b  12060  ltmuldiv2  12063  ltdivmul  12064  ledivmul  12065  ltdivmul2  12066  lt2mul2div  12067  ledivmul2  12068  lemuldiv2  12070  ltdiv2  12075  ltrec1  12076  lerec2  12077  ledivdiv  12078  lediv2  12079  ltdiv23  12080  lediv23  12081  lediv12a  12082  recp1lt1  12087  ledivp1  12091  negfi  12138  infm3lem  12147  supmul  12161  riotaneg  12168  negiso  12169  cju  12188  nnge1  12238  halfpos  12448  lt2halves  12453  addltmul  12454  avgle1  12458  avgle2  12459  avgle  12460  div4p1lem1div2  12473  nnrecl  12476  difgtsumgt  12531  elznn0  12580  elznn  12581  elz2  12583  nzadd  12616  zmulcl  12617  gtndiv  12647  zeo  12656  eqreznegel  12932  supminf  12933  rebtwnz  12945  irradd  12971  irrmul  12972  divlt1lt  13061  divle1le  13062  max0sub  13196  xnegneg  13214  rexsub  13233  xnegid  13238  xaddcom  13240  xaddrid  13241  xnegdi  13248  xaddass  13249  rexmul  13271  xmulasslem3  13286  xadddilem  13294  divelunit  13495  fzonmapblen  13711  ico01fl0  13826  flzadd  13833  ltdifltdiv  13841  dfceil2  13846  intfrac2  13865  fldiv2  13868  flpmodeq  13881  mod0  13883  negmod0  13885  modlt  13887  modfrac  13891  flmod  13892  intfrac  13893  modmulnn  13896  modvalp1  13897  modid  13903  modcyc  13913  modcyc2  13914  modadd1  13915  modaddabs  13918  muladdmodid  13920  muladdmod  13922  negmod  13926  modadd2mod  13931  modmul1  13934  modmulmodr  13947  modaddmulmod  13948  moddi  13949  modsubdir  13950  modirr  13952  addmodlteq  13956  expgt1  14110  mulexpz  14112  sqgt0  14136  lt2sq  14143  le2sq  14144  sqge0  14146  expmordi  14177  leexp1a  14185  expubnd  14188  sumsqeq0  14189  sqlecan  14219  bernneq  14239  bernneq2  14240  expnbnd  14242  digit2  14246  digit1  14247  expnngt1  14251  swrdccatin2  14739  swrdccat3blem  14749  cshweqrep  14831  crre  15124  crim  15125  reim0  15128  mulre  15131  rere  15132  remul2  15140  rediv  15141  immul2  15147  imdiv  15148  cjre  15149  cjreim  15170  rennim  15249  resqrex  15260  resqreu  15262  resqrtcl  15263  resqrtthlem  15264  sqrtneglem  15276  sqrtneg  15277  absreimsq  15302  absreim  15303  absnid  15308  leabs  15309  absre  15311  absresq  15312  sqabs  15317  max0add  15320  absz  15321  absdiflt  15328  absdifle  15329  lenegsq  15331  abssuble0  15339  absmax  15340  rddif  15351  absrdbnd  15352  o1rlimmul  15629  caurcvg2  15688  reefcl  16100  efgt0  16118  reeftlcl  16123  resinval  16150  recosval  16151  resin4p  16153  recos4p  16154  resincl  16155  recoscl  16156  retancl  16157  resinhcl  16171  rpcoshcl  16172  retanhcl  16174  tanhlt1  16175  tanhbnd  16176  efieq  16178  sinbnd  16195  cosbnd  16196  absefi  16211  dvdsaddre2b  16324  odd2np1  16358  bezoutlem1  16556  xrsdsreclb  21446  remulg  21639  resubdrg  21640  remetdval  24829  bl2ioo  24832  ioo2bl  24833  cnperf  24861  icccvx  24992  tcphcph  25279  shft2rab  25550  volsup2  25647  volcn  25648  c1lip1  26039  plyreres  26324  aalioulem3  26375  taylthlem2  26414  reeff1o  26487  reefgim  26490  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sinq12gt0  26549  pige3ALT  26562  efif1olem4  26587  efifo  26589  relogrn  26603  logrnaddcl  26616  relogoprlem  26633  advlog  26696  advlogexp  26697  logtayl  26702  recxpcl  26717  rpcxpcl  26718  cxpge0  26725  cxpcom  26781  dvcxp1  26782  logreclem  26804  relogbreexp  26817  relogbcxp  26827  angpieqvd  26873  atanre  26927  basellem9  27130  gausslemma2dlem1a  27406  2sqnn0  27479  log2sumbnd  27585  brbtwn2  29052  colinearalglem4  29056  colinearalg  29057  crctcshwlkn0lem1  29956  nvsge0  30813  nmoub3i  30922  nmlnoubi  30945  isblo3i  30950  ipasslem3  30982  ipasslem9  30987  ipasslem11  30989  hmopm  32170  riesz1  32214  leopmuli  32282  leopmul  32283  leopmul2i  32284  leopnmid  32287  nmopleid  32288  cdj1i  32582  cdj3lem1  32583  cdj3i  32590  addltmulALT  32595  sgnneg  32985  dpfrac1  33030  rexdiv  33064  xdivid  33066  xdiv0  33067  lediv2aALT  35991  nndivlub  36782  irrdiff  37782  cos2h  38074  tan2h  38075  poimir  38116  mblfinlem2  38121  mblfinlem4  38123  itg2addnclem  38134  itg2addnclem2  38135  dvasin  38167  areacirclem1  38171  areacirclem2  38172  areacirclem4  38174  areacirclem5  38175  areacirc  38176  lcmineqlem12  42621  dvrelog2b  42647  aks4d1p1p6  42654  retire  42892  readvrec2  42934  readvrec  42935  resubeulem2  42949  renegneg  42985  renegid2  42987  sn-it0e0  42989  sn-negex12  42990  resubeqsub  43003  sn-mullid  43009  sn-mul02  43038  areaquad  43757  reabssgn  44176  radcnvrat  44854  lhe4.4ex1a  44869  expgrowthi  44873  mulltgt0  45566  refsum2cnlem1  45581  infnsuprnmpt  45789  dstregt0  45825  suplesup  45879  infleinflem1  45909  infleinflem2  45910  ltdiv23neg  45933  rexabslelem  45956  supminfrnmpt  45983  supminfxr  46002  fmul01lt1lem1  46124  lptre2pt  46178  cnrefiisplem  46367  dvcosre  46450  itgsin0pilem1  46488  itgsinexplem1  46492  volioc  46510  volico  46521  stoweidlem7  46545  stoweidlem10  46548  stoweidlem19  46557  stoweidlem34  46572  stoweid  46601  dirker2re  46630  dirkerdenne0  46631  dirkerper  46634  dirkertrigeq  46639  dirkeritg  46640  fourierdlem39  46684  fourierdlem42  46687  fourierdlem47  46691  fourierdlem56  46700  fourierdlem57  46701  fourierdlem58  46702  fourierdlem60  46704  fourierdlem61  46705  fourierdlem73  46717  fourierdlem76  46720  fourierdlem77  46721  fourierdlem92  46736  fourierdlem97  46741  etransclem46  46818  volico2  47179  smflimlem4  47312  smfinflem  47355  et-sqrtnegnre  47411  squeezedltsq  47428  2leaddle2  47856  ltsubsubaddltsub  47859  sqrtnegnre  47865  ceildivmod  47903  m1mod0mod1  47918  requad01  48207  requad1  48208  bgoldbtbndlem2  48392  flsubz  49108  rege1logbrege0  49144  nn0digval  49186  rrx2vlinest  49327  line2  49338  line2xlem  49339  line2x  49340  itscnhlc0yqe  49345  itsclc0yqsollem2  49349  itsclc0yqsol  49350  itscnhlc0xyqsol  49351  itschlc0xyqsol1  49352  itsclc0xyqsolr  49355  itsclquadb  49362  reseccl  50338  recsccl  50339  recotcl  50340