Theorem 3cn 9084

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 9083	. 2 ⊢ 3 ∈ ℝ
2	1	recni 8057	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2167  ℂcc 7896  3c3 9061

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9068  df-3 9069

This theorem is referenced by:  3ex  9085  3m1e2  9129  4m1e3  9130  3p2e5  9151  3p3e6  9152  4p4e8  9155  5p4e9  9158  3t1e3  9165  3t2e6  9166  3t3e9  9167  8th4div3  9229  halfpm6th  9230  6p4e10  9547  9t8e72  9603  halfthird  9618  fzo0to42pr  10315  sq3  10747  expnass  10756  fac3  10843  4bc3eq4  10884  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  cos01gt0  11947  3dvdsdec  12049  3dvds2dec  12050  5ndvds3  12118  3lcm2e6woprm  12281  2exp6  12629  2exp16  12633  cosq23lt0  15177  tangtx  15182  sincos6thpi  15186  sincos3rdpi  15187  pigt3  15188  binom4  15323  lgsdir2lem1  15377  lgsdir2lem5  15381  2lgslem3b  15443  2lgslem3d  15445  2lgsoddprmlem3c  15458  2lgsoddprmlem3d  15459  ex-exp  15481  ex-dvds  15484  ex-gcd  15485