Theorem 4cn 9188

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

Syntax hints:   e. wcel 2200   CCcc 7997   4c4 9163

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 8091  ax-1re 8093  ax-addrcl 8096

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 9169  df-3 9170  df-4 9171

This theorem is referenced by:  5m1e4  9232  4p2e6  9254  4p3e7  9255  4p4e8  9256  4t2e8  9269  4d2e2  9271  8th4div3  9330  div4p1lem1div2  9365  5p5e10  9648  4t4e16  9676  6t5e30  9684  fzo0to42pr  10426  fldiv4p1lem1div2  10525  sq4e2t8  10859  sqoddm1div8  10915  4bc3eq4  10995  4bc2eq6  10996  resqrexlemover  11521  resqrexlemcalc1  11525  resqrexlemcalc3  11527  cos2bnd  12271  flodddiv4  12447  6gcd4e2  12516  6lcm4e12  12609  pythagtriplem1  12788  2exp11  12959  dveflem  15400  sincosq4sgn  15503  cosq23lt0  15507  sincos6thpi  15516  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgsoddprmlem2  15785  2lgsoddprmlem3c  15788  2lgsoddprmlem3d  15789  ex-exp  16091  ex-fac  16092  ex-bc  16093