Theorem 3cn 9379

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

Assertion

Ref	Expression
3cn	|- 3 e. CC

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 9378	. 2 |- 3 e. RR
2	1	recni 8338	1 |- 3 e. CC

This proof depends on syntax axioms:   e. wcel 2209   CCcc 8177   3c3 9356

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9363  df-3 9364

This theorem is used by:  3ex  9380  3m1e2  9424  4m1e3  9425  3p2e5  9446  3p3e6  9447  4p4e8  9450  5p4e9  9453  3t1e3  9460  3t2e6  9461  3t3e9  9462  8th4div3  9524  halfpm6th  9525  6p4e10  9848  9t8e72  9904  halfthird  9919  fzo0to42pr  10638  sq3  11073  expnass  11082  fac3  11170  4bc3eq4  11212  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  cos01gt0  12530  3dvdsdec  12632  3dvds2dec  12633  5ndvds3  12701  3lcm2e6woprm  12864  2exp6  13212  2exp16  13216  cosq23lt0  15934  tangtx  15939  sincos6thpi  15943  sincos3rdpi  15944  pigt3  15945  binom4  16081  log2tlbndlog2  16082  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  lgsdir2lem1  16147  lgsdir2lem5  16151  2lgslem3b  16213  2lgslem3d  16215  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  ex-exp  16741  ex-dvds  16744  ex-gcd  16745