Theorem 4cn 9085

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 9084	. 2 |- 4 e. RR
2	1	recni 8055	1 |- 4 e. CC

Syntax hints:   e. wcel 2167   CCcc 7894   4c4 9060

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  df-4 9068

This theorem is referenced by:  5m1e4  9129  4p2e6  9151  4p3e7  9152  4p4e8  9153  4t2e8  9166  4d2e2  9168  8th4div3  9227  div4p1lem1div2  9262  5p5e10  9544  4t4e16  9572  6t5e30  9580  fzo0to42pr  10313  fldiv4p1lem1div2  10412  sq4e2t8  10746  sqoddm1div8  10802  4bc3eq4  10882  4bc2eq6  10883  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemcalc3  11198  cos2bnd  11942  flodddiv4  12118  6gcd4e2  12187  6lcm4e12  12280  pythagtriplem1  12459  2exp11  12630  dveflem  15046  sincosq4sgn  15149  cosq23lt0  15153  sincos6thpi  15162  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgsoddprmlem2  15431  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  ex-exp  15457  ex-fac  15458  ex-bc  15459