Theorem 3cn 9059

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)

Assertion

Ref	Expression
3cn	⊢ 3 ∈ ℂ

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 9058	. 2 ⊢ 3 ∈ ℝ
2	1	recni 8033	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2164  ℂcc 7872  3c3 9036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167  df-2 9043  df-3 9044

This theorem is referenced by:  3ex  9060  3m1e2  9104  4m1e3  9105  3p2e5  9126  3p3e6  9127  4p4e8  9130  5p4e9  9133  3t1e3  9140  3t2e6  9141  3t3e9  9142  8th4div3  9204  halfpm6th  9205  6p4e10  9522  9t8e72  9578  halfthird  9593  fzo0to42pr  10290  sq3  10710  expnass  10719  fac3  10806  4bc3eq4  10847  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  cos01gt0  11909  3dvdsdec  12009  3dvds2dec  12010  3lcm2e6woprm  12227  cosq23lt0  15009  tangtx  15014  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  binom4  15152  lgsdir2lem1  15185  lgsdir2lem5  15189  2lgslem3b  15251  2lgslem3d  15253  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  ex-exp  15289  ex-dvds  15292  ex-gcd  15293