Theorem recn 11128

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℝcr 11037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ss 3906

This theorem is referenced by:  mulrid  11142  recnd  11173  pnfnre  11186  mnfnre  11188  mul02  11324  ltaddneg  11362  ltaddnegr  11363  renegcli  11455  resubcl  11458  negn0  11579  negf1o  11580  ltaddsub2  11625  leaddsub2  11627  leltadd  11634  ltaddpos  11640  ltaddpos2  11641  posdif  11643  lenegcon1  11654  lenegcon2  11655  addge01  11660  addge02  11661  leaddle0  11665  mullt0  11669  recex  11782  ltm1  11997  prodgt02  12003  ltmul2  12006  lemul1  12007  lemul2  12008  lemul1a  12009  lemul2a  12010  ltmulgt12  12016  lemulge12  12019  gt0div  12022  ge0div  12023  mulge0b  12026  mulle0b  12027  ltmuldiv2  12030  ltdivmul  12031  ledivmul  12032  ltdivmul2  12033  lt2mul2div  12034  ledivmul2  12035  lemuldiv2  12037  ltdiv2  12042  ltrec1  12043  lerec2  12044  ledivdiv  12045  lediv2  12046  ltdiv23  12047  lediv23  12048  lediv12a  12049  recp1lt1  12054  ledivp1  12058  negfi  12105  infm3lem  12114  supmul  12128  riotaneg  12135  negiso  12136  cju  12155  nnge1  12205  halfpos  12407  lt2halves  12412  addltmul  12413  avgle1  12417  avgle2  12418  avgle  12419  div4p1lem1div2  12432  nnrecl  12435  difgtsumgt  12490  elznn0  12539  elznn  12540  elz2  12542  nzadd  12575  zmulcl  12576  gtndiv  12606  zeo  12615  eqreznegel  12884  supminf  12885  rebtwnz  12897  irradd  12923  irrmul  12924  divlt1lt  13013  divle1le  13014  max0sub  13148  xnegneg  13166  rexsub  13185  xnegid  13190  xaddcom  13192  xaddrid  13193  xnegdi  13200  xaddass  13201  rexmul  13223  xmulasslem3  13238  xadddilem  13246  divelunit  13447  fzonmapblen  13663  ico01fl0  13778  flzadd  13785  ltdifltdiv  13793  dfceil2  13798  intfrac2  13817  fldiv2  13820  flpmodeq  13833  mod0  13835  negmod0  13837  modlt  13839  modfrac  13843  flmod  13844  intfrac  13845  modmulnn  13848  modvalp1  13849  modid  13855  modcyc  13865  modcyc2  13866  modadd1  13867  modaddabs  13870  muladdmodid  13872  muladdmod  13874  negmod  13878  modadd2mod  13883  modmul1  13886  modmulmodr  13899  modaddmulmod  13900  moddi  13901  modsubdir  13902  modirr  13904  addmodlteq  13908  expgt1  14062  mulexpz  14064  sqgt0  14088  lt2sq  14095  le2sq  14096  sqge0  14098  expmordi  14129  leexp1a  14137  expubnd  14140  sumsqeq0  14141  sqlecan  14171  bernneq  14191  bernneq2  14192  expnbnd  14194  digit2  14198  digit1  14199  expnngt1  14203  swrdccatin2  14691  swrdccat3blem  14701  cshweqrep  14783  crre  15076  crim  15077  reim0  15080  mulre  15083  rere  15084  remul2  15092  rediv  15093  immul2  15099  imdiv  15100  cjre  15101  cjreim  15122  rennim  15201  resqrex  15212  resqreu  15214  resqrtcl  15215  resqrtthlem  15216  sqrtneglem  15228  sqrtneg  15229  absreimsq  15254  absreim  15255  absnid  15260  leabs  15261  absre  15263  absresq  15264  sqabs  15269  max0add  15272  absz  15273  absdiflt  15280  absdifle  15281  lenegsq  15283  abssuble0  15291  absmax  15292  rddif  15303  absrdbnd  15304  o1rlimmul  15581  caurcvg2  15640  reefcl  16052  efgt0  16070  reeftlcl  16075  resinval  16102  recosval  16103  resin4p  16105  recos4p  16106  resincl  16107  recoscl  16108  retancl  16109  resinhcl  16123  rpcoshcl  16124  retanhcl  16126  tanhlt1  16127  tanhbnd  16128  efieq  16130  sinbnd  16147  cosbnd  16148  absefi  16163  dvdsaddre2b  16276  odd2np1  16310  bezoutlem1  16508  xrsdsreclb  21394  remulg  21587  resubdrg  21588  remetdval  24754  bl2ioo  24757  ioo2bl  24758  cnperf  24786  icccvx  24917  tcphcph  25204  shft2rab  25475  volsup2  25572  volcn  25573  c1lip1  25964  plyreres  26249  aalioulem3  26300  taylthlem2  26339  reeff1o  26412  reefgim  26415  sincosq1sgn  26462  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  sinq12gt0  26471  pige3ALT  26484  efif1olem4  26509  efifo  26511  relogrn  26525  logrnaddcl  26538  relogoprlem  26555  advlog  26618  advlogexp  26619  logtayl  26624  recxpcl  26639  rpcxpcl  26640  cxpge0  26647  cxpcom  26703  dvcxp1  26704  logreclem  26726  relogbreexp  26739  relogbcxp  26749  angpieqvd  26795  atanre  26849  basellem9  27052  gausslemma2dlem1a  27328  2sqnn0  27401  log2sumbnd  27507  brbtwn2  28974  colinearalglem4  28978  colinearalg  28979  crctcshwlkn0lem1  29878  nvsge0  30735  nmoub3i  30844  nmlnoubi  30867  isblo3i  30872  ipasslem3  30904  ipasslem9  30909  ipasslem11  30911  hmopm  32092  riesz1  32136  leopmuli  32204  leopmul  32205  leopmul2i  32206  leopnmid  32209  nmopleid  32210  cdj1i  32504  cdj3lem1  32505  cdj3i  32512  addltmulALT  32517  sgnneg  32906  dpfrac1  32951  rexdiv  32985  xdivid  32987  xdiv0  32988  lediv2aALT  35859  nndivlub  36640  irrdiff  37640  cos2h  37932  tan2h  37933  poimir  37974  mblfinlem2  37979  mblfinlem4  37981  itg2addnclem  37992  itg2addnclem2  37993  dvasin  38025  areacirclem1  38029  areacirclem2  38030  areacirclem4  38032  areacirclem5  38033  areacirc  38034  lcmineqlem12  42479  dvrelog2b  42505  aks4d1p1p6  42512  retire  42751  readvrec2  42793  readvrec  42794  resubeulem2  42808  renegneg  42844  renegid2  42846  sn-it0e0  42848  sn-negex12  42849  resubeqsub  42862  sn-mullid  42868  sn-mul02  42897  areaquad  43644  reabssgn  44063  radcnvrat  44741  lhe4.4ex1a  44756  expgrowthi  44760  mulltgt0  45453  refsum2cnlem1  45468  infnsuprnmpt  45679  dstregt0  45715  suplesup  45769  infleinflem1  45799  infleinflem2  45800  ltdiv23neg  45823  rexabslelem  45846  supminfrnmpt  45873  supminfxr  45892  fmul01lt1lem1  46014  lptre2pt  46068  cnrefiisplem  46257  dvcosre  46340  itgsin0pilem1  46378  itgsinexplem1  46382  volioc  46400  volico  46411  stoweidlem7  46435  stoweidlem10  46438  stoweidlem19  46447  stoweidlem34  46462  stoweid  46491  dirker2re  46520  dirkerdenne0  46521  dirkerper  46524  dirkertrigeq  46529  dirkeritg  46530  fourierdlem39  46574  fourierdlem42  46577  fourierdlem47  46581  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem60  46594  fourierdlem61  46595  fourierdlem73  46607  fourierdlem76  46610  fourierdlem77  46611  fourierdlem92  46626  fourierdlem97  46631  etransclem46  46708  volico2  47069  smflimlem4  47202  smfinflem  47245  et-sqrtnegnre  47301  squeezedltsq  47318  2leaddle2  47746  ltsubsubaddltsub  47749  sqrtnegnre  47755  ceildivmod  47793  m1mod0mod1  47808  requad01  48097  requad1  48098  bgoldbtbndlem2  48282  flsubz  48998  rege1logbrege0  49034  nn0digval  49076  rrx2vlinest  49217  line2  49228  line2xlem  49229  line2x  49230  itscnhlc0yqe  49235  itsclc0yqsollem2  49239  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  itsclc0xyqsolr  49245  itsclquadb  49252  reseccl  50228  recsccl  50229  recotcl  50230