Theorem 4cn 9062

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

Syntax hints:   e. wcel 2164   CCcc 7872   4c4 9037

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167  df-2 9043  df-3 9044  df-4 9045

This theorem is referenced by:  5m1e4  9106  4p2e6  9128  4p3e7  9129  4p4e8  9130  4t2e8  9143  4d2e2  9145  8th4div3  9204  div4p1lem1div2  9239  5p5e10  9521  4t4e16  9549  6t5e30  9557  fzo0to42pr  10290  fldiv4p1lem1div2  10377  sq4e2t8  10711  sqoddm1div8  10767  4bc3eq4  10847  4bc2eq6  10848  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemcalc3  11163  cos2bnd  11906  flodddiv4  12078  6gcd4e2  12135  6lcm4e12  12228  pythagtriplem1  12406  dveflem  14905  sincosq4sgn  15005  cosq23lt0  15009  sincos6thpi  15018  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgsoddprmlem2  15263  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  ex-exp  15289  ex-fac  15290  ex-bc  15291