ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recn GIF version

Theorem recn 7014
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 6976 . 2 ℝ ⊆ ℂ
21sseli 2941 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  cc 6887  cr 6888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-resscn 6976
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931
This theorem is referenced by:  mulid1  7024  recnd  7054  pnfnre  7067  mnfnre  7068  cnegexlem1  7186  cnegexlem2  7187  cnegexlem3  7188  cnegex  7189  renegcl  7272  resubcl  7275  mul02lem2  7385  ltaddsub2  7432  leaddsub2  7434  leltadd  7442  ltaddpos  7447  ltaddpos2  7448  posdif  7450  lenegcon1  7461  lenegcon2  7462  addge01  7467  addge02  7468  leaddle0  7472  mullt0  7475  recexre  7569  msqge0  7607  mulge0  7610  recexap  7634  ltm1  7812  prodgt02  7819  prodge02  7821  ltmul2  7822  lemul2  7823  lemul2a  7825  ltmulgt12  7831  lemulge12  7833  gt0div  7836  ge0div  7837  ltmuldiv2  7841  ltdivmul  7842  ltdivmul2  7844  ledivmul2  7846  lemuldiv2  7848  cju  7913  nnge1  7937  halfpos  8156  lt2halves  8160  addltmul  8161  avgle1  8165  avgle2  8166  div4p1lem1div2  8177  nnrecl  8179  elznn0  8260  elznn  8261  zmulcl  8297  elz2  8312  gtndiv  8335  zeo  8343  eqreznegel  8549  negm  8550  irradd  8580  irrmul  8581  divlt1lt  8650  divle1le  8651  xnegneg  8746  divelunit  8870  fzonmapblen  9043  expgt1  9293  mulexpzap  9295  leexp1a  9309  expubnd  9311  sqgt0ap  9322  lt2sq  9327  le2sq  9328  sqge0  9330  sumsqeq0  9332  bernneq  9369  bernneq2  9370  crre  9457  crim  9458  reim0  9461  mulreap  9464  rere  9465  remul2  9473  redivap  9474  immul2  9480  imdivap  9481  cjre  9482  cjreim  9503  rennim  9600  sqrt0rlem  9601  resqrexlemover  9608  absreimsq  9665  absreim  9666  absnid  9671  leabs  9672  absre  9673  absresq  9674  sqabs  9678  ltabs  9683  absdiflt  9688  absdifle  9689  lenegsq  9691  abssuble0  9699
  Copyright terms: Public domain W3C validator