Theorem 4cn 9087

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

Syntax hints:   ∈ wcel 2167  ℂcc 7896  4c4 9062

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9068  df-3 9069  df-4 9070

This theorem is referenced by:  5m1e4  9131  4p2e6  9153  4p3e7  9154  4p4e8  9155  4t2e8  9168  4d2e2  9170  8th4div3  9229  div4p1lem1div2  9264  5p5e10  9546  4t4e16  9574  6t5e30  9582  fzo0to42pr  10315  fldiv4p1lem1div2  10414  sq4e2t8  10748  sqoddm1div8  10804  4bc3eq4  10884  4bc2eq6  10885  resqrexlemover  11194  resqrexlemcalc1  11198  resqrexlemcalc3  11200  cos2bnd  11944  flodddiv4  12120  6gcd4e2  12189  6lcm4e12  12282  pythagtriplem1  12461  2exp11  12632  dveflem  15070  sincosq4sgn  15173  cosq23lt0  15177  sincos6thpi  15186  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgsoddprmlem2  15455  2lgsoddprmlem3c  15458  2lgsoddprmlem3d  15459  ex-exp  15481  ex-fac  15482  ex-bc  15483