Theorem 5cn 9223

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

Assertion

Ref	Expression
5cn	⊢ 5 ∈ ℂ

Proof of Theorem 5cn

Step	Hyp	Ref	Expression
1		5re 9222	. 2 ⊢ 5 ∈ ℝ
2	1	recni 8191	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2202  ℂcc 8030  5c5 9197

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-2 9202  df-3 9203  df-4 9204  df-5 9205

This theorem is referenced by:  6m1e5  9266  5p2e7  9290  5p3e8  9291  5p4e9  9292  5p5e10  9681  5t2e10  9710  5recm6rec  9754  ef01bndlem  12319  5ndvds3  12497  5ndvds6  12498  dec5dvds  12987  dec5nprm  12989  2exp11  13011  2exp16  13012  lgsdir2lem1  15760  2lgslem3c  15827  2lgsoddprmlem3d  15842  ex-fac  16341