Theorem 4cn 8996

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 8995	. 2 ⊢ 4 ∈ ℝ
2	1	recni 7968	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2148  ℂcc 7808  4c4 8971

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 7902  ax-1re 7904  ax-addrcl 7907

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 3135  df-ss 3142  df-2 8977  df-3 8978  df-4 8979

This theorem is referenced by:  5m1e4  9040  4p2e6  9061  4p3e7  9062  4p4e8  9063  4t2e8  9076  4d2e2  9078  8th4div3  9137  div4p1lem1div2  9171  5p5e10  9453  4t4e16  9481  6t5e30  9489  fzo0to42pr  10219  fldiv4p1lem1div2  10304  sq4e2t8  10617  sqoddm1div8  10673  4bc3eq4  10752  4bc2eq6  10753  resqrexlemover  11018  resqrexlemcalc1  11022  resqrexlemcalc3  11024  cos2bnd  11767  flodddiv4  11938  6gcd4e2  11995  6lcm4e12  12086  pythagtriplem1  12264  dveflem  14157  sincosq4sgn  14220  cosq23lt0  14224  sincos6thpi  14233  2lgsoddprmlem2  14424  2lgsoddprmlem3c  14427  2lgsoddprmlem3d  14428  ex-exp  14449  ex-fac  14450  ex-bc  14451