Theorem recn 7419

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

Syntax hints:   → wi 4   ∈ wcel 1436  ℂcc 7292  ℝcr 7293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-resscn 7381

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001

This theorem is referenced by:  mulid1  7429  recnd  7460  pnfnre  7473  mnfnre  7474  cnegexlem1  7601  cnegexlem2  7602  cnegexlem3  7603  cnegex  7604  renegcl  7687  resubcl  7690  negf1o  7804  mul02lem2  7810  ltaddneg  7846  ltaddnegr  7847  ltaddsub2  7859  leaddsub2  7861  leltadd  7869  ltaddpos  7874  ltaddpos2  7875  posdif  7877  lenegcon1  7888  lenegcon2  7889  addge01  7894  addge02  7895  leaddle0  7899  mullt0  7902  recexre  7996  msqge0  8034  mulge0  8037  recexap  8061  ltm1  8242  prodgt02  8249  prodge02  8251  ltmul2  8252  lemul2  8253  lemul2a  8255  ltmulgt12  8261  lemulge12  8263  gt0div  8266  ge0div  8267  ltmuldiv2  8271  ltdivmul  8272  ltdivmul2  8274  ledivmul2  8276  lemuldiv2  8278  negiso  8351  cju  8356  nnge1  8380  halfpos  8580  lt2halves  8584  addltmul  8585  avgle1  8589  avgle2  8590  div4p1lem1div2  8602  nnrecl  8604  elznn0  8698  elznn  8699  nzadd  8735  zmulcl  8736  elz2  8751  gtndiv  8774  zeo  8784  supminfex  9017  eqreznegel  9031  negm  9032  irradd  9063  irrmul  9064  divlt1lt  9133  divle1le  9134  xnegneg  9227  divelunit  9351  fzonmapblen  9526  expgt1  9892  mulexpzap  9894  leexp1a  9909  expubnd  9911  sqgt0ap  9922  lt2sq  9927  le2sq  9928  sqge0  9930  sumsqeq0  9932  bernneq  9971  bernneq2  9972  crre  10187  crim  10188  reim0  10191  mulreap  10194  rere  10195  remul2  10203  redivap  10204  immul2  10210  imdivap  10211  cjre  10212  cjreim  10233  rennim  10331  sqrt0rlem  10332  resqrexlemover  10339  absreimsq  10396  absreim  10397  absnid  10402  leabs  10403  absre  10406  absresq  10407  sqabs  10411  ltabs  10416  absdiflt  10421  absdifle  10422  lenegsq  10424  abssuble0  10432  dfabsmax  10546  max0addsup  10548  negfi  10554  odd2np1  10755  infssuzex  10827