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

Theorem 3cn 8752
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 8751 . 2 3 ∈ ℝ
21recni 7742 1 3 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1463  cc 7582  3c3 8729
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-resscn 7676  ax-1re 7678  ax-addrcl 7681
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052  df-2 8736  df-3 8737
This theorem is referenced by:  3ex  8753  3m1e2  8797  3p2e5  8812  3p3e6  8813  4p4e8  8816  5p4e9  8819  3t1e3  8826  3t2e6  8827  3t3e9  8828  8th4div3  8890  halfpm6th  8891  6p4e10  9204  9t8e72  9260  fzo0to42pr  9937  sq3  10329  expnass  10338  fac3  10418  4bc3eq4  10459  ef01bndlem  11362  sin01bnd  11363  cos01bnd  11364  cos1bnd  11365  cos2bnd  11366  cos01gt0  11368  3dvdsdec  11458  3dvds2dec  11459  3lcm2e6woprm  11663  ex-exp  12741  ex-dvds  12744  ex-gcd  12745
  Copyright terms: Public domain W3C validator