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

Theorem 3cn 8181
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 8180 . 2 3 ∈ ℝ
21recni 7193 1 3 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1434  cc 7041  3c3 8157
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 2064  ax-resscn 7130  ax-1re 7132  ax-addrcl 7135
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987  df-2 8165  df-3 8166
This theorem is referenced by:  3ex  8182  3m1e2  8225  3p2e5  8240  3p3e6  8241  4p4e8  8244  5p4e9  8247  3t1e3  8254  3t2e6  8255  3t3e9  8256  8th4div3  8317  halfpm6th  8318  6p4e10  8629  9t8e72  8685  fzo0to42pr  9306  sq3  9669  expnass  9677  fac3  9756  4bc3eq4  9797  3dvdsdec  10409  3dvds2dec  10410  3lcm2e6woprm  10612  ex-dvds  10718  ex-gcd  10719
  Copyright terms: Public domain W3C validator