Theorem recn 7753

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7618  ℝcr 7619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7712

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  mulid1  7763  recnd  7794  pnfnre  7807  mnfnre  7808  cnegexlem1  7937  cnegexlem2  7938  cnegexlem3  7939  cnegex  7940  renegcl  8023  resubcl  8026  negf1o  8144  mul02lem2  8150  ltaddneg  8186  ltaddnegr  8187  ltaddsub2  8199  leaddsub2  8201  leltadd  8209  ltaddpos  8214  ltaddpos2  8215  posdif  8217  lenegcon1  8228  lenegcon2  8229  addge01  8234  addge02  8235  leaddle0  8239  mullt0  8242  recexre  8340  msqge0  8378  mulge0  8381  aprcl  8408  recexap  8414  ltm1  8604  prodgt02  8611  prodge02  8613  ltmul2  8614  lemul2  8615  lemul2a  8617  ltmulgt12  8623  lemulge12  8625  gt0div  8628  ge0div  8629  ltmuldiv2  8633  ltdivmul  8634  ltdivmul2  8636  ledivmul2  8638  lemuldiv2  8640  negiso  8713  cju  8719  nnge1  8743  halfpos  8951  lt2halves  8955  addltmul  8956  avgle1  8960  avgle2  8961  div4p1lem1div2  8973  nnrecl  8975  elznn0  9069  elznn  9070  nzadd  9106  zmulcl  9107  elz2  9122  gtndiv  9146  zeo  9156  supminfex  9392  eqreznegel  9406  negm  9407  irradd  9438  irrmul  9439  divlt1lt  9511  divle1le  9512  xnegneg  9616  rexsub  9636  xnegid  9642  xaddcom  9644  xaddid1  9645  xnegdi  9651  xaddass  9652  xleaddadd  9670  divelunit  9785  fzonmapblen  9964  expgt1  10331  mulexpzap  10333  leexp1a  10348  expubnd  10350  sqgt0ap  10361  lt2sq  10366  le2sq  10367  sqge0  10369  sumsqeq0  10371  bernneq  10412  bernneq2  10413  crre  10629  crim  10630  reim0  10633  mulreap  10636  rere  10637  remul2  10645  redivap  10646  immul2  10652  imdivap  10653  cjre  10654  cjreim  10675  rennim  10774  sqrt0rlem  10775  resqrexlemover  10782  absreimsq  10839  absreim  10840  absnid  10845  leabs  10846  absre  10849  absresq  10850  sqabs  10854  ltabs  10859  absdiflt  10864  absdifle  10865  lenegsq  10867  abssuble0  10875  dfabsmax  10989  max0addsup  10991  negfi  10999  minclpr  11008  reefcl  11374  efgt0  11390  reeftlcl  11395  resinval  11422  recosval  11423  resin4p  11425  recos4p  11426  resincl  11427  recoscl  11428  retanclap  11429  efieq  11442  sinbnd  11459  cosbnd  11460  absefi  11475  odd2np1  11570  infssuzex  11642  remetdval  12708  bl2ioo  12711  ioo2bl  12712  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  triap  13224