Theorem recn 11290

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11198  ℝcr 11199

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-resscn 11257

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

This theorem is used by:  mulrid  11306  recnd  11337  pnfnre  11350  mnfnre  11352  mul02  11488  ltaddneg  11526  ltaddnegr  11527  renegcli  11619  resubcl  11622  negn0  11745  negf1o  11746  ltaddsub2  11791  leaddsub2  11793  leltadd  11800  ltaddpos  11806  ltaddpos2  11807  posdif  11809  lenegcon1  11820  lenegcon2  11821  addge01  11826  addge02  11827  leaddle0  11831  mullt0  11835  recex  11948  ltm1  12159  prodgt02  12165  ltmul2  12168  lemul1  12169  lemul2  12170  lemul1a  12171  lemul2a  12172  ltmulgt12  12177  lemulge12  12180  gt0div  12183  ge0div  12184  mulge0b  12187  mulle0b  12188  ltmuldiv2  12191  ltdivmul  12192  ledivmul  12193  ltdivmul2  12194  lt2mul2div  12195  ledivmul2  12196  lemuldiv2  12198  ltdiv2  12203  ltrec1  12204  lerec2  12205  ledivdiv  12206  lediv2  12207  ltdiv23  12208  lediv23  12209  lediv12a  12210  recp1lt1  12215  ledivp1  12219  negfi  12266  infm3lem  12275  supmul  12289  riotaneg  12296  negiso  12297  cju  12316  nnge1  12366  halfpos  12576  lt2halves  12581  addltmul  12582  avgle1  12586  avgle2  12587  avgle  12588  div4p1lem1div2  12601  nnrecl  12604  difgtsumgt  12659  elznn0  12708  elznn  12709  elz2  12711  nzadd  12744  zmulcl  12745  gtndiv  12776  zeo  12785  eqreznegel  13061  supminf  13062  rebtwnz  13074  irradd  13101  irrmul  13102  divlt1lt  13191  divle1le  13192  max0sub  13326  xnegneg  13344  rexsub  13363  xnegid  13368  xaddcom  13370  xaddrid  13371  xnegdi  13378  xaddass  13379  rexmul  13401  xmulasslem3  13416  xadddilem  13424  divelunit  13625  fzonmapblen  13843  ico01fl0  13959  flzadd  13966  ltdifltdiv  13974  dfceil2  13979  intfrac2  13998  fldiv2  14001  flpmodeq  14014  mod0  14016  negmod0  14018  modlt  14020  modfrac  14024  flmod  14025  intfrac  14026  modmulnn  14029  modvalp1  14030  modid  14036  modcyc  14046  modcyc2  14047  modadd1  14048  modaddabs  14051  muladdmodid  14053  muladdmod  14055  negmod  14059  modadd2mod  14064  modmul1  14067  modmulmodr  14080  modaddmulmod  14081  moddi  14082  modsubdir  14083  modirr  14085  addmodlteq  14089  expgt1  14243  mulexpz  14245  sqgt0  14269  lt2sq  14276  le2sq  14277  sqge0  14279  expmordi  14310  leexp1a  14318  expubnd  14321  sumsqeq0  14322  sqlecan  14353  bernneq  14373  bernneq2  14374  expnbnd  14376  digit2  14380  digit1  14381  expnngt1  14385  swrdccatin2  14878  swrdccat3blem  14888  cshweqrep  14972  sgnneg  15253  crre  15281  crim  15282  reim0  15285  mulre  15288  rere  15289  remul2  15297  rediv  15298  immul2  15304  imdiv  15305  cjre  15306  cjreim  15327  rennim  15406  resqrex  15417  resqreu  15419  resqrtcl  15420  resqrtthlem  15421  sqrtneglem  15433  sqrtneg  15434  absreimsq  15459  absreim  15460  absnid  15465  leabs  15466  absre  15468  absresq  15469  sqabs  15474  max0add  15477  absz  15478  absdiflt  15485  absdifle  15486  lenegsq  15488  abssuble0  15496  absmax  15497  rddif  15508  absrdbnd  15509  o1rlimmul  15786  caurcvg2  15845  reefcl  16253  efgt0  16271  reeftlcl  16276  resinval  16303  recosval  16304  resin4p  16306  recos4p  16307  resincl  16308  recoscl  16309  retancl  16310  resinhcl  16324  rpcoshcl  16325  retanhcl  16327  tanhlt1  16328  tanhbnd  16329  efieq  16331  sinbnd  16348  cosbnd  16349  absefi  16364  dvdsaddre2b  16477  odd2np1  16511  bezoutlem1  16712  xrsdsreclb  21720  remulg  21913  resubdrg  21914  remetdval  25108  bl2ioo  25111  ioo2bl  25112  cnperf  25140  icccvx  25271  tcphcph  25558  shft2rab  25829  volsup2  25926  volcn  25927  c1lip1  26317  plyreres  26604  aalioulem3  26661  taylthlem2  26701  reeff1o  26774  reefgim  26777  sincosq1sgn  26827  sincosq2sgn  26828  sincosq3sgn  26829  sincosq4sgn  26830  sinq12gt0  26836  pige3ALT  26848  efif1olem4  26873  efifo  26875  relogrn  26889  logrnaddcl  26902  relogoprlem  26919  advlog  26982  advlogexp  26983  logtayl  26988  recxpcl  27003  rpcxpcl  27004  cxpge0  27011  cxpcom  27067  dvcxp1  27068  logreclem  27090  relogbreexp  27103  relogbcxp  27113  angpieqvd  27159  atanre  27213  basellem9  27416  gausslemma2dlem1a  27692  2sqnn0  27765  log2sumbnd  27871  brbtwn2  29483  colinearalglem4  29487  colinearalg  29488  crctcshwlkn0lem1  30399  nvsge0  31266  nmoub3i  31375  nmlnoubi  31398  isblo3i  31403  ipasslem3  31435  ipasslem9  31440  ipasslem11  31442  hmopm  32623  riesz1  32667  leopmuli  32735  leopmul  32736  leopmul2i  32737  leopnmid  32740  nmopleid  32741  cdj1i  33035  cdj3lem1  33036  cdj3i  33043  addltmulALT  33048  dpfrac1  33458  rexdiv  33492  xdivid  33494  xdiv0  33495  lediv2aALT  36442  nndivlub  37246  irrdiff  38248  cos2h  38535  tan2h  38536  poimir  38572  mblfinlem2  38577  mblfinlem4  38579  itg2addnclem  38590  itg2addnclem2  38591  dvasin  38623  areacirclem1  38627  areacirclem2  38628  areacirclem4  38630  areacirclem5  38631  areacirc  38632  lcmineqlem12  43091  dvrelog2b  43117  aks4d1p1p6  43124  retire  43377  readvrec2  43413  readvrec  43414  resubeulem2  43428  renegneg  43464  renegid2  43466  sn-it0e0  43468  sn-negex12  43469  resubeqsub  43482  sn-mullid  43488  sn-mul02  43517  areaquad  44218  reabssgn  44636  radcnvrat  45298  lhe4.4ex1a  45313  expgrowthi  45317  mulltgt0  46039  refsum2cnlem1  46054  infnsuprnmpt  46262  dstregt0  46298  suplesup  46351  infleinflem1  46381  infleinflem2  46382  ltdiv23neg  46405  rexabslelem  46428  supminfrnmpt  46455  supminfxr  46474  fmul01lt1lem1  46596  lptre2pt  46650  cnrefiisplem  46839  dvcosre  46922  itgsin0pilem1  46960  itgsinexplem1  46964  volioc  46982  volico  46993  stoweidlem7  47017  stoweidlem10  47020  stoweidlem19  47029  stoweidlem34  47044  stoweid  47073  dirker2re  47102  dirkerdenne0  47103  dirkerper  47106  dirkertrigeq  47111  dirkeritg  47112  fourierdlem39  47156  fourierdlem42  47159  fourierdlem47  47163  fourierdlem56  47172  fourierdlem57  47173  fourierdlem58  47174  fourierdlem60  47176  fourierdlem61  47177  fourierdlem73  47189  fourierdlem76  47192  fourierdlem77  47193  fourierdlem92  47208  fourierdlem97  47213  etransclem46  47290  volico2  47651  smflimlem4  47784  smfinflem  47827  et-sqrtnegnre  47883  squeezedltsq  47912  2leaddle2  48368  ltsubsubaddltsub  48371  sqrtnegnre  48377  ceildivmod  48415  m1mod0mod1  48430  requad01  48719  requad1  48720  bgoldbtbndlem2  48904  flsubz  49634  rege1logbrege0  49670  nn0digval  49712  rrx2vlinest  49853  line2  49864  line2xlem  49865  line2x  49866  itscnhlc0yqe  49871  itsclc0yqsollem2  49875  itsclc0yqsol  49876  itscnhlc0xyqsol  49877  itschlc0xyqsol1  49878  itsclc0xyqsolr  49881  itsclquadb  49888  reseccl  50846  recsccl  50847  recotcl  50848