Theorem recn 11271

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

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

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 11238

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  11287  recnd  11318  pnfnre  11331  mnfnre  11333  mul02  11469  ltaddneg  11507  ltaddnegr  11508  renegcli  11600  resubcl  11603  negn0  11726  negf1o  11727  ltaddsub2  11772  leaddsub2  11774  leltadd  11781  ltaddpos  11787  ltaddpos2  11788  posdif  11790  lenegcon1  11801  lenegcon2  11802  addge01  11807  addge02  11808  leaddle0  11812  mullt0  11816  recex  11929  ltm1  12140  prodgt02  12146  ltmul2  12149  lemul1  12150  lemul2  12151  lemul1a  12152  lemul2a  12153  ltmulgt12  12158  lemulge12  12161  gt0div  12164  ge0div  12165  mulge0b  12168  mulle0b  12169  ltmuldiv2  12172  ltdivmul  12173  ledivmul  12174  ltdivmul2  12175  lt2mul2div  12176  ledivmul2  12177  lemuldiv2  12179  ltdiv2  12184  ltrec1  12185  lerec2  12186  ledivdiv  12187  lediv2  12188  ltdiv23  12189  lediv23  12190  lediv12a  12191  recp1lt1  12196  ledivp1  12200  negfi  12247  infm3lem  12256  supmul  12270  riotaneg  12277  negiso  12278  cju  12297  nnge1  12347  halfpos  12557  lt2halves  12562  addltmul  12563  avgle1  12567  avgle2  12568  avgle  12569  div4p1lem1div2  12582  nnrecl  12585  difgtsumgt  12640  elznn0  12689  elznn  12690  elz2  12692  nzadd  12725  zmulcl  12726  gtndiv  12757  zeo  12766  eqreznegel  13042  supminf  13043  rebtwnz  13055  irradd  13082  irrmul  13083  divlt1lt  13172  divle1le  13173  max0sub  13307  xnegneg  13325  rexsub  13344  xnegid  13349  xaddcom  13351  xaddrid  13352  xnegdi  13359  xaddass  13360  rexmul  13382  xmulasslem3  13397  xadddilem  13405  divelunit  13606  fzonmapblen  13823  ico01fl0  13939  flzadd  13946  ltdifltdiv  13954  dfceil2  13959  intfrac2  13978  fldiv2  13981  flpmodeq  13994  mod0  13996  negmod0  13998  modlt  14000  modfrac  14004  flmod  14005  intfrac  14006  modmulnn  14009  modvalp1  14010  modid  14016  modcyc  14026  modcyc2  14027  modadd1  14028  modaddabs  14031  muladdmodid  14033  muladdmod  14035  negmod  14039  modadd2mod  14044  modmul1  14047  modmulmodr  14060  modaddmulmod  14061  moddi  14062  modsubdir  14063  modirr  14065  addmodlteq  14069  expgt1  14223  mulexpz  14225  sqgt0  14249  lt2sq  14256  le2sq  14257  sqge0  14259  expmordi  14290  leexp1a  14298  expubnd  14301  sumsqeq0  14302  sqlecan  14333  bernneq  14353  bernneq2  14354  expnbnd  14356  digit2  14360  digit1  14361  expnngt1  14365  swrdccatin2  14858  swrdccat3blem  14868  cshweqrep  14952  sgnneg  15233  crre  15261  crim  15262  reim0  15265  mulre  15268  rere  15269  remul2  15277  rediv  15278  immul2  15284  imdiv  15285  cjre  15286  cjreim  15307  rennim  15386  resqrex  15397  resqreu  15399  resqrtcl  15400  resqrtthlem  15401  sqrtneglem  15413  sqrtneg  15414  absreimsq  15439  absreim  15440  absnid  15445  leabs  15446  absre  15448  absresq  15449  sqabs  15454  max0add  15457  absz  15458  absdiflt  15465  absdifle  15466  lenegsq  15468  abssuble0  15476  absmax  15477  rddif  15488  absrdbnd  15489  o1rlimmul  15766  caurcvg2  15825  reefcl  16233  efgt0  16251  reeftlcl  16256  resinval  16283  recosval  16284  resin4p  16286  recos4p  16287  resincl  16288  recoscl  16289  retancl  16290  resinhcl  16304  rpcoshcl  16305  retanhcl  16307  tanhlt1  16308  tanhbnd  16309  efieq  16311  sinbnd  16328  cosbnd  16329  absefi  16344  dvdsaddre2b  16457  odd2np1  16491  bezoutlem1  16692  xrsdsreclb  21700  remulg  21893  resubdrg  21894  remetdval  25088  bl2ioo  25091  ioo2bl  25092  cnperf  25120  icccvx  25251  tcphcph  25538  shft2rab  25809  volsup2  25906  volcn  25907  c1lip1  26297  plyreres  26586  aalioulem3  26643  taylthlem2  26683  reeff1o  26756  reefgim  26759  sincosq1sgn  26809  sincosq2sgn  26810  sincosq3sgn  26811  sincosq4sgn  26812  sinq12gt0  26818  pige3ALT  26830  efif1olem4  26855  efifo  26857  relogrn  26871  logrnaddcl  26884  relogoprlem  26901  advlog  26964  advlogexp  26965  logtayl  26970  recxpcl  26985  rpcxpcl  26986  cxpge0  26993  cxpcom  27049  dvcxp1  27050  logreclem  27072  relogbreexp  27085  relogbcxp  27095  angpieqvd  27141  atanre  27195  basellem9  27398  gausslemma2dlem1a  27674  2sqnn0  27747  log2sumbnd  27853  brbtwn2  29465  colinearalglem4  29469  colinearalg  29470  crctcshwlkn0lem1  30381  nvsge0  31248  nmoub3i  31357  nmlnoubi  31380  isblo3i  31385  ipasslem3  31417  ipasslem9  31422  ipasslem11  31424  hmopm  32605  riesz1  32649  leopmuli  32717  leopmul  32718  leopmul2i  32719  leopnmid  32722  nmopleid  32723  cdj1i  33017  cdj3lem1  33018  cdj3i  33025  addltmulALT  33030  dpfrac1  33440  rexdiv  33474  xdivid  33476  xdiv0  33477  lediv2aALT  36411  nndivlub  37216  irrdiff  38215  cos2h  38502  tan2h  38503  poimir  38539  mblfinlem2  38544  mblfinlem4  38546  itg2addnclem  38557  itg2addnclem2  38558  dvasin  38590  areacirclem1  38594  areacirclem2  38595  areacirclem4  38597  areacirclem5  38598  areacirc  38599  lcmineqlem12  43058  dvrelog2b  43084  aks4d1p1p6  43091  retire  43344  readvrec2  43380  readvrec  43381  resubeulem2  43395  renegneg  43431  renegid2  43433  sn-it0e0  43435  sn-negex12  43436  resubeqsub  43449  sn-mullid  43455  sn-mul02  43484  areaquad  44176  reabssgn  44595  radcnvrat  45257  lhe4.4ex1a  45272  expgrowthi  45276  mulltgt0  45982  refsum2cnlem1  45997  infnsuprnmpt  46205  dstregt0  46241  suplesup  46295  infleinflem1  46325  infleinflem2  46326  ltdiv23neg  46349  rexabslelem  46372  supminfrnmpt  46399  supminfxr  46418  fmul01lt1lem1  46540  lptre2pt  46594  cnrefiisplem  46783  dvcosre  46866  itgsin0pilem1  46904  itgsinexplem1  46908  volioc  46926  volico  46937  stoweidlem7  46961  stoweidlem10  46964  stoweidlem19  46973  stoweidlem34  46988  stoweid  47017  dirker2re  47046  dirkerdenne0  47047  dirkerper  47050  dirkertrigeq  47055  dirkeritg  47056  fourierdlem39  47100  fourierdlem42  47103  fourierdlem47  47107  fourierdlem56  47116  fourierdlem57  47117  fourierdlem58  47118  fourierdlem60  47120  fourierdlem61  47121  fourierdlem73  47133  fourierdlem76  47136  fourierdlem77  47137  fourierdlem92  47152  fourierdlem97  47157  etransclem46  47234  volico2  47595  smflimlem4  47728  smfinflem  47771  et-sqrtnegnre  47827  squeezedltsq  47856  2leaddle2  48312  ltsubsubaddltsub  48315  sqrtnegnre  48321  ceildivmod  48359  m1mod0mod1  48374  requad01  48663  requad1  48664  bgoldbtbndlem2  48848  flsubz  49578  rege1logbrege0  49614  nn0digval  49656  rrx2vlinest  49797  line2  49808  line2xlem  49809  line2x  49810  itscnhlc0yqe  49815  itsclc0yqsollem2  49819  itsclc0yqsol  49820  itscnhlc0xyqsol  49821  itschlc0xyqsol1  49822  itsclc0xyqsolr  49825  itsclquadb  49832  reseccl  50790  recsccl  50791  recotcl  50792