Theorem recn 7746

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7611  ℝcr 7612

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 2119  ax-resscn 7705

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  mulid1  7756  recnd  7787  pnfnre  7800  mnfnre  7801  cnegexlem1  7930  cnegexlem2  7931  cnegexlem3  7932  cnegex  7933  renegcl  8016  resubcl  8019  negf1o  8137  mul02lem2  8143  ltaddneg  8179  ltaddnegr  8180  ltaddsub2  8192  leaddsub2  8194  leltadd  8202  ltaddpos  8207  ltaddpos2  8208  posdif  8210  lenegcon1  8221  lenegcon2  8222  addge01  8227  addge02  8228  leaddle0  8232  mullt0  8235  recexre  8333  msqge0  8371  mulge0  8374  aprcl  8401  recexap  8407  ltm1  8597  prodgt02  8604  prodge02  8606  ltmul2  8607  lemul2  8608  lemul2a  8610  ltmulgt12  8616  lemulge12  8618  gt0div  8621  ge0div  8622  ltmuldiv2  8626  ltdivmul  8627  ltdivmul2  8629  ledivmul2  8631  lemuldiv2  8633  negiso  8706  cju  8712  nnge1  8736  halfpos  8944  lt2halves  8948  addltmul  8949  avgle1  8953  avgle2  8954  div4p1lem1div2  8966  nnrecl  8968  elznn0  9062  elznn  9063  nzadd  9099  zmulcl  9100  elz2  9115  gtndiv  9139  zeo  9149  supminfex  9385  eqreznegel  9399  negm  9400  irradd  9431  irrmul  9432  divlt1lt  9504  divle1le  9505  xnegneg  9609  rexsub  9629  xnegid  9635  xaddcom  9637  xaddid1  9638  xnegdi  9644  xaddass  9645  xleaddadd  9663  divelunit  9778  fzonmapblen  9957  expgt1  10324  mulexpzap  10326  leexp1a  10341  expubnd  10343  sqgt0ap  10354  lt2sq  10359  le2sq  10360  sqge0  10362  sumsqeq0  10364  bernneq  10405  bernneq2  10406  crre  10622  crim  10623  reim0  10626  mulreap  10629  rere  10630  remul2  10638  redivap  10639  immul2  10645  imdivap  10646  cjre  10647  cjreim  10668  rennim  10767  sqrt0rlem  10768  resqrexlemover  10775  absreimsq  10832  absreim  10833  absnid  10838  leabs  10839  absre  10842  absresq  10843  sqabs  10847  ltabs  10852  absdiflt  10857  absdifle  10858  lenegsq  10860  abssuble0  10868  dfabsmax  10982  max0addsup  10984  negfi  10992  minclpr  11001  reefcl  11363  efgt0  11379  reeftlcl  11384  resinval  11411  recosval  11412  resin4p  11414  recos4p  11415  resincl  11416  recoscl  11417  retanclap  11418  efieq  11431  sinbnd  11448  cosbnd  11449  absefi  11464  odd2np1  11559  infssuzex  11631  remetdval  12697  bl2ioo  12700  ioo2bl  12701  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  sinq12gt0  12900  triap  13213