Theorem recn 7572

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

Syntax hints:   → wi 4   ∈ wcel 1445  ℂcc 7445  ℝcr 7446

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-resscn 7534

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026

This theorem is referenced by:  mulid1  7582  recnd  7613  pnfnre  7626  mnfnre  7627  cnegexlem1  7754  cnegexlem2  7755  cnegexlem3  7756  cnegex  7757  renegcl  7840  resubcl  7843  negf1o  7957  mul02lem2  7963  ltaddneg  7999  ltaddnegr  8000  ltaddsub2  8012  leaddsub2  8014  leltadd  8022  ltaddpos  8027  ltaddpos2  8028  posdif  8030  lenegcon1  8041  lenegcon2  8042  addge01  8047  addge02  8048  leaddle0  8052  mullt0  8055  recexre  8152  msqge0  8190  mulge0  8193  recexap  8219  ltm1  8404  prodgt02  8411  prodge02  8413  ltmul2  8414  lemul2  8415  lemul2a  8417  ltmulgt12  8423  lemulge12  8425  gt0div  8428  ge0div  8429  ltmuldiv2  8433  ltdivmul  8434  ltdivmul2  8436  ledivmul2  8438  lemuldiv2  8440  negiso  8513  cju  8519  nnge1  8543  halfpos  8745  lt2halves  8749  addltmul  8750  avgle1  8754  avgle2  8755  div4p1lem1div2  8767  nnrecl  8769  elznn0  8863  elznn  8864  nzadd  8900  zmulcl  8901  elz2  8916  gtndiv  8940  zeo  8950  supminfex  9184  eqreznegel  9198  negm  9199  irradd  9230  irrmul  9231  divlt1lt  9300  divle1le  9301  xnegneg  9399  rexsub  9419  xnegid  9425  xaddcom  9427  xaddid1  9428  xnegdi  9434  xaddass  9435  xleaddadd  9453  divelunit  9568  fzonmapblen  9747  expgt1  10124  mulexpzap  10126  leexp1a  10141  expubnd  10143  sqgt0ap  10154  lt2sq  10159  le2sq  10160  sqge0  10162  sumsqeq0  10164  bernneq  10205  bernneq2  10206  crre  10422  crim  10423  reim0  10426  mulreap  10429  rere  10430  remul2  10438  redivap  10439  immul2  10445  imdivap  10446  cjre  10447  cjreim  10468  rennim  10566  sqrt0rlem  10567  resqrexlemover  10574  absreimsq  10631  absreim  10632  absnid  10637  leabs  10638  absre  10641  absresq  10642  sqabs  10646  ltabs  10651  absdiflt  10656  absdifle  10657  lenegsq  10659  abssuble0  10667  dfabsmax  10781  max0addsup  10783  negfi  10790  minclpr  10799  reefcl  11123  efgt0  11139  reeftlcl  11144  resinval  11171  recosval  11172  resin4p  11174  recos4p  11175  resincl  11176  recoscl  11177  retanclap  11178  efieq  11191  sinbnd  11208  cosbnd  11209  absefi  11223  odd2np1  11316  infssuzex  11388  remetdval  12329  bl2ioo  12332  ioo2bl  12333