Theorem recn 11218

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11126  ℝcr 11127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-resscn 11185

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837  df-ss 3919

This theorem is used by:  mulrid  11234  recnd  11265  pnfnre  11278  mnfnre  11280  mul02  11416  ltaddneg  11454  ltaddnegr  11455  renegcli  11547  resubcl  11550  negn0  11671  negf1o  11672  ltaddsub2  11717  leaddsub2  11719  leltadd  11726  ltaddpos  11732  ltaddpos2  11733  posdif  11735  lenegcon1  11746  lenegcon2  11747  addge01  11752  addge02  11753  leaddle0  11757  mullt0  11761  recex  11874  ltm1  12085  prodgt02  12091  ltmul2  12094  lemul1  12095  lemul2  12096  lemul1a  12097  lemul2a  12098  ltmulgt12  12103  lemulge12  12106  gt0div  12109  ge0div  12110  mulge0b  12113  mulle0b  12114  ltmuldiv2  12117  ltdivmul  12118  ledivmul  12119  ltdivmul2  12120  lt2mul2div  12121  ledivmul2  12122  lemuldiv2  12124  ltdiv2  12129  ltrec1  12130  lerec2  12131  ledivdiv  12132  lediv2  12133  ltdiv23  12134  lediv23  12135  lediv12a  12136  recp1lt1  12141  ledivp1  12145  negfi  12192  infm3lem  12201  supmul  12215  riotaneg  12222  negiso  12223  cju  12242  nnge1  12292  halfpos  12502  lt2halves  12507  addltmul  12508  avgle1  12512  avgle2  12513  avgle  12514  div4p1lem1div2  12527  nnrecl  12530  difgtsumgt  12585  elznn0  12634  elznn  12635  elz2  12637  nzadd  12670  zmulcl  12671  gtndiv  12702  zeo  12711  eqreznegel  12987  supminf  12988  rebtwnz  13000  irradd  13027  irrmul  13028  divlt1lt  13117  divle1le  13118  max0sub  13252  xnegneg  13270  rexsub  13289  xnegid  13294  xaddcom  13296  xaddrid  13297  xnegdi  13304  xaddass  13305  rexmul  13327  xmulasslem3  13342  xadddilem  13350  divelunit  13551  fzonmapblen  13768  ico01fl0  13884  flzadd  13891  ltdifltdiv  13899  dfceil2  13904  intfrac2  13923  fldiv2  13926  flpmodeq  13939  mod0  13941  negmod0  13943  modlt  13945  modfrac  13949  flmod  13950  intfrac  13951  modmulnn  13954  modvalp1  13955  modid  13961  modcyc  13971  modcyc2  13972  modadd1  13973  modaddabs  13976  muladdmodid  13978  muladdmod  13980  negmod  13984  modadd2mod  13989  modmul1  13992  modmulmodr  14005  modaddmulmod  14006  moddi  14007  modsubdir  14008  modirr  14010  addmodlteq  14014  expgt1  14168  mulexpz  14170  sqgt0  14194  lt2sq  14201  le2sq  14202  sqge0  14204  expmordi  14235  leexp1a  14243  expubnd  14246  sumsqeq0  14247  sqlecan  14277  bernneq  14297  bernneq2  14298  expnbnd  14300  digit2  14304  digit1  14305  expnngt1  14309  swrdccatin2  14802  swrdccat3blem  14812  cshweqrep  14896  sgnneg  15177  crre  15205  crim  15206  reim0  15209  mulre  15212  rere  15213  remul2  15221  rediv  15222  immul2  15228  imdiv  15229  cjre  15230  cjreim  15251  rennim  15330  resqrex  15341  resqreu  15343  resqrtcl  15344  resqrtthlem  15345  sqrtneglem  15357  sqrtneg  15358  absreimsq  15383  absreim  15384  absnid  15389  leabs  15390  absre  15392  absresq  15393  sqabs  15398  max0add  15401  absz  15402  absdiflt  15409  absdifle  15410  lenegsq  15412  abssuble0  15420  absmax  15421  rddif  15432  absrdbnd  15433  o1rlimmul  15710  caurcvg2  15769  reefcl  16179  efgt0  16197  reeftlcl  16202  resinval  16229  recosval  16230  resin4p  16232  recos4p  16233  resincl  16234  recoscl  16235  retancl  16236  resinhcl  16250  rpcoshcl  16251  retanhcl  16253  tanhlt1  16254  tanhbnd  16255  efieq  16257  sinbnd  16274  cosbnd  16275  absefi  16290  dvdsaddre2b  16403  odd2np1  16437  bezoutlem1  16635  xrsdsreclb  21633  remulg  21826  resubdrg  21827  remetdval  25021  bl2ioo  25024  ioo2bl  25025  cnperf  25053  icccvx  25184  tcphcph  25471  shft2rab  25742  volsup2  25839  volcn  25840  c1lip1  26231  plyreres  26520  aalioulem3  26577  taylthlem2  26617  reeff1o  26690  reefgim  26693  sincosq1sgn  26743  sincosq2sgn  26744  sincosq3sgn  26745  sincosq4sgn  26746  sinq12gt0  26752  pige3ALT  26765  efif1olem4  26790  efifo  26792  relogrn  26806  logrnaddcl  26819  relogoprlem  26836  advlog  26899  advlogexp  26900  logtayl  26905  recxpcl  26920  rpcxpcl  26921  cxpge0  26928  cxpcom  26984  dvcxp1  26985  logreclem  27007  relogbreexp  27020  relogbcxp  27030  angpieqvd  27076  atanre  27130  basellem9  27333  gausslemma2dlem1a  27609  2sqnn0  27682  log2sumbnd  27788  brbtwn2  29370  colinearalglem4  29374  colinearalg  29375  crctcshwlkn0lem1  30286  nvsge0  31153  nmoub3i  31262  nmlnoubi  31285  isblo3i  31290  ipasslem3  31322  ipasslem9  31327  ipasslem11  31329  hmopm  32510  riesz1  32554  leopmuli  32622  leopmul  32623  leopmul2i  32624  leopnmid  32627  nmopleid  32628  cdj1i  32922  cdj3lem1  32923  cdj3i  32930  addltmulALT  32935  dpfrac1  33345  rexdiv  33379  xdivid  33381  xdiv0  33382  lediv2aALT  36264  nndivlub  37085  irrdiff  38086  cos2h  38373  tan2h  38374  poimir  38410  mblfinlem2  38415  mblfinlem4  38417  itg2addnclem  38428  itg2addnclem2  38429  dvasin  38461  areacirclem1  38465  areacirclem2  38466  areacirclem4  38468  areacirclem5  38469  areacirc  38470  lcmineqlem12  42914  dvrelog2b  42940  aks4d1p1p6  42947  retire  43202  readvrec2  43244  readvrec  43245  resubeulem2  43259  renegneg  43295  renegid2  43297  sn-it0e0  43299  sn-negex12  43300  resubeqsub  43313  sn-mullid  43319  sn-mul02  43348  areaquad  44065  reabssgn  44484  radcnvrat  45146  lhe4.4ex1a  45161  expgrowthi  45165  mulltgt0  45864  refsum2cnlem1  45879  infnsuprnmpt  46087  dstregt0  46123  suplesup  46177  infleinflem1  46207  infleinflem2  46208  ltdiv23neg  46231  rexabslelem  46254  supminfrnmpt  46281  supminfxr  46300  fmul01lt1lem1  46422  lptre2pt  46476  cnrefiisplem  46665  dvcosre  46748  itgsin0pilem1  46786  itgsinexplem1  46790  volioc  46808  volico  46819  stoweidlem7  46843  stoweidlem10  46846  stoweidlem19  46855  stoweidlem34  46870  stoweid  46899  dirker2re  46928  dirkerdenne0  46929  dirkerper  46932  dirkertrigeq  46937  dirkeritg  46938  fourierdlem39  46982  fourierdlem42  46985  fourierdlem47  46989  fourierdlem56  46998  fourierdlem57  46999  fourierdlem58  47000  fourierdlem60  47002  fourierdlem61  47003  fourierdlem73  47015  fourierdlem76  47018  fourierdlem77  47019  fourierdlem92  47034  fourierdlem97  47039  etransclem46  47116  volico2  47477  smflimlem4  47610  smfinflem  47653  et-sqrtnegnre  47709  squeezedltsq  47738  2leaddle2  48194  ltsubsubaddltsub  48197  sqrtnegnre  48203  ceildivmod  48241  m1mod0mod1  48256  requad01  48545  requad1  48546  bgoldbtbndlem2  48730  flsubz  49460  rege1logbrege0  49496  nn0digval  49538  rrx2vlinest  49679  line2  49690  line2xlem  49691  line2x  49692  itscnhlc0yqe  49697  itsclc0yqsollem2  49701  itsclc0yqsol  49702  itscnhlc0xyqsol  49703  itschlc0xyqsol1  49704  itsclc0xyqsolr  49707  itsclquadb  49714  reseccl  50687  recsccl  50688  recotcl  50689