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

Theorem recn 7012
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 6974 . 2 ℝ ⊆ ℂ
21sseli 2941 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  cc 6885  cr 6886
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 6974
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  7022  recnd  7052  pnfnre  7065  mnfnre  7066  cnegexlem1  7184  cnegexlem2  7185  cnegexlem3  7186  cnegex  7187  renegcl  7270  resubcl  7273  mul02lem2  7383  ltaddsub2  7430  leaddsub2  7432  leltadd  7440  ltaddpos  7445  ltaddpos2  7446  posdif  7448  lenegcon1  7459  lenegcon2  7460  addge01  7465  addge02  7466  leaddle0  7470  mullt0  7473  recexre  7567  msqge0  7605  mulge0  7608  recexap  7632  ltm1  7810  prodgt02  7817  prodge02  7819  ltmul2  7820  lemul2  7821  lemul2a  7823  ltmulgt12  7829  lemulge12  7831  gt0div  7834  ge0div  7835  ltmuldiv2  7839  ltdivmul  7840  ltdivmul2  7842  ledivmul2  7844  lemuldiv2  7846  cju  7911  nnge1  7935  halfpos  8154  lt2halves  8158  addltmul  8159  avgle1  8163  avgle2  8164  div4p1lem1div2  8175  nnrecl  8177  elznn0  8258  elznn  8259  zmulcl  8295  elz2  8310  gtndiv  8333  zeo  8341  eqreznegel  8547  negm  8548  irradd  8578  irrmul  8579  divlt1lt  8648  divle1le  8649  xnegneg  8744  divelunit  8868  fzonmapblen  9041  expgt1  9267  mulexpzap  9269  leexp1a  9283  expubnd  9285  sqgt0ap  9296  lt2sq  9301  le2sq  9302  sqge0  9304  sumsqeq0  9306  bernneq  9343  bernneq2  9344  crre  9431  crim  9432  reim0  9435  mulreap  9438  rere  9439  remul2  9447  redivap  9448  immul2  9454  imdivap  9455  cjre  9456  cjreim  9477  rennim  9574  sqrt0rlem  9575  resqrexlemover  9582  absreimsq  9639  absreim  9640  absnid  9645  leabs  9646  absre  9647  absresq  9648  sqabs  9652  ltabs  9657  absdiflt  9662  absdifle  9663  lenegsq  9665  abssuble0  9673
  Copyright terms: Public domain W3C validator