Theorem recn 8170

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℂcc 8035  ℝcr 8036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-resscn 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  mulrid  8181  recnd  8213  pnfnre  8226  mnfnre  8227  cnegexlem1  8359  cnegexlem2  8360  cnegexlem3  8361  cnegex  8362  renegcl  8445  resubcl  8448  negf1o  8566  mul02lem2  8572  ltaddneg  8609  ltaddnegr  8610  ltaddsub2  8622  leaddsub2  8624  leltadd  8632  ltaddpos  8637  ltaddpos2  8638  posdif  8640  lenegcon1  8651  lenegcon2  8652  addge01  8657  addge02  8658  leaddle0  8662  mullt0  8665  recexre  8763  msqge0  8801  mulge0  8804  aprcl  8831  recexap  8838  rerecapb  9028  ltm1  9031  prodgt02  9038  prodge02  9040  ltmul2  9041  lemul2  9042  lemul2a  9044  ltmulgt12  9050  lemulge12  9052  gt0div  9055  ge0div  9056  ltmuldiv2  9060  ltdivmul  9061  ltdivmul2  9063  ledivmul2  9065  lemuldiv2  9067  negiso  9140  cju  9146  nnge1  9171  halfpos  9380  lt2halves  9385  addltmul  9386  avgle1  9390  avgle2  9391  div4p1lem1div2  9403  nnrecl  9405  elznn0  9499  elznn  9500  nzadd  9537  zmulcl  9538  difgtsumgt  9554  elz2  9556  gtndiv  9580  zeo  9590  supminfex  9836  eqreznegel  9853  negm  9854  irradd  9885  irrmul  9886  divlt1lt  9964  divle1le  9965  xnegneg  10073  rexsub  10093  xnegid  10099  xaddcom  10101  xaddid1  10102  xnegdi  10108  xaddass  10109  xleaddadd  10127  divelunit  10242  fzonmapblen  10432  infssuzex  10499  expgt1  10845  mulexpzap  10847  leexp1a  10862  expubnd  10864  sqgt0ap  10876  lt2sq  10881  le2sq  10882  sqge0  10884  sumsqeq0  10886  bernneq  10928  bernneq2  10929  nn0ltexp2  10977  swrdccatin2  11319  swrdccat3blem  11329  crre  11440  crim  11441  reim0  11444  mulreap  11447  rere  11448  remul2  11456  redivap  11457  immul2  11463  imdivap  11464  cjre  11465  cjreim  11486  rennim  11585  sqrt0rlem  11586  resqrexlemover  11593  absreimsq  11650  absreim  11651  absnid  11656  leabs  11657  absre  11660  absresq  11661  sqabs  11665  ltabs  11670  absdiflt  11675  absdifle  11676  lenegsq  11678  abssuble0  11686  dfabsmax  11800  max0addsup  11802  negfi  11811  minclpr  11820  reefcl  12252  efgt0  12268  reeftlcl  12273  resinval  12299  recosval  12300  resin4p  12302  recos4p  12303  resincl  12304  recoscl  12305  retanclap  12306  efieq  12319  sinbnd  12336  cosbnd  12337  absefi  12353  odd2np1  12457  remetdval  15300  bl2ioo  15303  ioo2bl  15304  hoverb  15401  plyreres  15517  sincosq1sgn  15579  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  sinq12gt0  15583  relogoprlem  15621  logcxp  15650  rpcxpcl  15656  cxpcom  15691  rprelogbdiv  15710  gausslemma2dlem1a  15816  triap  16700  trirec0  16715