Theorem recn 11119

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11027  ℝcr 11028

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 11086

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

This theorem is referenced by:  mulrid  11133  recnd  11164  pnfnre  11177  mnfnre  11179  mul02  11315  ltaddneg  11353  ltaddnegr  11354  renegcli  11446  resubcl  11449  negn0  11570  negf1o  11571  ltaddsub2  11616  leaddsub2  11618  leltadd  11625  ltaddpos  11631  ltaddpos2  11632  posdif  11634  lenegcon1  11645  lenegcon2  11646  addge01  11651  addge02  11652  leaddle0  11656  mullt0  11660  recex  11773  ltm1  11988  prodgt02  11994  ltmul2  11997  lemul1  11998  lemul2  11999  lemul1a  12000  lemul2a  12001  ltmulgt12  12007  lemulge12  12010  gt0div  12013  ge0div  12014  mulge0b  12017  mulle0b  12018  ltmuldiv2  12021  ltdivmul  12022  ledivmul  12023  ltdivmul2  12024  lt2mul2div  12025  ledivmul2  12026  lemuldiv2  12028  ltdiv2  12033  ltrec1  12034  lerec2  12035  ledivdiv  12036  lediv2  12037  ltdiv23  12038  lediv23  12039  lediv12a  12040  recp1lt1  12045  ledivp1  12049  negfi  12096  infm3lem  12105  supmul  12119  riotaneg  12126  negiso  12127  cju  12146  nnge1  12196  halfpos  12398  lt2halves  12403  addltmul  12404  avgle1  12408  avgle2  12409  avgle  12410  div4p1lem1div2  12423  nnrecl  12426  difgtsumgt  12481  elznn0  12530  elznn  12531  elz2  12533  nzadd  12566  zmulcl  12567  gtndiv  12597  zeo  12606  eqreznegel  12875  supminf  12876  rebtwnz  12888  irradd  12914  irrmul  12915  divlt1lt  13004  divle1le  13005  max0sub  13139  xnegneg  13157  rexsub  13176  xnegid  13181  xaddcom  13183  xaddrid  13184  xnegdi  13191  xaddass  13192  rexmul  13214  xmulasslem3  13229  xadddilem  13237  divelunit  13438  fzonmapblen  13654  ico01fl0  13769  flzadd  13776  ltdifltdiv  13784  dfceil2  13789  intfrac2  13808  fldiv2  13811  flpmodeq  13824  mod0  13826  negmod0  13828  modlt  13830  modfrac  13834  flmod  13835  intfrac  13836  modmulnn  13839  modvalp1  13840  modid  13846  modcyc  13856  modcyc2  13857  modadd1  13858  modaddabs  13861  muladdmodid  13863  muladdmod  13865  negmod  13869  modadd2mod  13874  modmul1  13877  modmulmodr  13890  modaddmulmod  13891  moddi  13892  modsubdir  13893  modirr  13895  addmodlteq  13899  expgt1  14053  mulexpz  14055  sqgt0  14079  lt2sq  14086  le2sq  14087  sqge0  14089  expmordi  14120  leexp1a  14128  expubnd  14131  sumsqeq0  14132  sqlecan  14162  bernneq  14182  bernneq2  14183  expnbnd  14185  digit2  14189  digit1  14190  expnngt1  14194  swrdccatin2  14682  swrdccat3blem  14692  cshweqrep  14774  crre  15067  crim  15068  reim0  15071  mulre  15074  rere  15075  remul2  15083  rediv  15084  immul2  15090  imdiv  15091  cjre  15092  cjreim  15113  rennim  15192  resqrex  15203  resqreu  15205  resqrtcl  15206  resqrtthlem  15207  sqrtneglem  15219  sqrtneg  15220  absreimsq  15245  absreim  15246  absnid  15251  leabs  15252  absre  15254  absresq  15255  sqabs  15260  max0add  15263  absz  15264  absdiflt  15271  absdifle  15272  lenegsq  15274  abssuble0  15282  absmax  15283  rddif  15294  absrdbnd  15295  o1rlimmul  15572  caurcvg2  15631  reefcl  16043  efgt0  16061  reeftlcl  16066  resinval  16093  recosval  16094  resin4p  16096  recos4p  16097  resincl  16098  recoscl  16099  retancl  16100  resinhcl  16114  rpcoshcl  16115  retanhcl  16117  tanhlt1  16118  tanhbnd  16119  efieq  16121  sinbnd  16138  cosbnd  16139  absefi  16154  dvdsaddre2b  16267  odd2np1  16301  bezoutlem1  16499  xrsdsreclb  21403  remulg  21597  resubdrg  21598  remetdval  24764  bl2ioo  24767  ioo2bl  24768  cnperf  24796  icccvx  24927  tcphcph  25214  shft2rab  25485  volsup2  25582  volcn  25583  c1lip1  25974  plyreres  26259  aalioulem3  26311  taylthlem2  26351  taylthlem2OLD  26352  reeff1o  26425  reefgim  26428  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12gt0  26484  pige3ALT  26497  efif1olem4  26522  efifo  26524  relogrn  26538  logrnaddcl  26551  relogoprlem  26568  advlog  26631  advlogexp  26632  logtayl  26637  recxpcl  26652  rpcxpcl  26653  cxpge0  26660  cxpcom  26716  dvcxp1  26717  logreclem  26739  relogbreexp  26752  relogbcxp  26762  angpieqvd  26808  atanre  26862  basellem9  27066  gausslemma2dlem1a  27342  2sqnn0  27415  log2sumbnd  27521  brbtwn2  28988  colinearalglem4  28992  colinearalg  28993  crctcshwlkn0lem1  29893  nvsge0  30750  nmoub3i  30859  nmlnoubi  30882  isblo3i  30887  ipasslem3  30919  ipasslem9  30924  ipasslem11  30926  hmopm  32107  riesz1  32151  leopmuli  32219  leopmul  32220  leopmul2i  32221  leopnmid  32224  nmopleid  32225  cdj1i  32519  cdj3lem1  32520  cdj3i  32527  addltmulALT  32532  sgnneg  32921  dpfrac1  32966  rexdiv  33000  xdivid  33002  xdiv0  33003  lediv2aALT  35875  nndivlub  36656  irrdiff  37656  cos2h  37946  tan2h  37947  poimir  37988  mblfinlem2  37993  mblfinlem4  37995  itg2addnclem  38006  itg2addnclem2  38007  dvasin  38039  areacirclem1  38043  areacirclem2  38044  areacirclem4  38046  areacirclem5  38047  areacirc  38048  lcmineqlem12  42493  dvrelog2b  42519  aks4d1p1p6  42526  retire  42765  readvrec2  42807  readvrec  42808  resubeulem2  42822  renegneg  42858  renegid2  42860  sn-it0e0  42862  sn-negex12  42863  resubeqsub  42876  sn-mullid  42882  sn-mul02  42911  areaquad  43662  reabssgn  44081  radcnvrat  44759  lhe4.4ex1a  44774  expgrowthi  44778  mulltgt0  45471  refsum2cnlem1  45486  infnsuprnmpt  45697  dstregt0  45733  suplesup  45787  infleinflem1  45817  infleinflem2  45818  ltdiv23neg  45841  rexabslelem  45864  supminfrnmpt  45891  supminfxr  45910  fmul01lt1lem1  46032  lptre2pt  46086  cnrefiisplem  46275  dvcosre  46358  itgsin0pilem1  46396  itgsinexplem1  46400  volioc  46418  volico  46429  stoweidlem7  46453  stoweidlem10  46456  stoweidlem19  46465  stoweidlem34  46480  stoweid  46509  dirker2re  46538  dirkerdenne0  46539  dirkerper  46542  dirkertrigeq  46547  dirkeritg  46548  fourierdlem39  46592  fourierdlem42  46595  fourierdlem47  46599  fourierdlem56  46608  fourierdlem57  46609  fourierdlem58  46610  fourierdlem60  46612  fourierdlem61  46613  fourierdlem73  46625  fourierdlem76  46628  fourierdlem77  46629  fourierdlem92  46644  fourierdlem97  46649  etransclem46  46726  volico2  47087  smflimlem4  47220  smfinflem  47263  et-sqrtnegnre  47319  squeezedltsq  47334  2leaddle2  47758  ltsubsubaddltsub  47761  sqrtnegnre  47767  ceildivmod  47805  m1mod0mod1  47820  requad01  48109  requad1  48110  bgoldbtbndlem2  48294  flsubz  49010  rege1logbrege0  49046  nn0digval  49088  rrx2vlinest  49229  line2  49240  line2xlem  49241  line2x  49242  itscnhlc0yqe  49247  itsclc0yqsollem2  49251  itsclc0yqsol  49252  itscnhlc0xyqsol  49253  itschlc0xyqsol1  49254  itsclc0xyqsolr  49257  itsclquadb  49264  reseccl  50240  recsccl  50241  recotcl  50242