Theorem recn 11200

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  ℝcr 11109

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 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  mulrid  11212  recnd  11242  pnfnre  11255  mnfnre  11257  mul02  11392  ltaddneg  11429  ltaddnegr  11430  renegcli  11521  resubcl  11524  negn0  11643  negf1o  11644  ltaddsub2  11689  leaddsub2  11691  leltadd  11698  ltaddpos  11704  ltaddpos2  11705  posdif  11707  lenegcon1  11718  lenegcon2  11719  addge01  11724  addge02  11725  leaddle0  11729  mullt0  11733  recex  11846  ltm1  12056  prodgt02  12062  ltmul2  12065  lemul1  12066  lemul2  12067  lemul1a  12068  lemul2a  12069  ltmulgt12  12075  lemulge12  12077  gt0div  12080  ge0div  12081  mulge0b  12084  mulle0b  12085  ltmuldiv2  12088  ltdivmul  12089  ledivmul  12090  ltdivmul2  12091  lt2mul2div  12092  ledivmul2  12093  lemuldiv2  12095  ltdiv2  12100  ltrec1  12101  lerec2  12102  ledivdiv  12103  lediv2  12104  ltdiv23  12105  lediv23  12106  lediv12a  12107  recp1lt1  12112  ledivp1  12116  negfi  12163  infm3lem  12172  supmul  12186  riotaneg  12193  negiso  12194  cju  12208  nnge1  12240  halfpos  12442  lt2halves  12447  addltmul  12448  avgle1  12452  avgle2  12453  avgle  12454  div4p1lem1div2  12467  nnrecl  12470  difgtsumgt  12525  elznn0  12573  elznn  12574  elz2  12576  nzadd  12610  zmulcl  12611  gtndiv  12639  zeo  12648  eqreznegel  12918  supminf  12919  rebtwnz  12931  irradd  12957  irrmul  12958  divlt1lt  13043  divle1le  13044  max0sub  13175  xnegneg  13193  rexsub  13212  xnegid  13217  xaddcom  13219  xaddrid  13220  xnegdi  13227  xaddass  13228  rexmul  13250  xmulasslem3  13265  xadddilem  13273  divelunit  13471  fzonmapblen  13678  ico01fl0  13784  flzadd  13791  ltdifltdiv  13799  dfceil2  13804  intfrac2  13823  fldiv2  13826  flpmodeq  13839  mod0  13841  negmod0  13843  modlt  13845  modfrac  13849  flmod  13850  intfrac  13851  modmulnn  13854  modvalp1  13855  modid  13861  modcyc  13871  modcyc2  13872  modadd1  13873  modaddabs  13874  muladdmodid  13876  negmod  13881  modadd2mod  13886  modmul1  13889  modmulmodr  13902  modaddmulmod  13903  moddi  13904  modsubdir  13905  modirr  13907  addmodlteq  13911  expgt1  14066  mulexpz  14068  sqgt0  14091  lt2sq  14098  le2sq  14099  sqge0  14101  expmordi  14132  leexp1a  14140  expubnd  14142  sumsqeq0  14143  sqlecan  14173  bernneq  14192  bernneq2  14193  expnbnd  14195  digit2  14199  digit1  14200  expnngt1  14204  swrdccatin2  14679  swrdccat3blem  14689  cshweqrep  14771  crre  15061  crim  15062  reim0  15065  mulre  15068  rere  15069  remul2  15077  rediv  15078  immul2  15084  imdiv  15085  cjre  15086  cjreim  15107  rennim  15186  resqrex  15197  resqreu  15199  resqrtcl  15200  resqrtthlem  15201  sqrtneglem  15213  sqrtneg  15214  absreimsq  15239  absreim  15240  absnid  15245  leabs  15246  absre  15248  absresq  15249  sqabs  15254  max0add  15257  absz  15258  absdiflt  15264  absdifle  15265  lenegsq  15267  abssuble0  15275  absmax  15276  rddif  15287  absrdbnd  15288  o1rlimmul  15563  caurcvg2  15624  reefcl  16030  efgt0  16046  reeftlcl  16051  resinval  16078  recosval  16079  resin4p  16081  recos4p  16082  resincl  16083  recoscl  16084  retancl  16085  resinhcl  16099  rpcoshcl  16100  retanhcl  16102  tanhlt1  16103  tanhbnd  16104  efieq  16106  sinbnd  16123  cosbnd  16124  absefi  16139  dvdsaddre2b  16250  odd2np1  16284  bezoutlem1  16481  xrsdsreclb  20992  remulg  21160  resubdrg  21161  remetdval  24305  bl2ioo  24308  ioo2bl  24309  cnperf  24336  icccvx  24466  tcphcph  24754  shft2rab  25025  volsup2  25122  volcn  25123  c1lip1  25514  plyreres  25796  aalioulem3  25847  taylthlem2  25886  reeff1o  25959  reefgim  25962  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  sinq12gt0  26017  pige3ALT  26029  efif1olem4  26054  efifo  26056  relogrn  26070  logrnaddcl  26083  relogoprlem  26099  advlog  26162  advlogexp  26163  logtayl  26168  recxpcl  26183  rpcxpcl  26184  cxpge0  26191  cxpcom  26247  dvcxp1  26248  logreclem  26267  relogbreexp  26280  relogbcxp  26290  angpieqvd  26336  atanre  26390  basellem9  26593  gausslemma2dlem1a  26868  2sqnn0  26941  log2sumbnd  27047  brbtwn2  28163  colinearalglem4  28167  colinearalg  28168  crctcshwlkn0lem1  29064  nvsge0  29917  nmoub3i  30026  nmlnoubi  30049  isblo3i  30054  ipasslem3  30086  ipasslem9  30091  ipasslem11  30093  hmopm  31274  riesz1  31318  leopmuli  31386  leopmul  31387  leopmul2i  31388  leopnmid  31391  nmopleid  31392  cdj1i  31686  cdj3lem1  31687  cdj3i  31694  addltmulALT  31699  dpfrac1  32058  rexdiv  32092  xdivid  32094  xdiv0  32095  rmulccn  32908  sgnneg  33539  lediv2aALT  34662  gg-rmulccn  35179  nndivlub  35343  irrdiff  36207  cos2h  36479  tan2h  36480  poimir  36521  mblfinlem2  36526  mblfinlem4  36528  itg2addnclem  36539  itg2addnclem2  36540  dvasin  36572  areacirclem1  36576  areacirclem2  36577  areacirclem4  36579  areacirclem5  36580  areacirc  36581  lcmineqlem12  40905  dvrelog2b  40931  aks4d1p1p6  40938  2xp3dxp2ge1d  41022  resubeulem2  41249  renegneg  41284  renegid2  41286  sn-it0e0  41288  sn-negex12  41289  resubeqsub  41302  sn-mullid  41308  sn-mul02  41313  areaquad  41965  reabssgn  42387  radcnvrat  43073  lhe4.4ex1a  43088  expgrowthi  43092  mulltgt0  43706  refsum2cnlem1  43721  infnsuprnmpt  43954  dstregt0  43991  suplesup  44049  infleinflem1  44080  infleinflem2  44081  ltdiv23neg  44104  rexabslelem  44128  supminfrnmpt  44155  supminfxr  44174  fmul01lt1lem1  44300  lptre2pt  44356  cnrefiisplem  44545  dvcosre  44628  itgsin0pilem1  44666  itgsinexplem1  44670  volioc  44688  volico  44699  stoweidlem7  44723  stoweidlem10  44726  stoweidlem19  44735  stoweidlem34  44750  stoweid  44779  dirker2re  44808  dirkerdenne0  44809  dirkerper  44812  dirkertrigeq  44817  dirkeritg  44818  fourierdlem39  44862  fourierdlem42  44865  fourierdlem47  44869  fourierdlem56  44878  fourierdlem57  44879  fourierdlem58  44880  fourierdlem60  44882  fourierdlem61  44883  fourierdlem73  44895  fourierdlem76  44898  fourierdlem77  44899  fourierdlem92  44914  fourierdlem97  44919  etransclem46  44996  volico2  45357  smflimlem4  45490  smfinflem  45533  et-sqrtnegnre  45589  2leaddle2  46006  ltsubsubaddltsub  46009  sqrtnegnre  46015  m1mod0mod1  46037  requad01  46289  requad1  46290  bgoldbtbndlem2  46474  flsubz  47203  rege1logbrege0  47244  nn0digval  47286  rrx2vlinest  47427  line2  47438  line2xlem  47439  line2x  47440  itscnhlc0yqe  47445  itsclc0yqsollem2  47449  itsclc0yqsol  47450  itscnhlc0xyqsol  47451  itschlc0xyqsol1  47452  itsclc0xyqsolr  47455  itsclquadb  47462  reseccl  47798  recsccl  47799  recotcl  47800