Theorem recn 11120

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

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

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 11087

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

This theorem is referenced by:  mulrid  11134  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  11987  prodgt02  11993  ltmul2  11996  lemul1  11997  lemul2  11998  lemul1a  11999  lemul2a  12000  ltmulgt12  12006  lemulge12  12009  gt0div  12012  ge0div  12013  mulge0b  12016  mulle0b  12017  ltmuldiv2  12020  ltdivmul  12021  ledivmul  12022  ltdivmul2  12023  lt2mul2div  12024  ledivmul2  12025  lemuldiv2  12027  ltdiv2  12032  ltrec1  12033  lerec2  12034  ledivdiv  12035  lediv2  12036  ltdiv23  12037  lediv23  12038  lediv12a  12039  recp1lt1  12044  ledivp1  12048  negfi  12095  infm3lem  12104  supmul  12118  riotaneg  12125  negiso  12126  cju  12145  nnge1  12177  halfpos  12375  lt2halves  12380  addltmul  12381  avgle1  12385  avgle2  12386  avgle  12387  div4p1lem1div2  12400  nnrecl  12403  difgtsumgt  12458  elznn0  12507  elznn  12508  elz2  12510  nzadd  12543  zmulcl  12544  gtndiv  12573  zeo  12582  eqreznegel  12851  supminf  12852  rebtwnz  12864  irradd  12890  irrmul  12891  divlt1lt  12980  divle1le  12981  max0sub  13115  xnegneg  13133  rexsub  13152  xnegid  13157  xaddcom  13159  xaddrid  13160  xnegdi  13167  xaddass  13168  rexmul  13190  xmulasslem3  13205  xadddilem  13213  divelunit  13414  fzonmapblen  13628  ico01fl0  13743  flzadd  13750  ltdifltdiv  13758  dfceil2  13763  intfrac2  13782  fldiv2  13785  flpmodeq  13798  mod0  13800  negmod0  13802  modlt  13804  modfrac  13808  flmod  13809  intfrac  13810  modmulnn  13813  modvalp1  13814  modid  13820  modcyc  13830  modcyc2  13831  modadd1  13832  modaddabs  13835  muladdmodid  13837  muladdmod  13839  negmod  13843  modadd2mod  13848  modmul1  13851  modmulmodr  13864  modaddmulmod  13865  moddi  13866  modsubdir  13867  modirr  13869  addmodlteq  13873  expgt1  14027  mulexpz  14029  sqgt0  14053  lt2sq  14060  le2sq  14061  sqge0  14063  expmordi  14094  leexp1a  14102  expubnd  14105  sumsqeq0  14106  sqlecan  14136  bernneq  14156  bernneq2  14157  expnbnd  14159  digit2  14163  digit1  14164  expnngt1  14168  swrdccatin2  14656  swrdccat3blem  14666  cshweqrep  14748  crre  15041  crim  15042  reim0  15045  mulre  15048  rere  15049  remul2  15057  rediv  15058  immul2  15064  imdiv  15065  cjre  15066  cjreim  15087  rennim  15166  resqrex  15177  resqreu  15179  resqrtcl  15180  resqrtthlem  15181  sqrtneglem  15193  sqrtneg  15194  absreimsq  15219  absreim  15220  absnid  15225  leabs  15226  absre  15228  absresq  15229  sqabs  15234  max0add  15237  absz  15238  absdiflt  15245  absdifle  15246  lenegsq  15248  abssuble0  15256  absmax  15257  rddif  15268  absrdbnd  15269  o1rlimmul  15546  caurcvg2  15605  reefcl  16014  efgt0  16032  reeftlcl  16037  resinval  16064  recosval  16065  resin4p  16067  recos4p  16068  resincl  16069  recoscl  16070  retancl  16071  resinhcl  16085  rpcoshcl  16086  retanhcl  16088  tanhlt1  16089  tanhbnd  16090  efieq  16092  sinbnd  16109  cosbnd  16110  absefi  16125  dvdsaddre2b  16238  odd2np1  16272  bezoutlem1  16470  xrsdsreclb  21372  remulg  21566  resubdrg  21567  remetdval  24737  bl2ioo  24740  ioo2bl  24741  cnperf  24769  icccvx  24908  tcphcph  25197  shft2rab  25469  volsup2  25566  volcn  25567  c1lip1  25962  plyreres  26250  aalioulem3  26302  taylthlem2  26342  taylthlem2OLD  26343  reeff1o  26417  reefgim  26420  sincosq1sgn  26467  sincosq2sgn  26468  sincosq3sgn  26469  sincosq4sgn  26470  sinq12gt0  26476  pige3ALT  26489  efif1olem4  26514  efifo  26516  relogrn  26530  logrnaddcl  26543  relogoprlem  26560  advlog  26623  advlogexp  26624  logtayl  26629  recxpcl  26644  rpcxpcl  26645  cxpge0  26652  cxpcom  26708  dvcxp1  26709  logreclem  26732  relogbreexp  26745  relogbcxp  26755  angpieqvd  26801  atanre  26855  basellem9  27059  gausslemma2dlem1a  27336  2sqnn0  27409  log2sumbnd  27515  brbtwn2  28961  colinearalglem4  28965  colinearalg  28966  crctcshwlkn0lem1  29866  nvsge0  30722  nmoub3i  30831  nmlnoubi  30854  isblo3i  30859  ipasslem3  30891  ipasslem9  30896  ipasslem11  30898  hmopm  32079  riesz1  32123  leopmuli  32191  leopmul  32192  leopmul2i  32193  leopnmid  32196  nmopleid  32197  cdj1i  32491  cdj3lem1  32492  cdj3i  32499  addltmulALT  32504  sgnneg  32895  dpfrac1  32954  rexdiv  32988  xdivid  32990  xdiv0  32991  lediv2aALT  35852  nndivlub  36633  irrdiff  37502  cos2h  37783  tan2h  37784  poimir  37825  mblfinlem2  37830  mblfinlem4  37832  itg2addnclem  37843  itg2addnclem2  37844  dvasin  37876  areacirclem1  37880  areacirclem2  37881  areacirclem4  37883  areacirclem5  37884  areacirc  37885  lcmineqlem12  42331  dvrelog2b  42357  aks4d1p1p6  42364  retire  42610  readvrec2  42652  readvrec  42653  resubeulem2  42667  renegneg  42703  renegid2  42705  sn-it0e0  42707  sn-negex12  42708  resubeqsub  42721  sn-mullid  42727  sn-mul02  42743  areaquad  43494  reabssgn  43913  radcnvrat  44591  lhe4.4ex1a  44606  expgrowthi  44610  mulltgt0  45303  refsum2cnlem1  45318  infnsuprnmpt  45530  dstregt0  45566  suplesup  45620  infleinflem1  45650  infleinflem2  45651  ltdiv23neg  45674  rexabslelem  45698  supminfrnmpt  45725  supminfxr  45744  fmul01lt1lem1  45866  lptre2pt  45920  cnrefiisplem  46109  dvcosre  46192  itgsin0pilem1  46230  itgsinexplem1  46234  volioc  46252  volico  46263  stoweidlem7  46287  stoweidlem10  46290  stoweidlem19  46299  stoweidlem34  46314  stoweid  46343  dirker2re  46372  dirkerdenne0  46373  dirkerper  46376  dirkertrigeq  46381  dirkeritg  46382  fourierdlem39  46426  fourierdlem42  46429  fourierdlem47  46433  fourierdlem56  46442  fourierdlem57  46443  fourierdlem58  46444  fourierdlem60  46446  fourierdlem61  46447  fourierdlem73  46459  fourierdlem76  46462  fourierdlem77  46463  fourierdlem92  46478  fourierdlem97  46483  etransclem46  46560  volico2  46921  smflimlem4  47054  smfinflem  47097  et-sqrtnegnre  47153  squeezedltsq  47168  2leaddle2  47580  ltsubsubaddltsub  47583  sqrtnegnre  47589  ceildivmod  47621  m1mod0mod1  47636  requad01  47903  requad1  47904  bgoldbtbndlem2  48088  flsubz  48804  rege1logbrege0  48840  nn0digval  48882  rrx2vlinest  49023  line2  49034  line2xlem  49035  line2x  49036  itscnhlc0yqe  49041  itsclc0yqsollem2  49045  itsclc0yqsol  49046  itscnhlc0xyqsol  49047  itschlc0xyqsol1  49048  itsclc0xyqsolr  49051  itsclquadb  49058  reseccl  50034  recsccl  50035  recotcl  50036