Theorem 4cn 8970

Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
4cn	|- 4 e. CC

Proof of Theorem 4cn

Step	Hyp	Ref	Expression
1		4re 8969	. 2 |- 4 e. RR
2	1	recni 7944	1 |- 4 e. CC

Syntax hints:   e. wcel 2146   CCcc 7784   4c4 8945

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140  df-2 8951  df-3 8952  df-4 8953

This theorem is referenced by:  5m1e4  9014  4p2e6  9035  4p3e7  9036  4p4e8  9037  4t2e8  9050  4d2e2  9052  8th4div3  9111  div4p1lem1div2  9145  5p5e10  9427  4t4e16  9455  6t5e30  9463  fzo0to42pr  10190  fldiv4p1lem1div2  10275  sq4e2t8  10587  sqoddm1div8  10643  4bc3eq4  10721  4bc2eq6  10722  resqrexlemover  10987  resqrexlemcalc1  10991  resqrexlemcalc3  10993  cos2bnd  11736  flodddiv4  11906  6gcd4e2  11963  6lcm4e12  12054  pythagtriplem1  12232  dveflem  13758  sincosq4sgn  13821  cosq23lt0  13825  sincos6thpi  13834  ex-exp  14039  ex-fac  14040  ex-bc  14041