Theorem recn 11178

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℂcc 11086  ℝcr 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-ss 3924

This theorem is referenced by:  mulrid  11194  recnd  11225  pnfnre  11238  mnfnre  11240  mul02  11376  ltaddneg  11414  ltaddnegr  11415  renegcli  11507  resubcl  11510  negn0  11631  negf1o  11632  ltaddsub2  11677  leaddsub2  11679  leltadd  11686  ltaddpos  11692  ltaddpos2  11693  posdif  11695  lenegcon1  11706  lenegcon2  11707  addge01  11712  addge02  11713  leaddle0  11717  mullt0  11721  recex  11834  ltm1  12048  prodgt02  12054  ltmul2  12057  lemul1  12058  lemul2  12059  lemul1a  12060  lemul2a  12061  ltmulgt12  12066  lemulge12  12069  gt0div  12072  ge0div  12073  mulge0b  12076  mulle0b  12077  ltmuldiv2  12080  ltdivmul  12081  ledivmul  12082  ltdivmul2  12083  lt2mul2div  12084  ledivmul2  12085  lemuldiv2  12087  ltdiv2  12092  ltrec1  12093  lerec2  12094  ledivdiv  12095  lediv2  12096  ltdiv23  12097  lediv23  12098  lediv12a  12099  recp1lt1  12104  ledivp1  12108  negfi  12155  infm3lem  12164  supmul  12178  riotaneg  12185  negiso  12186  cju  12205  nnge1  12255  halfpos  12465  lt2halves  12470  addltmul  12471  avgle1  12475  avgle2  12476  avgle  12477  div4p1lem1div2  12490  nnrecl  12493  difgtsumgt  12548  elznn0  12597  elznn  12598  elz2  12600  nzadd  12633  zmulcl  12634  gtndiv  12664  zeo  12673  eqreznegel  12949  supminf  12950  rebtwnz  12962  irradd  12988  irrmul  12989  divlt1lt  13078  divle1le  13079  max0sub  13213  xnegneg  13231  rexsub  13250  xnegid  13255  xaddcom  13257  xaddrid  13258  xnegdi  13265  xaddass  13266  rexmul  13288  xmulasslem3  13303  xadddilem  13311  divelunit  13512  fzonmapblen  13728  ico01fl0  13843  flzadd  13850  ltdifltdiv  13858  dfceil2  13863  intfrac2  13882  fldiv2  13885  flpmodeq  13898  mod0  13900  negmod0  13902  modlt  13904  modfrac  13908  flmod  13909  intfrac  13910  modmulnn  13913  modvalp1  13914  modid  13920  modcyc  13930  modcyc2  13931  modadd1  13932  modaddabs  13935  muladdmodid  13937  muladdmod  13939  negmod  13943  modadd2mod  13948  modmul1  13951  modmulmodr  13964  modaddmulmod  13965  moddi  13966  modsubdir  13967  modirr  13969  addmodlteq  13973  expgt1  14127  mulexpz  14129  sqgt0  14153  lt2sq  14160  le2sq  14161  sqge0  14163  expmordi  14194  leexp1a  14202  expubnd  14205  sumsqeq0  14206  sqlecan  14236  bernneq  14256  bernneq2  14257  expnbnd  14259  digit2  14263  digit1  14264  expnngt1  14268  swrdccatin2  14756  swrdccat3blem  14766  cshweqrep  14848  sgnneg  15127  crre  15155  crim  15156  reim0  15159  mulre  15162  rere  15163  remul2  15171  rediv  15172  immul2  15178  imdiv  15179  cjre  15180  cjreim  15201  rennim  15280  resqrex  15291  resqreu  15293  resqrtcl  15294  resqrtthlem  15295  sqrtneglem  15307  sqrtneg  15308  absreimsq  15333  absreim  15334  absnid  15339  leabs  15340  absre  15342  absresq  15343  sqabs  15348  max0add  15351  absz  15352  absdiflt  15359  absdifle  15360  lenegsq  15362  abssuble0  15370  absmax  15371  rddif  15382  absrdbnd  15383  o1rlimmul  15660  caurcvg2  15719  reefcl  16131  efgt0  16149  reeftlcl  16154  resinval  16181  recosval  16182  resin4p  16184  recos4p  16185  resincl  16186  recoscl  16187  retancl  16188  resinhcl  16202  rpcoshcl  16203  retanhcl  16205  tanhlt1  16206  tanhbnd  16207  efieq  16209  sinbnd  16226  cosbnd  16227  absefi  16242  dvdsaddre2b  16355  odd2np1  16389  bezoutlem1  16587  xrsdsreclb  21524  remulg  21717  resubdrg  21718  remetdval  24907  bl2ioo  24910  ioo2bl  24911  cnperf  24939  icccvx  25070  tcphcph  25357  shft2rab  25628  volsup2  25725  volcn  25726  c1lip1  26117  plyreres  26405  aalioulem3  26456  taylthlem2  26495  reeff1o  26568  reefgim  26571  sincosq1sgn  26621  sincosq2sgn  26622  sincosq3sgn  26623  sincosq4sgn  26624  sinq12gt0  26630  pige3ALT  26643  efif1olem4  26668  efifo  26670  relogrn  26684  logrnaddcl  26697  relogoprlem  26714  advlog  26777  advlogexp  26778  logtayl  26783  recxpcl  26798  rpcxpcl  26799  cxpge0  26806  cxpcom  26862  dvcxp1  26863  logreclem  26885  relogbreexp  26898  relogbcxp  26908  angpieqvd  26954  atanre  27008  basellem9  27211  gausslemma2dlem1a  27487  2sqnn0  27560  log2sumbnd  27666  brbtwn2  29164  colinearalglem4  29168  colinearalg  29169  crctcshwlkn0lem1  30068  nvsge0  30925  nmoub3i  31034  nmlnoubi  31057  isblo3i  31062  ipasslem3  31094  ipasslem9  31099  ipasslem11  31101  hmopm  32282  riesz1  32326  leopmuli  32394  leopmul  32395  leopmul2i  32396  leopnmid  32399  nmopleid  32400  cdj1i  32694  cdj3lem1  32695  cdj3i  32702  addltmulALT  32707  dpfrac1  33124  rexdiv  33158  xdivid  33160  xdiv0  33161  lediv2aALT  36040  nndivlub  36831  irrdiff  37830  cos2h  38122  tan2h  38123  poimir  38164  mblfinlem2  38169  mblfinlem4  38171  itg2addnclem  38182  itg2addnclem2  38183  dvasin  38215  areacirclem1  38219  areacirclem2  38220  areacirclem4  38222  areacirclem5  38223  areacirc  38224  lcmineqlem12  42669  dvrelog2b  42695  aks4d1p1p6  42702  retire  42940  readvrec2  42982  readvrec  42983  resubeulem2  42997  renegneg  43033  renegid2  43035  sn-it0e0  43037  sn-negex12  43038  resubeqsub  43051  sn-mullid  43057  sn-mul02  43086  areaquad  43805  reabssgn  44224  radcnvrat  44888  lhe4.4ex1a  44903  expgrowthi  44907  mulltgt0  45600  refsum2cnlem1  45615  infnsuprnmpt  45823  dstregt0  45859  suplesup  45913  infleinflem1  45943  infleinflem2  45944  ltdiv23neg  45967  rexabslelem  45990  supminfrnmpt  46017  supminfxr  46036  fmul01lt1lem1  46158  lptre2pt  46212  cnrefiisplem  46401  dvcosre  46484  itgsin0pilem1  46522  itgsinexplem1  46526  volioc  46544  volico  46555  stoweidlem7  46579  stoweidlem10  46582  stoweidlem19  46591  stoweidlem34  46606  stoweid  46635  dirker2re  46664  dirkerdenne0  46665  dirkerper  46668  dirkertrigeq  46673  dirkeritg  46674  fourierdlem39  46718  fourierdlem42  46721  fourierdlem47  46725  fourierdlem56  46734  fourierdlem57  46735  fourierdlem58  46736  fourierdlem60  46738  fourierdlem61  46739  fourierdlem73  46751  fourierdlem76  46754  fourierdlem77  46755  fourierdlem92  46770  fourierdlem97  46775  etransclem46  46852  volico2  47213  smflimlem4  47346  smfinflem  47389  et-sqrtnegnre  47445  squeezedltsq  47462  2leaddle2  47890  ltsubsubaddltsub  47893  sqrtnegnre  47899  ceildivmod  47937  m1mod0mod1  47952  requad01  48241  requad1  48242  bgoldbtbndlem2  48426  flsubz  49153  rege1logbrege0  49189  nn0digval  49231  rrx2vlinest  49372  line2  49383  line2xlem  49384  line2x  49385  itscnhlc0yqe  49390  itsclc0yqsollem2  49394  itsclc0yqsol  49395  itscnhlc0xyqsol  49396  itschlc0xyqsol1  49397  itsclc0xyqsolr  49400  itsclquadb  49407  reseccl  50382  recsccl  50383  recotcl  50384