Theorem recn 8276

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  ℝcr 8142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  mulrid  8287  recnd  8318  pnfnre  8331  mnfnre  8332  cnegexlem1  8465  cnegexlem2  8466  cnegexlem3  8467  cnegex  8468  renegcl  8551  resubcl  8554  negf1o  8673  mul02lem2  8679  ltaddneg  8716  ltaddnegr  8717  ltaddsub2  8729  leaddsub2  8731  leltadd  8739  ltaddpos  8744  ltaddpos2  8745  posdif  8747  lenegcon1  8758  lenegcon2  8759  addge01  8764  addge02  8765  leaddle0  8769  mullt0  8772  recexre  8870  msqge0  8908  mulge0  8911  aprcl  8938  recexap  8945  rerecapb  9137  ltm1  9140  prodgt02  9147  prodge02  9149  ltmul2  9150  lemul2  9151  lemul2a  9153  ltmulgt12  9159  lemulge12  9161  gt0div  9164  ge0div  9165  ltmuldiv2  9169  ltdivmul  9170  ltdivmul2  9172  ledivmul2  9174  lemuldiv2  9176  negiso  9249  cju  9255  nnge1  9280  halfpos  9489  lt2halves  9494  addltmul  9495  avgle1  9499  avgle2  9500  div4p1lem1div2  9512  nnrecl  9514  elznn0  9612  elznn  9613  nzadd  9650  zmulcl  9651  difgtsumgt  9667  elz2  9669  gtndiv  9694  zeo  9704  supminfex  9950  eqreznegel  9967  negm  9968  irradd  9999  irrmul  10000  divlt1lt  10078  divle1le  10079  xnegneg  10188  rexsub  10208  xnegid  10214  xaddcom  10216  xaddid1  10217  xnegdi  10223  xaddass  10224  xleaddadd  10242  divelunit  10357  fzonmapblen  10551  infssuzex  10618  expgt1  10966  mulexpzap  10968  leexp1a  10983  expubnd  10985  sqgt0ap  10997  lt2sq  11002  le2sq  11003  sqge0  11005  sumsqeq0  11007  bernneq  11050  bernneq2  11051  nn0ltexp2  11099  swrdccatin2  11449  swrdccat3blem  11459  crre  11570  crim  11571  reim0  11574  mulreap  11577  rere  11578  remul2  11586  redivap  11587  immul2  11593  imdivap  11594  cjre  11595  cjreim  11616  rennim  11715  sqrt0rlem  11716  resqrexlemover  11723  absreimsq  11780  absreim  11781  absnid  11786  leabs  11787  absre  11790  absresq  11791  sqabs  11795  ltabs  11800  absdiflt  11805  absdifle  11806  lenegsq  11808  abssuble0  11816  dfabsmax  11930  max0addsup  11932  negfi  11941  minclpr  11950  reefcl  12382  efgt0  12398  reeftlcl  12403  resinval  12429  recosval  12430  resin4p  12432  recos4p  12433  resincl  12434  recoscl  12435  retanclap  12436  efieq  12449  sinbnd  12466  cosbnd  12467  absefi  12483  odd2np1  12587  remetdval  15541  bl2ioo  15544  ioo2bl  15545  hoverb  15642  plyreres  15758  sincosq1sgn  15820  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  sinq12gt0  15824  relogoprlem  15862  logcxp  15891  rpcxpcl  15897  cxpcom  15932  rprelogbdiv  15951  gausslemma2dlem1a  16060  triap  16952  trirec0  16967