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

Theorem 3cn 8818
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 8817 . 2  |-  3  e.  RR
21recni 7801 1  |-  3  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1481   CCcc 7641   3c3 8795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7735  ax-1re 7737  ax-addrcl 7740
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3081  df-ss 3088  df-2 8802  df-3 8803
This theorem is referenced by:  3ex  8819  3m1e2  8863  4m1e3  8864  3p2e5  8884  3p3e6  8885  4p4e8  8888  5p4e9  8891  3t1e3  8898  3t2e6  8899  3t3e9  8900  8th4div3  8962  halfpm6th  8963  6p4e10  9276  9t8e72  9332  halfthird  9347  fzo0to42pr  10027  sq3  10419  expnass  10428  fac3  10509  4bc3eq4  10550  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos1bnd  11500  cos2bnd  11501  cos01gt0  11503  3dvdsdec  11596  3dvds2dec  11597  3lcm2e6woprm  11801  cosq23lt0  12960  tangtx  12965  sincos6thpi  12969  sincos3rdpi  12970  pigt3  12971  ex-exp  13108  ex-dvds  13111  ex-gcd  13112
  Copyright terms: Public domain W3C validator