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

Theorem recni 7696
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1 𝐴 ∈ ℝ
Assertion
Ref Expression
recni 𝐴 ∈ ℂ

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 7631 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3058 1 𝐴 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1461  cc 7539  cr 7540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-resscn 7631
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048
This theorem is referenced by:  resubcli  7942  ltapii  8308  nncni  8634  2cn  8695  3cn  8699  4cn  8702  5cn  8704  6cn  8706  7cn  8708  8cn  8710  9cn  8712  halfcn  8832  8th4div3  8837  nn0cni  8887  numltc  9105  sqge0i  10266  lt2sqi  10267  le2sqi  10268  sq11i  10269  sqrtmsq2i  10793  0.999...  11176  ef01bndlem  11308  sin4lt0  11318  eirraplem  11325  eirr  11327  egt2lt3  11328  sqrt2irraplemnn  11696
  Copyright terms: Public domain W3C validator