Theorem 3cn 9181

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

Syntax hints:   ∈ wcel 2200  ℂcc 7993  3c3 9158

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9165  df-3 9166

This theorem is referenced by:  3ex  9182  3m1e2  9226  4m1e3  9227  3p2e5  9248  3p3e6  9249  4p4e8  9252  5p4e9  9255  3t1e3  9262  3t2e6  9263  3t3e9  9264  8th4div3  9326  halfpm6th  9327  6p4e10  9645  9t8e72  9701  halfthird  9716  fzo0to42pr  10421  sq3  10853  expnass  10862  fac3  10949  4bc3eq4  10990  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  cos01gt0  12269  3dvdsdec  12371  3dvds2dec  12372  5ndvds3  12440  3lcm2e6woprm  12603  2exp6  12951  2exp16  12955  cosq23lt0  15501  tangtx  15506  sincos6thpi  15510  sincos3rdpi  15511  pigt3  15512  binom4  15647  lgsdir2lem1  15701  lgsdir2lem5  15705  2lgslem3b  15767  2lgslem3d  15769  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  ex-exp  16049  ex-dvds  16052  ex-gcd  16053