Theorem 8cn 9093

Description: The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
8cn	|- 8 e. CC

Proof of Theorem 8cn

Step	Hyp	Ref	Expression
1		8re 9092	. 2 |- 8 e. RR
2	1	recni 8055	1 |- 8 e. CC

Syntax hints:   e. wcel 2167   CCcc 7894   8c8 9064

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 7988  ax-1re 7990  ax-addrcl 7993

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 9066  df-3 9067  df-4 9068  df-5 9069  df-6 9070  df-7 9071  df-8 9072

This theorem is referenced by:  9m1e8  9133  8p2e10  9553  8t2e16  9588  8t5e40  9591  cos2bnd  11942  2exp11  12630  2exp16  12631  lgsdir2lem1  15353  lgsdir2lem5  15357  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgsoddprmlem1  15430  2lgsoddprmlem2  15431  2lgsoddprmlem3a  15432  2lgsoddprmlem3b  15433  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  ex-exp  15457