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

Theorem recni 7229
 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 7166 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3006 1 𝐴 ∈ ℂ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1434  ℂcc 7077  ℝcr 7078 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-resscn 7166 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2989  df-ss 2996 This theorem is referenced by:  resubcli  7474  ltapii  7836  nncni  8152  2cn  8213  3cn  8217  4cn  8220  5cn  8222  6cn  8224  7cn  8226  8cn  8228  9cn  8230  halfcn  8348  8th4div3  8353  nn0cni  8403  numltc  8619  sqge0i  9695  lt2sqi  9696  le2sqi  9697  sq11i  9698  sqrtmsq2i  10206  sqrt2irraplemnn  10748
 Copyright terms: Public domain W3C validator