Theorem 4cn 8999

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

Syntax hints:   e. wcel 2148   CCcc 7811   4c4 8974

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144  df-2 8980  df-3 8981  df-4 8982

This theorem is referenced by:  5m1e4  9043  4p2e6  9064  4p3e7  9065  4p4e8  9066  4t2e8  9079  4d2e2  9081  8th4div3  9140  div4p1lem1div2  9174  5p5e10  9456  4t4e16  9484  6t5e30  9492  fzo0to42pr  10222  fldiv4p1lem1div2  10307  sq4e2t8  10620  sqoddm1div8  10676  4bc3eq4  10755  4bc2eq6  10756  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemcalc3  11027  cos2bnd  11770  flodddiv4  11941  6gcd4e2  11998  6lcm4e12  12089  pythagtriplem1  12267  dveflem  14272  sincosq4sgn  14335  cosq23lt0  14339  sincos6thpi  14348  2lgsoddprmlem2  14539  2lgsoddprmlem3c  14542  2lgsoddprmlem3d  14543  ex-exp  14564  ex-fac  14565  ex-bc  14566