Theorem recn 11093

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11001  ℝcr 11002

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 1968  ax-7 2009  ax-8 2113  ax-resscn 11060

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3919

This theorem is referenced by:  mulrid  11107  recnd  11137  pnfnre  11150  mnfnre  11152  mul02  11288  ltaddneg  11326  ltaddnegr  11327  renegcli  11419  resubcl  11422  negn0  11543  negf1o  11544  ltaddsub2  11589  leaddsub2  11591  leltadd  11598  ltaddpos  11604  ltaddpos2  11605  posdif  11607  lenegcon1  11618  lenegcon2  11619  addge01  11624  addge02  11625  leaddle0  11629  mullt0  11633  recex  11746  ltm1  11960  prodgt02  11966  ltmul2  11969  lemul1  11970  lemul2  11971  lemul1a  11972  lemul2a  11973  ltmulgt12  11979  lemulge12  11982  gt0div  11985  ge0div  11986  mulge0b  11989  mulle0b  11990  ltmuldiv2  11993  ltdivmul  11994  ledivmul  11995  ltdivmul2  11996  lt2mul2div  11997  ledivmul2  11998  lemuldiv2  12000  ltdiv2  12005  ltrec1  12006  lerec2  12007  ledivdiv  12008  lediv2  12009  ltdiv23  12010  lediv23  12011  lediv12a  12012  recp1lt1  12017  ledivp1  12021  negfi  12068  infm3lem  12077  supmul  12091  riotaneg  12098  negiso  12099  cju  12118  nnge1  12150  halfpos  12348  lt2halves  12353  addltmul  12354  avgle1  12358  avgle2  12359  avgle  12360  div4p1lem1div2  12373  nnrecl  12376  difgtsumgt  12431  elznn0  12480  elznn  12481  elz2  12483  nzadd  12517  zmulcl  12518  gtndiv  12547  zeo  12556  eqreznegel  12829  supminf  12830  rebtwnz  12842  irradd  12868  irrmul  12869  divlt1lt  12958  divle1le  12959  max0sub  13092  xnegneg  13110  rexsub  13129  xnegid  13134  xaddcom  13136  xaddrid  13137  xnegdi  13144  xaddass  13145  rexmul  13167  xmulasslem3  13182  xadddilem  13190  divelunit  13391  fzonmapblen  13605  ico01fl0  13720  flzadd  13727  ltdifltdiv  13735  dfceil2  13740  intfrac2  13759  fldiv2  13762  flpmodeq  13775  mod0  13777  negmod0  13779  modlt  13781  modfrac  13785  flmod  13786  intfrac  13787  modmulnn  13790  modvalp1  13791  modid  13797  modcyc  13807  modcyc2  13808  modadd1  13809  modaddabs  13812  muladdmodid  13814  muladdmod  13816  negmod  13820  modadd2mod  13825  modmul1  13828  modmulmodr  13841  modaddmulmod  13842  moddi  13843  modsubdir  13844  modirr  13846  addmodlteq  13850  expgt1  14004  mulexpz  14006  sqgt0  14030  lt2sq  14037  le2sq  14038  sqge0  14040  expmordi  14071  leexp1a  14079  expubnd  14082  sumsqeq0  14083  sqlecan  14113  bernneq  14133  bernneq2  14134  expnbnd  14136  digit2  14140  digit1  14141  expnngt1  14145  swrdccatin2  14633  swrdccat3blem  14643  cshweqrep  14725  crre  15018  crim  15019  reim0  15022  mulre  15025  rere  15026  remul2  15034  rediv  15035  immul2  15041  imdiv  15042  cjre  15043  cjreim  15064  rennim  15143  resqrex  15154  resqreu  15156  resqrtcl  15157  resqrtthlem  15158  sqrtneglem  15170  sqrtneg  15171  absreimsq  15196  absreim  15197  absnid  15202  leabs  15203  absre  15205  absresq  15206  sqabs  15211  max0add  15214  absz  15215  absdiflt  15222  absdifle  15223  lenegsq  15225  abssuble0  15233  absmax  15234  rddif  15245  absrdbnd  15246  o1rlimmul  15523  caurcvg2  15582  reefcl  15991  efgt0  16009  reeftlcl  16014  resinval  16041  recosval  16042  resin4p  16044  recos4p  16045  resincl  16046  recoscl  16047  retancl  16048  resinhcl  16062  rpcoshcl  16063  retanhcl  16065  tanhlt1  16066  tanhbnd  16067  efieq  16069  sinbnd  16086  cosbnd  16087  absefi  16102  dvdsaddre2b  16215  odd2np1  16249  bezoutlem1  16447  xrsdsreclb  21348  remulg  21542  resubdrg  21543  remetdval  24702  bl2ioo  24705  ioo2bl  24706  cnperf  24734  icccvx  24873  tcphcph  25162  shft2rab  25434  volsup2  25531  volcn  25532  c1lip1  25927  plyreres  26215  aalioulem3  26267  taylthlem2  26307  taylthlem2OLD  26308  reeff1o  26382  reefgim  26385  sincosq1sgn  26432  sincosq2sgn  26433  sincosq3sgn  26434  sincosq4sgn  26435  sinq12gt0  26441  pige3ALT  26454  efif1olem4  26479  efifo  26481  relogrn  26495  logrnaddcl  26508  relogoprlem  26525  advlog  26588  advlogexp  26589  logtayl  26594  recxpcl  26609  rpcxpcl  26610  cxpge0  26617  cxpcom  26673  dvcxp1  26674  logreclem  26697  relogbreexp  26710  relogbcxp  26720  angpieqvd  26766  atanre  26820  basellem9  27024  gausslemma2dlem1a  27301  2sqnn0  27374  log2sumbnd  27480  brbtwn2  28881  colinearalglem4  28885  colinearalg  28886  crctcshwlkn0lem1  29786  nvsge0  30639  nmoub3i  30748  nmlnoubi  30771  isblo3i  30776  ipasslem3  30808  ipasslem9  30813  ipasslem11  30815  hmopm  31996  riesz1  32040  leopmuli  32108  leopmul  32109  leopmul2i  32110  leopnmid  32113  nmopleid  32114  cdj1i  32408  cdj3lem1  32409  cdj3i  32416  addltmulALT  32421  sgnneg  32811  dpfrac1  32867  rexdiv  32901  xdivid  32903  xdiv0  32904  lediv2aALT  35709  nndivlub  36491  irrdiff  37359  cos2h  37650  tan2h  37651  poimir  37692  mblfinlem2  37697  mblfinlem4  37699  itg2addnclem  37710  itg2addnclem2  37711  dvasin  37743  areacirclem1  37747  areacirclem2  37748  areacirclem4  37750  areacirclem5  37751  areacirc  37752  lcmineqlem12  42072  dvrelog2b  42098  aks4d1p1p6  42105  retire  42351  readvrec2  42393  readvrec  42394  resubeulem2  42408  renegneg  42444  renegid2  42446  sn-it0e0  42448  sn-negex12  42449  resubeqsub  42462  sn-mullid  42468  sn-mul02  42484  areaquad  43248  reabssgn  43668  radcnvrat  44346  lhe4.4ex1a  44361  expgrowthi  44365  mulltgt0  45058  refsum2cnlem1  45073  infnsuprnmpt  45286  dstregt0  45322  suplesup  45377  infleinflem1  45407  infleinflem2  45408  ltdiv23neg  45431  rexabslelem  45455  supminfrnmpt  45482  supminfxr  45501  fmul01lt1lem1  45623  lptre2pt  45677  cnrefiisplem  45866  dvcosre  45949  itgsin0pilem1  45987  itgsinexplem1  45991  volioc  46009  volico  46020  stoweidlem7  46044  stoweidlem10  46047  stoweidlem19  46056  stoweidlem34  46071  stoweid  46100  dirker2re  46129  dirkerdenne0  46130  dirkerper  46133  dirkertrigeq  46138  dirkeritg  46139  fourierdlem39  46183  fourierdlem42  46186  fourierdlem47  46190  fourierdlem56  46199  fourierdlem57  46200  fourierdlem58  46201  fourierdlem60  46203  fourierdlem61  46204  fourierdlem73  46216  fourierdlem76  46219  fourierdlem77  46220  fourierdlem92  46235  fourierdlem97  46240  etransclem46  46317  volico2  46678  smflimlem4  46811  smfinflem  46854  et-sqrtnegnre  46910  squeezedltsq  46916  2leaddle2  47328  ltsubsubaddltsub  47331  sqrtnegnre  47337  ceildivmod  47369  m1mod0mod1  47384  requad01  47651  requad1  47652  bgoldbtbndlem2  47836  flsubz  48553  rege1logbrege0  48589  nn0digval  48631  rrx2vlinest  48772  line2  48783  line2xlem  48784  line2x  48785  itscnhlc0yqe  48790  itsclc0yqsollem2  48794  itsclc0yqsol  48795  itscnhlc0xyqsol  48796  itschlc0xyqsol1  48797  itsclc0xyqsolr  48800  itsclquadb  48807  reseccl  49784  recsccl  49785  recotcl  49786