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

Theorem 3cn 8035
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
Assertion
Ref Expression
3cn 3 ∈ ℂ

Proof of Theorem 3cn
StepHypRef Expression
1 3re 8034 . 2 3 ∈ ℝ
21recni 7067 1 3 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1407  cc 6915  3c3 8011
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 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-11 1411  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-resscn 7004  ax-1re 7006  ax-addrcl 7009
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-in 2949  df-ss 2956  df-2 8019  df-3 8020
This theorem is referenced by:  3ex  8036  3m1e2  8079  3p2e5  8094  3p3e6  8095  4p4e8  8098  5p4e9  8101  3t1e3  8108  3t2e6  8109  3t3e9  8110  8th4div3  8171  halfpm6th  8172  6p4e10  8468  9t8e72  8524  fzo0to42pr  9148  sq3  9481  expnass  9488  fac3  9564  4bc3eq4  9605  3dvdsdec  10139  3dvds2dec  10140  ex-dvds  10226
  Copyright terms: Public domain W3C validator