Theorem recn 11103

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11011  ℝcr 11012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-resscn 11070

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-ss 3915

This theorem is referenced by:  mulrid  11117  recnd  11147  pnfnre  11160  mnfnre  11162  mul02  11298  ltaddneg  11336  ltaddnegr  11337  renegcli  11429  resubcl  11432  negn0  11553  negf1o  11554  ltaddsub2  11599  leaddsub2  11601  leltadd  11608  ltaddpos  11614  ltaddpos2  11615  posdif  11617  lenegcon1  11628  lenegcon2  11629  addge01  11634  addge02  11635  leaddle0  11639  mullt0  11643  recex  11756  ltm1  11970  prodgt02  11976  ltmul2  11979  lemul1  11980  lemul2  11981  lemul1a  11982  lemul2a  11983  ltmulgt12  11989  lemulge12  11992  gt0div  11995  ge0div  11996  mulge0b  11999  mulle0b  12000  ltmuldiv2  12003  ltdivmul  12004  ledivmul  12005  ltdivmul2  12006  lt2mul2div  12007  ledivmul2  12008  lemuldiv2  12010  ltdiv2  12015  ltrec1  12016  lerec2  12017  ledivdiv  12018  lediv2  12019  ltdiv23  12020  lediv23  12021  lediv12a  12022  recp1lt1  12027  ledivp1  12031  negfi  12078  infm3lem  12087  supmul  12101  riotaneg  12108  negiso  12109  cju  12128  nnge1  12160  halfpos  12358  lt2halves  12363  addltmul  12364  avgle1  12368  avgle2  12369  avgle  12370  div4p1lem1div2  12383  nnrecl  12386  difgtsumgt  12441  elznn0  12490  elznn  12491  elz2  12493  nzadd  12526  zmulcl  12527  gtndiv  12556  zeo  12565  eqreznegel  12834  supminf  12835  rebtwnz  12847  irradd  12873  irrmul  12874  divlt1lt  12963  divle1le  12964  max0sub  13097  xnegneg  13115  rexsub  13134  xnegid  13139  xaddcom  13141  xaddrid  13142  xnegdi  13149  xaddass  13150  rexmul  13172  xmulasslem3  13187  xadddilem  13195  divelunit  13396  fzonmapblen  13610  ico01fl0  13725  flzadd  13732  ltdifltdiv  13740  dfceil2  13745  intfrac2  13764  fldiv2  13767  flpmodeq  13780  mod0  13782  negmod0  13784  modlt  13786  modfrac  13790  flmod  13791  intfrac  13792  modmulnn  13795  modvalp1  13796  modid  13802  modcyc  13812  modcyc2  13813  modadd1  13814  modaddabs  13817  muladdmodid  13819  muladdmod  13821  negmod  13825  modadd2mod  13830  modmul1  13833  modmulmodr  13846  modaddmulmod  13847  moddi  13848  modsubdir  13849  modirr  13851  addmodlteq  13855  expgt1  14009  mulexpz  14011  sqgt0  14035  lt2sq  14042  le2sq  14043  sqge0  14045  expmordi  14076  leexp1a  14084  expubnd  14087  sumsqeq0  14088  sqlecan  14118  bernneq  14138  bernneq2  14139  expnbnd  14141  digit2  14145  digit1  14146  expnngt1  14150  swrdccatin2  14638  swrdccat3blem  14648  cshweqrep  14730  crre  15023  crim  15024  reim0  15027  mulre  15030  rere  15031  remul2  15039  rediv  15040  immul2  15046  imdiv  15047  cjre  15048  cjreim  15069  rennim  15148  resqrex  15159  resqreu  15161  resqrtcl  15162  resqrtthlem  15163  sqrtneglem  15175  sqrtneg  15176  absreimsq  15201  absreim  15202  absnid  15207  leabs  15208  absre  15210  absresq  15211  sqabs  15216  max0add  15219  absz  15220  absdiflt  15227  absdifle  15228  lenegsq  15230  abssuble0  15238  absmax  15239  rddif  15250  absrdbnd  15251  o1rlimmul  15528  caurcvg2  15587  reefcl  15996  efgt0  16014  reeftlcl  16019  resinval  16046  recosval  16047  resin4p  16049  recos4p  16050  resincl  16051  recoscl  16052  retancl  16053  resinhcl  16067  rpcoshcl  16068  retanhcl  16070  tanhlt1  16071  tanhbnd  16072  efieq  16074  sinbnd  16091  cosbnd  16092  absefi  16107  dvdsaddre2b  16220  odd2np1  16254  bezoutlem1  16452  xrsdsreclb  21352  remulg  21546  resubdrg  21547  remetdval  24705  bl2ioo  24708  ioo2bl  24709  cnperf  24737  icccvx  24876  tcphcph  25165  shft2rab  25437  volsup2  25534  volcn  25535  c1lip1  25930  plyreres  26218  aalioulem3  26270  taylthlem2  26310  taylthlem2OLD  26311  reeff1o  26385  reefgim  26388  sincosq1sgn  26435  sincosq2sgn  26436  sincosq3sgn  26437  sincosq4sgn  26438  sinq12gt0  26444  pige3ALT  26457  efif1olem4  26482  efifo  26484  relogrn  26498  logrnaddcl  26511  relogoprlem  26528  advlog  26591  advlogexp  26592  logtayl  26597  recxpcl  26612  rpcxpcl  26613  cxpge0  26620  cxpcom  26676  dvcxp1  26677  logreclem  26700  relogbreexp  26713  relogbcxp  26723  angpieqvd  26769  atanre  26823  basellem9  27027  gausslemma2dlem1a  27304  2sqnn0  27377  log2sumbnd  27483  brbtwn2  28885  colinearalglem4  28889  colinearalg  28890  crctcshwlkn0lem1  29790  nvsge0  30646  nmoub3i  30755  nmlnoubi  30778  isblo3i  30783  ipasslem3  30815  ipasslem9  30820  ipasslem11  30822  hmopm  32003  riesz1  32047  leopmuli  32115  leopmul  32116  leopmul2i  32117  leopnmid  32120  nmopleid  32121  cdj1i  32415  cdj3lem1  32416  cdj3i  32423  addltmulALT  32428  sgnneg  32821  dpfrac1  32879  rexdiv  32913  xdivid  32915  xdiv0  32916  lediv2aALT  35742  nndivlub  36523  irrdiff  37391  cos2h  37671  tan2h  37672  poimir  37713  mblfinlem2  37718  mblfinlem4  37720  itg2addnclem  37731  itg2addnclem2  37732  dvasin  37764  areacirclem1  37768  areacirclem2  37769  areacirclem4  37771  areacirclem5  37772  areacirc  37773  lcmineqlem12  42153  dvrelog2b  42179  aks4d1p1p6  42186  retire  42437  readvrec2  42479  readvrec  42480  resubeulem2  42494  renegneg  42530  renegid2  42532  sn-it0e0  42534  sn-negex12  42535  resubeqsub  42548  sn-mullid  42554  sn-mul02  42570  areaquad  43333  reabssgn  43753  radcnvrat  44431  lhe4.4ex1a  44446  expgrowthi  44450  mulltgt0  45143  refsum2cnlem1  45158  infnsuprnmpt  45371  dstregt0  45407  suplesup  45462  infleinflem1  45492  infleinflem2  45493  ltdiv23neg  45516  rexabslelem  45540  supminfrnmpt  45567  supminfxr  45586  fmul01lt1lem1  45708  lptre2pt  45762  cnrefiisplem  45951  dvcosre  46034  itgsin0pilem1  46072  itgsinexplem1  46076  volioc  46094  volico  46105  stoweidlem7  46129  stoweidlem10  46132  stoweidlem19  46141  stoweidlem34  46156  stoweid  46185  dirker2re  46214  dirkerdenne0  46215  dirkerper  46218  dirkertrigeq  46223  dirkeritg  46224  fourierdlem39  46268  fourierdlem42  46271  fourierdlem47  46275  fourierdlem56  46284  fourierdlem57  46285  fourierdlem58  46286  fourierdlem60  46288  fourierdlem61  46289  fourierdlem73  46301  fourierdlem76  46304  fourierdlem77  46305  fourierdlem92  46320  fourierdlem97  46325  etransclem46  46402  volico2  46763  smflimlem4  46896  smfinflem  46939  et-sqrtnegnre  46995  squeezedltsq  47010  2leaddle2  47422  ltsubsubaddltsub  47425  sqrtnegnre  47431  ceildivmod  47463  m1mod0mod1  47478  requad01  47745  requad1  47746  bgoldbtbndlem2  47930  flsubz  48647  rege1logbrege0  48683  nn0digval  48725  rrx2vlinest  48866  line2  48877  line2xlem  48878  line2x  48879  itscnhlc0yqe  48884  itsclc0yqsollem2  48888  itsclc0yqsol  48889  itscnhlc0xyqsol  48890  itschlc0xyqsol1  48891  itsclc0xyqsolr  48894  itsclquadb  48901  reseccl  49878  recsccl  49879  recotcl  49880