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

Theorem 3cn 8435
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 8434 . 2 3 ∈ ℝ
21recni 7447 1 3 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1436  cc 7295  3c3 8411
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 7384  ax-1re 7386  ax-addrcl 7389
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 8419  df-3 8420
This theorem is referenced by:  3ex  8436  3m1e2  8479  3p2e5  8494  3p3e6  8495  4p4e8  8498  5p4e9  8501  3t1e3  8508  3t2e6  8509  3t3e9  8510  8th4div3  8571  halfpm6th  8572  6p4e10  8883  9t8e72  8939  fzo0to42pr  9562  sq3  9971  expnass  9979  fac3  10058  4bc3eq4  10099  3dvdsdec  10790  3dvds2dec  10791  3lcm2e6woprm  10993  ex-dvds  11145  ex-gcd  11146
  Copyright terms: Public domain W3C validator