Theorem recn 10892

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℝcr 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  mulid1  10904  recnd  10934  pnfnre  10947  mnfnre  10949  mul02  11083  ltaddneg  11120  ltaddnegr  11121  renegcli  11212  resubcl  11215  negn0  11334  negf1o  11335  ltaddsub2  11380  leaddsub2  11382  leltadd  11389  ltaddpos  11395  ltaddpos2  11396  posdif  11398  lenegcon1  11409  lenegcon2  11410  addge01  11415  addge02  11416  leaddle0  11420  mullt0  11424  recex  11537  ltm1  11747  prodgt02  11753  ltmul2  11756  lemul1  11757  lemul2  11758  lemul1a  11759  lemul2a  11760  ltmulgt12  11766  lemulge12  11768  gt0div  11771  ge0div  11772  mulge0b  11775  mulle0b  11776  ltmuldiv2  11779  ltdivmul  11780  ledivmul  11781  ltdivmul2  11782  lt2mul2div  11783  ledivmul2  11784  lemuldiv2  11786  ltdiv2  11791  ltrec1  11792  lerec2  11793  ledivdiv  11794  lediv2  11795  ltdiv23  11796  lediv23  11797  lediv12a  11798  recp1lt1  11803  ledivp1  11807  negfi  11854  infm3lem  11863  supmul  11877  riotaneg  11884  negiso  11885  cju  11899  nnge1  11931  halfpos  12133  lt2halves  12138  addltmul  12139  avgle1  12143  avgle2  12144  avgle  12145  div4p1lem1div2  12158  nnrecl  12161  difgtsumgt  12216  elznn0  12264  elznn  12265  elz2  12267  nzadd  12298  zmulcl  12299  gtndiv  12327  zeo  12336  eqreznegel  12603  supminf  12604  rebtwnz  12616  irradd  12642  irrmul  12643  divlt1lt  12728  divle1le  12729  max0sub  12859  xnegneg  12877  rexsub  12896  xnegid  12901  xaddcom  12903  xaddid1  12904  xnegdi  12911  xaddass  12912  rexmul  12934  xmulasslem3  12949  xadddilem  12957  divelunit  13155  fzonmapblen  13361  ico01fl0  13467  flzadd  13474  ltdifltdiv  13482  dfceil2  13487  intfrac2  13506  fldiv2  13509  flpmodeq  13522  mod0  13524  negmod0  13526  modlt  13528  modfrac  13532  flmod  13533  intfrac  13534  modmulnn  13537  modvalp1  13538  modid  13544  modcyc  13554  modcyc2  13555  modadd1  13556  modaddabs  13557  muladdmodid  13559  negmod  13564  modadd2mod  13569  modmul1  13572  modmulmodr  13585  modaddmulmod  13586  moddi  13587  modsubdir  13588  modirr  13590  addmodlteq  13594  expgt1  13749  mulexpz  13751  sqgt0  13773  lt2sq  13780  le2sq  13781  sqge0  13783  expmordi  13813  leexp1a  13821  expubnd  13823  sumsqeq0  13824  sqlecan  13853  bernneq  13872  bernneq2  13873  expnbnd  13875  digit2  13879  digit1  13880  expnngt1  13884  swrdccatin2  14370  swrdccat3blem  14380  cshweqrep  14462  crre  14753  crim  14754  reim0  14757  mulre  14760  rere  14761  remul2  14769  rediv  14770  immul2  14776  imdiv  14777  cjre  14778  cjreim  14799  rennim  14878  resqrex  14890  resqreu  14892  resqrtcl  14893  resqrtthlem  14894  sqrtneglem  14906  sqrtneg  14907  absreimsq  14932  absreim  14933  absnid  14938  leabs  14939  absre  14941  absresq  14942  sqabs  14947  max0add  14950  absz  14951  absdiflt  14957  absdifle  14958  lenegsq  14960  abssuble0  14968  absmax  14969  rddif  14980  absrdbnd  14981  o1rlimmul  15256  caurcvg2  15317  reefcl  15724  efgt0  15740  reeftlcl  15745  resinval  15772  recosval  15773  resin4p  15775  recos4p  15776  resincl  15777  recoscl  15778  retancl  15779  resinhcl  15793  rpcoshcl  15794  retanhcl  15796  tanhlt1  15797  tanhbnd  15798  efieq  15800  sinbnd  15817  cosbnd  15818  absefi  15833  dvdsaddre2b  15944  odd2np1  15978  bezoutlem1  16175  xrsdsreclb  20557  remulg  20724  resubdrg  20725  remetdval  23858  bl2ioo  23861  ioo2bl  23862  cnperf  23889  icccvx  24019  tcphcph  24306  shft2rab  24577  volsup2  24674  volcn  24675  c1lip1  25066  plyreres  25348  aalioulem3  25399  taylthlem2  25438  reeff1o  25511  reefgim  25514  sincosq1sgn  25560  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  sinq12gt0  25569  pige3ALT  25581  efif1olem4  25606  efifo  25608  relogrn  25622  logrnaddcl  25635  relogoprlem  25651  advlog  25714  advlogexp  25715  logtayl  25720  recxpcl  25735  rpcxpcl  25736  cxpge0  25743  cxpcom  25797  dvcxp1  25798  logreclem  25817  relogbreexp  25830  relogbcxp  25840  angpieqvd  25886  atanre  25940  basellem9  26143  gausslemma2dlem1a  26418  2sqnn0  26491  log2sumbnd  26597  brbtwn2  27176  colinearalglem4  27180  colinearalg  27181  crctcshwlkn0lem1  28076  nvsge0  28927  nmoub3i  29036  nmlnoubi  29059  isblo3i  29064  ipasslem3  29096  ipasslem9  29101  ipasslem11  29103  hmopm  30284  riesz1  30328  leopmuli  30396  leopmul  30397  leopmul2i  30398  leopnmid  30401  nmopleid  30402  cdj1i  30696  cdj3lem1  30697  cdj3i  30704  addltmulALT  30709  dpfrac1  31068  rexdiv  31102  xdivid  31104  xdiv0  31105  rmulccn  31780  sgnneg  32407  lediv2aALT  33535  nndivlub  34574  irrdiff  35424  cos2h  35695  tan2h  35696  poimir  35737  mblfinlem2  35742  mblfinlem4  35744  itg2addnclem  35755  itg2addnclem2  35756  dvasin  35788  areacirclem1  35792  areacirclem2  35793  areacirclem4  35795  areacirclem5  35796  areacirc  35797  lcmineqlem12  39976  dvrelog2b  40002  aks4d1p1p6  40009  2xp3dxp2ge1d  40090  resubeulem2  40280  renegneg  40315  renegid2  40317  sn-it0e0  40318  sn-negex12  40319  resubeqsub  40332  sn-mulid2  40338  sn-mul02  40343  areaquad  40963  reabssgn  41133  radcnvrat  41821  lhe4.4ex1a  41836  expgrowthi  41840  mulltgt0  42454  refsum2cnlem1  42469  infnsuprnmpt  42685  dstregt0  42709  suplesup  42768  infleinflem1  42799  infleinflem2  42800  ltdiv23neg  42824  rexabslelem  42848  supminfrnmpt  42875  supminfxr  42894  fmul01lt1lem1  43015  lptre2pt  43071  cnrefiisplem  43260  dvcosre  43343  itgsin0pilem1  43381  itgsinexplem1  43385  volioc  43403  volico  43414  stoweidlem7  43438  stoweidlem10  43441  stoweidlem19  43450  stoweidlem34  43465  stoweid  43494  dirker2re  43523  dirkerdenne0  43524  dirkerper  43527  dirkertrigeq  43532  dirkeritg  43533  fourierdlem39  43577  fourierdlem42  43580  fourierdlem47  43584  fourierdlem56  43593  fourierdlem57  43594  fourierdlem58  43595  fourierdlem60  43597  fourierdlem61  43598  fourierdlem73  43610  fourierdlem76  43613  fourierdlem77  43614  fourierdlem92  43629  fourierdlem97  43634  etransclem46  43711  volico2  44069  smflimlem4  44196  smfinflem  44237  2leaddle2  44678  ltsubsubaddltsub  44681  sqrtnegnre  44687  m1mod0mod1  44709  requad01  44961  requad1  44962  bgoldbtbndlem2  45146  flsubz  45751  rege1logbrege0  45792  nn0digval  45834  rrx2vlinest  45975  line2  45986  line2xlem  45987  line2x  45988  itscnhlc0yqe  45993  itsclc0yqsollem2  45997  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itsclc0xyqsolr  46003  itsclquadb  46010  reseccl  46341  recsccl  46342  recotcl  46343