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

Theorem recni 7096
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 7033 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 2969 1 𝐴 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1409  cc 6944  cr 6945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-resscn 7033
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2951  df-ss 2958
This theorem is referenced by:  resubcli  7336  ltapii  7697  nncni  7999  2cn  8060  3cn  8064  4cn  8067  5cn  8069  6cn  8071  7cn  8073  8cn  8075  9cn  8077  halfcn  8195  8th4div3  8200  nn0cni  8250  numltc  8451  sqge0i  9500  lt2sqi  9501  le2sqi  9502  sq11i  9503  sqrtmsq2i  9954
  Copyright terms: Public domain W3C validator