Theorem 4cn 9184

Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
4cn	⊢ 4 ∈ ℂ

Proof of Theorem 4cn

Step	Hyp	Ref	Expression
1		4re 9183	. 2 ⊢ 4 ∈ ℝ
2	1	recni 8154	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2200  ℂcc 7993  4c4 9159

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 8087  ax-1re 8089  ax-addrcl 8092

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 9165  df-3 9166  df-4 9167

This theorem is referenced by:  5m1e4  9228  4p2e6  9250  4p3e7  9251  4p4e8  9252  4t2e8  9265  4d2e2  9267  8th4div3  9326  div4p1lem1div2  9361  5p5e10  9644  4t4e16  9672  6t5e30  9680  fzo0to42pr  10421  fldiv4p1lem1div2  10520  sq4e2t8  10854  sqoddm1div8  10910  4bc3eq4  10990  4bc2eq6  10991  resqrexlemover  11516  resqrexlemcalc1  11520  resqrexlemcalc3  11522  cos2bnd  12266  flodddiv4  12442  6gcd4e2  12511  6lcm4e12  12604  pythagtriplem1  12783  2exp11  12954  dveflem  15394  sincosq4sgn  15497  cosq23lt0  15501  sincos6thpi  15510  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgsoddprmlem2  15779  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  ex-exp  16049  ex-fac  16050  ex-bc  16051