Theorem 4cn 9116

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

Syntax hints:   e. wcel 2176   CCcc 7925   4c4 9091

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-2 9097  df-3 9098  df-4 9099

This theorem is referenced by:  5m1e4  9160  4p2e6  9182  4p3e7  9183  4p4e8  9184  4t2e8  9197  4d2e2  9199  8th4div3  9258  div4p1lem1div2  9293  5p5e10  9576  4t4e16  9604  6t5e30  9612  fzo0to42pr  10351  fldiv4p1lem1div2  10450  sq4e2t8  10784  sqoddm1div8  10840  4bc3eq4  10920  4bc2eq6  10921  resqrexlemover  11354  resqrexlemcalc1  11358  resqrexlemcalc3  11360  cos2bnd  12104  flodddiv4  12280  6gcd4e2  12349  6lcm4e12  12442  pythagtriplem1  12621  2exp11  12792  dveflem  15231  sincosq4sgn  15334  cosq23lt0  15338  sincos6thpi  15347  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgsoddprmlem2  15616  2lgsoddprmlem3c  15619  2lgsoddprmlem3d  15620  ex-exp  15700  ex-fac  15701  ex-bc  15702