Theorem recn 11317

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11225  ℝcr 11226

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-resscn 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901

This theorem is used by:  mulrid  11333  recnd  11364  pnfnre  11377  mnfnre  11379  mul02  11515  ltaddneg  11553  ltaddnegr  11554  renegcli  11646  resubcl  11649  negn0  11772  negf1o  11773  ltaddsub2  11818  leaddsub2  11820  leltadd  11827  ltaddpos  11833  ltaddpos2  11834  posdif  11836  lenegcon1  11847  lenegcon2  11848  addge01  11853  addge02  11854  leaddle0  11858  mullt0  11862  recex  11975  ltm1  12186  prodgt02  12192  ltmul2  12195  lemul1  12196  lemul2  12197  lemul1a  12198  lemul2a  12199  ltmulgt12  12204  lemulge12  12207  gt0div  12210  ge0div  12211  mulge0b  12214  mulle0b  12215  ltmuldiv2  12218  ltdivmul  12219  ledivmul  12220  ltdivmul2  12221  lt2mul2div  12222  ledivmul2  12223  lemuldiv2  12225  ltdiv2  12230  ltrec1  12231  lerec2  12232  ledivdiv  12233  lediv2  12234  ltdiv23  12235  lediv23  12236  lediv12a  12237  recp1lt1  12242  ledivp1  12246  negfi  12293  infm3lem  12302  supmul  12316  riotaneg  12323  negiso  12324  cju  12343  nnge1  12393  halfpos  12603  lt2halves  12608  addltmul  12609  avgle1  12613  avgle2  12614  avgle  12615  div4p1lem1div2  12628  nnrecl  12631  difgtsumgt  12686  elznn0  12735  elznn  12736  elz2  12738  nzadd  12771  zmulcl  12772  gtndiv  12803  zeo  12812  eqreznegel  13088  supminf  13089  rebtwnz  13101  irradd  13128  irrmul  13129  divlt1lt  13218  divle1le  13219  max0sub  13353  xnegneg  13371  rexsub  13390  xnegid  13395  xaddcom  13397  xaddrid  13398  xnegdi  13405  xaddass  13406  rexmul  13428  xmulasslem3  13443  xadddilem  13451  divelunit  13652  fzonmapblen  13870  ico01fl0  13986  flzadd  13993  ltdifltdiv  14001  dfceil2  14006  intfrac2  14025  fldiv2  14028  flpmodeq  14041  mod0  14043  negmod0  14045  modlt  14047  modfrac  14051  flmod  14052  intfrac  14053  modmulnn  14056  modvalp1  14057  modid  14063  modcyc  14073  modcyc2  14074  modadd1  14075  modaddabs  14078  muladdmodid  14080  muladdmod  14082  negmod  14086  modadd2mod  14091  modmul1  14094  modmulmodr  14107  modaddmulmod  14108  moddi  14109  modsubdir  14110  modirr  14112  addmodlteq  14116  expgt1  14270  mulexpz  14272  sqgt0  14296  lt2sq  14303  le2sq  14304  sqge0  14306  expmordi  14337  leexp1a  14345  expubnd  14348  sumsqeq0  14349  sqlecan  14380  bernneq  14400  bernneq2  14401  expnbnd  14403  digit2  14407  digit1  14408  expnngt1  14412  swrdccatin2  14906  swrdccat3blem  14916  cshweqrep  15000  sgnneg  15282  crre  15310  crim  15311  reim0  15314  mulre  15317  rere  15318  remul2  15326  rediv  15327  immul2  15333  imdiv  15334  cjre  15335  cjreim  15356  rennim  15435  resqrex  15446  resqreu  15448  resqrtcl  15449  resqrtthlem  15450  sqrtneglem  15462  sqrtneg  15463  absreimsq  15488  absreim  15489  absnid  15494  leabs  15495  absre  15497  absresq  15498  sqabs  15503  max0add  15506  absz  15507  absdiflt  15514  absdifle  15515  lenegsq  15517  abssuble0  15525  absmax  15526  rddif  15537  absrdbnd  15538  o1rlimmul  15815  caurcvg2  15874  reefcl  16282  efgt0  16300  reeftlcl  16305  resinval  16332  recosval  16333  resin4p  16335  recos4p  16336  resincl  16337  recoscl  16338  retancl  16339  resinhcl  16353  rpcoshcl  16354  retanhcl  16356  tanhlt1  16357  tanhbnd  16358  efieq  16360  sinbnd  16377  cosbnd  16378  absefi  16393  dvdsaddre2b  16506  odd2np1  16540  bezoutlem1  16741  xrsdsreclb  21750  remulg  21943  resubdrg  21944  remetdval  25138  bl2ioo  25141  ioo2bl  25142  cnperf  25170  icccvx  25301  tcphcph  25588  shft2rab  25859  volsup2  25956  volcn  25957  c1lip1  26347  plyreres  26634  aalioulem3  26691  taylthlem2  26731  reeff1o  26804  reefgim  26807  sincosq1sgn  26857  sincosq2sgn  26858  sincosq3sgn  26859  sincosq4sgn  26860  sinq12gt0  26866  pige3ALT  26878  efif1olem4  26903  efifo  26905  relogrn  26919  logrnaddcl  26932  relogoprlem  26949  advlog  27012  advlogexp  27013  logtayl  27018  recxpcl  27033  rpcxpcl  27034  cxpge0  27041  cxpcom  27097  dvcxp1  27098  logreclem  27120  relogbreexp  27133  relogbcxp  27143  angpieqvd  27189  atanre  27243  basellem9  27446  gausslemma2dlem1a  27722  2sqnn0  27795  log2sumbnd  27901  brbtwn2  29513  colinearalglem4  29517  colinearalg  29518  crctcshwlkn0lem1  30429  nvsge0  31296  nmoub3i  31405  nmlnoubi  31428  isblo3i  31433  ipasslem3  31465  ipasslem9  31470  ipasslem11  31472  hmopm  32653  riesz1  32697  leopmuli  32765  leopmul  32766  leopmul2i  32767  leopnmid  32770  nmopleid  32771  cdj1i  33065  cdj3lem1  33066  cdj3i  33073  addltmulALT  33120  dpfrac1  33528  rexdiv  33562  xdivid  33564  xdiv0  33565  lediv2aALT  36609  nndivlub  37424  irrdiff  38439  cos2h  38726  tan2h  38727  poimir  38763  mblfinlem2  38768  mblfinlem4  38770  itg2addnclem  38781  itg2addnclem2  38782  dvasin  38814  areacirclem1  38818  areacirclem2  38819  areacirclem4  38821  areacirclem5  38822  areacirc  38823  lcmineqlem12  43282  dvrelog2b  43308  aks4d1p1p6  43315  retire  43569  readvrec2  43605  readvrec  43606  resubeulem2  43620  renegneg  43656  renegid2  43658  sn-it0e0  43660  sn-negex12  43661  resubeqsub  43674  sn-mullid  43680  sn-mul02  43709  areaquad  44410  reabssgn  44828  radcnvrat  45490  lhe4.4ex1a  45505  expgrowthi  45509  mulltgt0  46244  refsum2cnlem1  46259  infnsuprnmpt  46467  dstregt0  46503  suplesup  46556  infleinflem1  46586  infleinflem2  46587  ltdiv23neg  46610  rexabslelem  46633  supminfrnmpt  46660  supminfxr  46679  fmul01lt1lem1  46801  lptre2pt  46855  cnrefiisplem  47044  dvcosre  47127  itgsin0pilem1  47165  itgsinexplem1  47169  volioc  47187  volico  47198  stoweidlem7  47222  stoweidlem10  47225  stoweidlem19  47234  stoweidlem34  47249  stoweid  47278  dirker2re  47307  dirkerdenne0  47308  dirkerper  47311  dirkertrigeq  47316  dirkeritg  47317  fourierdlem39  47361  fourierdlem42  47364  fourierdlem47  47368  fourierdlem56  47377  fourierdlem57  47378  fourierdlem58  47379  fourierdlem60  47381  fourierdlem61  47382  fourierdlem73  47394  fourierdlem76  47397  fourierdlem77  47398  fourierdlem92  47413  fourierdlem97  47418  etransclem46  47495  volico2  47856  smflimlem4  47989  smfinflem  48032  et-sqrtnegnre  48088  squeezedltsq  48117  2leaddle2  48573  ltsubsubaddltsub  48576  sqrtnegnre  48582  ceildivmod  48620  m1mod0mod1  48635  requad01  48924  requad1  48925  bgoldbtbndlem2  49109  flsubz  49839  rege1logbrege0  49875  nn0digval  49917  rrx2vlinest  50058  line2  50069  line2xlem  50070  line2x  50071  itscnhlc0yqe  50076  itsclc0yqsollem2  50080  itsclc0yqsol  50081  itscnhlc0xyqsol  50082  itschlc0xyqsol1  50083  itsclc0xyqsolr  50086  itsclquadb  50093  reseccl  51126  recsccl  51127  recotcl  51128