Theorem 3cn 9082

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

Syntax hints:   ∈ wcel 2167  ℂcc 7894  3c3 9059

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 7988  ax-1re 7990  ax-addrcl 7993

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 9066  df-3 9067

This theorem is referenced by:  3ex  9083  3m1e2  9127  4m1e3  9128  3p2e5  9149  3p3e6  9150  4p4e8  9153  5p4e9  9156  3t1e3  9163  3t2e6  9164  3t3e9  9165  8th4div3  9227  halfpm6th  9228  6p4e10  9545  9t8e72  9601  halfthird  9616  fzo0to42pr  10313  sq3  10745  expnass  10754  fac3  10841  4bc3eq4  10882  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  cos01gt0  11945  3dvdsdec  12047  3dvds2dec  12048  5ndvds3  12116  3lcm2e6woprm  12279  2exp6  12627  2exp16  12631  cosq23lt0  15153  tangtx  15158  sincos6thpi  15162  sincos3rdpi  15163  pigt3  15164  binom4  15299  lgsdir2lem1  15353  lgsdir2lem5  15357  2lgslem3b  15419  2lgslem3d  15421  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  ex-exp  15457  ex-dvds  15460  ex-gcd  15461