Theorem 4cn 9199

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

Syntax hints:   e. wcel 2200   CCcc 8008   4c4 9174

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 8102  ax-1re 8104  ax-addrcl 8107

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 9180  df-3 9181  df-4 9182

This theorem is referenced by:  5m1e4  9243  4p2e6  9265  4p3e7  9266  4p4e8  9267  4t2e8  9280  4d2e2  9282  8th4div3  9341  div4p1lem1div2  9376  5p5e10  9659  4t4e16  9687  6t5e30  9695  fzo0to42pr  10438  fldiv4p1lem1div2  10537  sq4e2t8  10871  sqoddm1div8  10927  4bc3eq4  11007  4bc2eq6  11008  resqrexlemover  11537  resqrexlemcalc1  11541  resqrexlemcalc3  11543  cos2bnd  12287  flodddiv4  12463  6gcd4e2  12532  6lcm4e12  12625  pythagtriplem1  12804  2exp11  12975  dveflem  15416  sincosq4sgn  15519  cosq23lt0  15523  sincos6thpi  15532  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgsoddprmlem2  15801  2lgsoddprmlem3c  15804  2lgsoddprmlem3d  15805  ex-exp  16174  ex-fac  16175  ex-bc  16176