Theorem recn 11196

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℂcc 11104  ℝcr 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  mulrid  11209  recnd  11239  pnfnre  11252  mnfnre  11254  mul02  11389  ltaddneg  11426  ltaddnegr  11427  renegcli  11518  resubcl  11521  negn0  11640  negf1o  11641  ltaddsub2  11686  leaddsub2  11688  leltadd  11695  ltaddpos  11701  ltaddpos2  11702  posdif  11704  lenegcon1  11715  lenegcon2  11716  addge01  11721  addge02  11722  leaddle0  11726  mullt0  11730  recex  11843  ltm1  12053  prodgt02  12059  ltmul2  12062  lemul1  12063  lemul2  12064  lemul1a  12065  lemul2a  12066  ltmulgt12  12072  lemulge12  12074  gt0div  12077  ge0div  12078  mulge0b  12081  mulle0b  12082  ltmuldiv2  12085  ltdivmul  12086  ledivmul  12087  ltdivmul2  12088  lt2mul2div  12089  ledivmul2  12090  lemuldiv2  12092  ltdiv2  12097  ltrec1  12098  lerec2  12099  ledivdiv  12100  lediv2  12101  ltdiv23  12102  lediv23  12103  lediv12a  12104  recp1lt1  12109  ledivp1  12113  negfi  12160  infm3lem  12169  supmul  12183  riotaneg  12190  negiso  12191  cju  12205  nnge1  12237  halfpos  12439  lt2halves  12444  addltmul  12445  avgle1  12449  avgle2  12450  avgle  12451  div4p1lem1div2  12464  nnrecl  12467  difgtsumgt  12522  elznn0  12570  elznn  12571  elz2  12573  nzadd  12607  zmulcl  12608  gtndiv  12636  zeo  12645  eqreznegel  12915  supminf  12916  rebtwnz  12928  irradd  12954  irrmul  12955  divlt1lt  13040  divle1le  13041  max0sub  13172  xnegneg  13190  rexsub  13209  xnegid  13214  xaddcom  13216  xaddrid  13217  xnegdi  13224  xaddass  13225  rexmul  13247  xmulasslem3  13262  xadddilem  13270  divelunit  13468  fzonmapblen  13675  ico01fl0  13781  flzadd  13788  ltdifltdiv  13796  dfceil2  13801  intfrac2  13820  fldiv2  13823  flpmodeq  13836  mod0  13838  negmod0  13840  modlt  13842  modfrac  13846  flmod  13847  intfrac  13848  modmulnn  13851  modvalp1  13852  modid  13858  modcyc  13868  modcyc2  13869  modadd1  13870  modaddabs  13871  muladdmodid  13873  negmod  13878  modadd2mod  13883  modmul1  13886  modmulmodr  13899  modaddmulmod  13900  moddi  13901  modsubdir  13902  modirr  13904  addmodlteq  13908  expgt1  14063  mulexpz  14065  sqgt0  14088  lt2sq  14095  le2sq  14096  sqge0  14098  expmordi  14129  leexp1a  14137  expubnd  14139  sumsqeq0  14140  sqlecan  14170  bernneq  14189  bernneq2  14190  expnbnd  14192  digit2  14196  digit1  14197  expnngt1  14201  swrdccatin2  14676  swrdccat3blem  14686  cshweqrep  14768  crre  15058  crim  15059  reim0  15062  mulre  15065  rere  15066  remul2  15074  rediv  15075  immul2  15081  imdiv  15082  cjre  15083  cjreim  15104  rennim  15183  resqrex  15194  resqreu  15196  resqrtcl  15197  resqrtthlem  15198  sqrtneglem  15210  sqrtneg  15211  absreimsq  15236  absreim  15237  absnid  15242  leabs  15243  absre  15245  absresq  15246  sqabs  15251  max0add  15254  absz  15255  absdiflt  15261  absdifle  15262  lenegsq  15264  abssuble0  15272  absmax  15273  rddif  15284  absrdbnd  15285  o1rlimmul  15560  caurcvg2  15621  reefcl  16027  efgt0  16043  reeftlcl  16048  resinval  16075  recosval  16076  resin4p  16078  recos4p  16079  resincl  16080  recoscl  16081  retancl  16082  resinhcl  16096  rpcoshcl  16097  retanhcl  16099  tanhlt1  16100  tanhbnd  16101  efieq  16103  sinbnd  16120  cosbnd  16121  absefi  16136  dvdsaddre2b  16247  odd2np1  16281  bezoutlem1  16478  xrsdsreclb  21276  remulg  21468  resubdrg  21469  remetdval  24627  bl2ioo  24630  ioo2bl  24631  cnperf  24658  icccvx  24797  tcphcph  25087  shft2rab  25359  volsup2  25456  volcn  25457  c1lip1  25852  plyreres  26137  aalioulem3  26188  taylthlem2  26227  reeff1o  26301  reefgim  26304  sincosq1sgn  26350  sincosq2sgn  26351  sincosq3sgn  26352  sincosq4sgn  26353  sinq12gt0  26359  pige3ALT  26371  efif1olem4  26396  efifo  26398  relogrn  26412  logrnaddcl  26425  relogoprlem  26441  advlog  26504  advlogexp  26505  logtayl  26510  recxpcl  26525  rpcxpcl  26526  cxpge0  26533  cxpcom  26589  dvcxp1  26590  logreclem  26610  relogbreexp  26623  relogbcxp  26633  angpieqvd  26679  atanre  26733  basellem9  26937  gausslemma2dlem1a  27214  2sqnn0  27287  log2sumbnd  27393  brbtwn2  28632  colinearalglem4  28636  colinearalg  28637  crctcshwlkn0lem1  29533  nvsge0  30386  nmoub3i  30495  nmlnoubi  30518  isblo3i  30523  ipasslem3  30555  ipasslem9  30560  ipasslem11  30562  hmopm  31743  riesz1  31787  leopmuli  31855  leopmul  31856  leopmul2i  31857  leopnmid  31860  nmopleid  31861  cdj1i  32155  cdj3lem1  32156  cdj3i  32163  addltmulALT  32168  dpfrac1  32525  rexdiv  32559  xdivid  32561  xdiv0  32562  sgnneg  34028  lediv2aALT  35151  gg-taylthlem2  35657  nndivlub  35833  irrdiff  36697  cos2h  36969  tan2h  36970  poimir  37011  mblfinlem2  37016  mblfinlem4  37018  itg2addnclem  37029  itg2addnclem2  37030  dvasin  37062  areacirclem1  37066  areacirclem2  37067  areacirclem4  37069  areacirclem5  37070  areacirc  37071  lcmineqlem12  41398  dvrelog2b  41424  aks4d1p1p6  41431  2xp3dxp2ge1d  41515  resubeulem2  41738  renegneg  41773  renegid2  41775  sn-it0e0  41777  sn-negex12  41778  resubeqsub  41791  sn-mullid  41797  sn-mul02  41802  areaquad  42454  reabssgn  42876  radcnvrat  43562  lhe4.4ex1a  43577  expgrowthi  43581  mulltgt0  44195  refsum2cnlem1  44210  infnsuprnmpt  44439  dstregt0  44476  suplesup  44534  infleinflem1  44565  infleinflem2  44566  ltdiv23neg  44589  rexabslelem  44613  supminfrnmpt  44640  supminfxr  44659  fmul01lt1lem1  44785  lptre2pt  44841  cnrefiisplem  45030  dvcosre  45113  itgsin0pilem1  45151  itgsinexplem1  45155  volioc  45173  volico  45184  stoweidlem7  45208  stoweidlem10  45211  stoweidlem19  45220  stoweidlem34  45235  stoweid  45264  dirker2re  45293  dirkerdenne0  45294  dirkerper  45297  dirkertrigeq  45302  dirkeritg  45303  fourierdlem39  45347  fourierdlem42  45350  fourierdlem47  45354  fourierdlem56  45363  fourierdlem57  45364  fourierdlem58  45365  fourierdlem60  45367  fourierdlem61  45368  fourierdlem73  45380  fourierdlem76  45383  fourierdlem77  45384  fourierdlem92  45399  fourierdlem97  45404  etransclem46  45481  volico2  45842  smflimlem4  45975  smfinflem  46018  et-sqrtnegnre  46074  2leaddle2  46491  ltsubsubaddltsub  46494  sqrtnegnre  46500  m1mod0mod1  46522  requad01  46774  requad1  46775  bgoldbtbndlem2  46959  flsubz  47391  rege1logbrege0  47432  nn0digval  47474  rrx2vlinest  47615  line2  47626  line2xlem  47627  line2x  47628  itscnhlc0yqe  47633  itsclc0yqsollem2  47637  itsclc0yqsol  47638  itscnhlc0xyqsol  47639  itschlc0xyqsol1  47640  itsclc0xyqsolr  47643  itsclquadb  47650  reseccl  47986  recsccl  47987  recotcl  47988