Theorem recn 7106

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  ℝcr 6980

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 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  mulid1  7116  recnd  7147  pnfnre  7160  mnfnre  7161  cnegexlem1  7283  cnegexlem2  7284  cnegexlem3  7285  cnegex  7286  renegcl  7369  resubcl  7372  negf1o  7486  mul02lem2  7492  ltaddneg  7528  ltaddnegr  7529  ltaddsub2  7541  leaddsub2  7543  leltadd  7551  ltaddpos  7556  ltaddpos2  7557  posdif  7559  lenegcon1  7570  lenegcon2  7571  addge01  7576  addge02  7577  leaddle0  7581  mullt0  7584  recexre  7678  msqge0  7716  mulge0  7719  recexap  7743  ltm1  7924  prodgt02  7931  prodge02  7933  ltmul2  7934  lemul2  7935  lemul2a  7937  ltmulgt12  7943  lemulge12  7945  gt0div  7948  ge0div  7949  ltmuldiv2  7953  ltdivmul  7954  ltdivmul2  7956  ledivmul2  7958  lemuldiv2  7960  negiso  8033  cju  8038  nnge1  8062  halfpos  8262  lt2halves  8266  addltmul  8267  avgle1  8271  avgle2  8272  div4p1lem1div2  8284  nnrecl  8286  elznn0  8366  elznn  8367  nzadd  8403  zmulcl  8404  elz2  8419  gtndiv  8442  zeo  8452  supminfex  8685  eqreznegel  8699  negm  8700  irradd  8731  irrmul  8732  divlt1lt  8801  divle1le  8802  xnegneg  8900  divelunit  9024  fzonmapblen  9196  expgt1  9514  mulexpzap  9516  leexp1a  9531  expubnd  9533  sqgt0ap  9544  lt2sq  9549  le2sq  9550  sqge0  9552  sumsqeq0  9554  bernneq  9593  bernneq2  9594  crre  9744  crim  9745  reim0  9748  mulreap  9751  rere  9752  remul2  9760  redivap  9761  immul2  9767  imdivap  9768  cjre  9769  cjreim  9790  rennim  9888  sqrt0rlem  9889  resqrexlemover  9896  absreimsq  9953  absreim  9954  absnid  9959  leabs  9960  absre  9963  absresq  9964  sqabs  9968  ltabs  9973  absdiflt  9978  absdifle  9979  lenegsq  9981  abssuble0  9989  dfabsmax  10103  max0addsup  10105  negfi  10110  odd2np1  10272  infssuzex  10345