Theorem recn 11293

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11201  ℝcr 11202

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-resscn 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896

This theorem is used by:  mulrid  11309  recnd  11340  pnfnre  11353  mnfnre  11355  mul02  11491  ltaddneg  11529  ltaddnegr  11530  renegcli  11622  resubcl  11625  negn0  11748  negf1o  11749  ltaddsub2  11794  leaddsub2  11796  leltadd  11803  ltaddpos  11809  ltaddpos2  11810  posdif  11812  lenegcon1  11823  lenegcon2  11824  addge01  11829  addge02  11830  leaddle0  11834  mullt0  11838  recex  11951  ltm1  12162  prodgt02  12168  ltmul2  12171  lemul1  12172  lemul2  12173  lemul1a  12174  lemul2a  12175  ltmulgt12  12180  lemulge12  12183  gt0div  12186  ge0div  12187  mulge0b  12190  mulle0b  12191  ltmuldiv2  12194  ltdivmul  12195  ledivmul  12196  ltdivmul2  12197  lt2mul2div  12198  ledivmul2  12199  lemuldiv2  12201  ltdiv2  12206  ltrec1  12207  lerec2  12208  ledivdiv  12209  lediv2  12210  ltdiv23  12211  lediv23  12212  lediv12a  12213  recp1lt1  12218  ledivp1  12222  negfi  12269  infm3lem  12278  supmul  12292  riotaneg  12299  negiso  12300  cju  12319  nnge1  12369  halfpos  12579  lt2halves  12584  addltmul  12585  avgle1  12589  avgle2  12590  avgle  12591  div4p1lem1div2  12604  nnrecl  12607  difgtsumgt  12662  elznn0  12711  elznn  12712  elz2  12714  nzadd  12747  zmulcl  12748  gtndiv  12779  zeo  12788  eqreznegel  13064  supminf  13065  rebtwnz  13077  irradd  13104  irrmul  13105  divlt1lt  13194  divle1le  13195  max0sub  13329  xnegneg  13347  rexsub  13366  xnegid  13371  xaddcom  13373  xaddrid  13374  xnegdi  13381  xaddass  13382  rexmul  13404  xmulasslem3  13419  xadddilem  13427  divelunit  13628  fzonmapblen  13846  ico01fl0  13962  flzadd  13969  ltdifltdiv  13977  dfceil2  13982  intfrac2  14001  fldiv2  14004  flpmodeq  14017  mod0  14019  negmod0  14021  modlt  14023  modfrac  14027  flmod  14028  intfrac  14029  modmulnn  14032  modvalp1  14033  modid  14039  modcyc  14049  modcyc2  14050  modadd1  14051  modaddabs  14054  muladdmodid  14056  muladdmod  14058  negmod  14062  modadd2mod  14067  modmul1  14070  modmulmodr  14083  modaddmulmod  14084  moddi  14085  modsubdir  14086  modirr  14088  addmodlteq  14092  expgt1  14246  mulexpz  14248  sqgt0  14272  lt2sq  14279  le2sq  14280  sqge0  14282  expmordi  14313  leexp1a  14321  expubnd  14324  sumsqeq0  14325  sqlecan  14356  bernneq  14376  bernneq2  14377  expnbnd  14379  digit2  14383  digit1  14384  expnngt1  14388  swrdccatin2  14882  swrdccat3blem  14892  cshweqrep  14976  sgnneg  15258  crre  15286  crim  15287  reim0  15290  mulre  15293  rere  15294  remul2  15302  rediv  15303  immul2  15309  imdiv  15310  cjre  15311  cjreim  15332  rennim  15411  resqrex  15422  resqreu  15424  resqrtcl  15425  resqrtthlem  15426  sqrtneglem  15438  sqrtneg  15439  absreimsq  15464  absreim  15465  absnid  15470  leabs  15471  absre  15473  absresq  15474  sqabs  15479  max0add  15482  absz  15483  absdiflt  15490  absdifle  15491  lenegsq  15493  abssuble0  15501  absmax  15502  rddif  15513  absrdbnd  15514  o1rlimmul  15791  caurcvg2  15850  reefcl  16258  efgt0  16276  reeftlcl  16281  resinval  16308  recosval  16309  resin4p  16311  recos4p  16312  resincl  16313  recoscl  16314  retancl  16315  resinhcl  16329  rpcoshcl  16330  retanhcl  16332  tanhlt1  16333  tanhbnd  16334  efieq  16336  sinbnd  16353  cosbnd  16354  absefi  16369  dvdsaddre2b  16482  odd2np1  16516  bezoutlem1  16717  xrsdsreclb  21725  remulg  21918  resubdrg  21919  remetdval  25113  bl2ioo  25116  ioo2bl  25117  cnperf  25145  icccvx  25276  tcphcph  25563  shft2rab  25834  volsup2  25931  volcn  25932  c1lip1  26322  plyreres  26609  aalioulem3  26666  taylthlem2  26706  reeff1o  26779  reefgim  26782  sincosq1sgn  26832  sincosq2sgn  26833  sincosq3sgn  26834  sincosq4sgn  26835  sinq12gt0  26841  pige3ALT  26853  efif1olem4  26878  efifo  26880  relogrn  26894  logrnaddcl  26907  relogoprlem  26924  advlog  26987  advlogexp  26988  logtayl  26993  recxpcl  27008  rpcxpcl  27009  cxpge0  27016  cxpcom  27072  dvcxp1  27073  logreclem  27095  relogbreexp  27108  relogbcxp  27118  angpieqvd  27164  atanre  27218  basellem9  27421  gausslemma2dlem1a  27697  2sqnn0  27770  log2sumbnd  27876  brbtwn2  29488  colinearalglem4  29492  colinearalg  29493  crctcshwlkn0lem1  30404  nvsge0  31271  nmoub3i  31380  nmlnoubi  31403  isblo3i  31408  ipasslem3  31440  ipasslem9  31445  ipasslem11  31447  hmopm  32628  riesz1  32672  leopmuli  32740  leopmul  32741  leopmul2i  32742  leopnmid  32745  nmopleid  32746  cdj1i  33040  cdj3lem1  33041  cdj3i  33048  addltmulALT  33095  dpfrac1  33504  rexdiv  33538  xdivid  33540  xdiv0  33541  lediv2aALT  36528  nndivlub  37338  irrdiff  38340  cos2h  38627  tan2h  38628  poimir  38664  mblfinlem2  38669  mblfinlem4  38671  itg2addnclem  38682  itg2addnclem2  38683  dvasin  38715  areacirclem1  38719  areacirclem2  38720  areacirclem4  38722  areacirclem5  38723  areacirc  38724  lcmineqlem12  43183  dvrelog2b  43209  aks4d1p1p6  43216  retire  43469  readvrec2  43505  readvrec  43506  resubeulem2  43520  renegneg  43556  renegid2  43558  sn-it0e0  43560  sn-negex12  43561  resubeqsub  43574  sn-mullid  43580  sn-mul02  43609  areaquad  44311  reabssgn  44729  radcnvrat  45391  lhe4.4ex1a  45406  expgrowthi  45410  mulltgt0  46132  refsum2cnlem1  46147  infnsuprnmpt  46355  dstregt0  46391  suplesup  46444  infleinflem1  46474  infleinflem2  46475  ltdiv23neg  46498  rexabslelem  46521  supminfrnmpt  46548  supminfxr  46567  fmul01lt1lem1  46689  lptre2pt  46743  cnrefiisplem  46932  dvcosre  47015  itgsin0pilem1  47053  itgsinexplem1  47057  volioc  47075  volico  47086  stoweidlem7  47110  stoweidlem10  47113  stoweidlem19  47122  stoweidlem34  47137  stoweid  47166  dirker2re  47195  dirkerdenne0  47196  dirkerper  47199  dirkertrigeq  47204  dirkeritg  47205  fourierdlem39  47249  fourierdlem42  47252  fourierdlem47  47256  fourierdlem56  47265  fourierdlem57  47266  fourierdlem58  47267  fourierdlem60  47269  fourierdlem61  47270  fourierdlem73  47282  fourierdlem76  47285  fourierdlem77  47286  fourierdlem92  47301  fourierdlem97  47306  etransclem46  47383  volico2  47744  smflimlem4  47877  smfinflem  47920  et-sqrtnegnre  47976  squeezedltsq  48005  2leaddle2  48461  ltsubsubaddltsub  48464  sqrtnegnre  48470  ceildivmod  48508  m1mod0mod1  48523  requad01  48812  requad1  48813  bgoldbtbndlem2  48997  flsubz  49727  rege1logbrege0  49763  nn0digval  49805  rrx2vlinest  49946  line2  49957  line2xlem  49958  line2x  49959  itscnhlc0yqe  49964  itsclc0yqsollem2  49968  itsclc0yqsol  49969  itscnhlc0xyqsol  49970  itschlc0xyqsol1  49971  itsclc0xyqsolr  49974  itsclquadb  49981  reseccl  51014  recsccl  51015  recotcl  51016