ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3cn Unicode version

Theorem 3cn 8432
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
Assertion
Ref Expression
3cn  |-  3  e.  CC

Proof of Theorem 3cn
StepHypRef Expression
1 3re 8431 . 2  |-  3  e.  RR
21recni 7444 1  |-  3  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1436   CCcc 7292   3c3 8408
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-resscn 7381  ax-1re 7383  ax-addrcl 7386
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001  df-2 8416  df-3 8417
This theorem is referenced by:  3ex  8433  3m1e2  8476  3p2e5  8491  3p3e6  8492  4p4e8  8495  5p4e9  8498  3t1e3  8505  3t2e6  8506  3t3e9  8507  8th4div3  8568  halfpm6th  8569  6p4e10  8880  9t8e72  8936  fzo0to42pr  9559  sq3  9949  expnass  9957  fac3  10036  4bc3eq4  10077  3dvdsdec  10740  3dvds2dec  10741  3lcm2e6woprm  10943  ex-dvds  11095  ex-gcd  11096
  Copyright terms: Public domain W3C validator