Theorem 5cn 9213

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

Assertion

Ref	Expression
5cn	|- 5 e. CC

Proof of Theorem 5cn

Step	Hyp	Ref	Expression
1		5re 9212	. 2 |- 5 e. RR
2	1	recni 8181	1 |- 5 e. CC

Syntax hints:   e. wcel 2200   CCcc 8020   5c5 9187

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 8114  ax-1re 8116  ax-addrcl 8119

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 3204  df-ss 3211  df-2 9192  df-3 9193  df-4 9194  df-5 9195

This theorem is referenced by:  6m1e5  9256  5p2e7  9280  5p3e8  9281  5p4e9  9282  5p5e10  9671  5t2e10  9700  5recm6rec  9744  ef01bndlem  12307  5ndvds3  12485  5ndvds6  12486  dec5dvds  12975  dec5nprm  12977  2exp11  12999  2exp16  13000  lgsdir2lem1  15747  2lgslem3c  15814  2lgsoddprmlem3d  15829  ex-fac  16260