Theorem 5cn 9228

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 9227	. 2 ⊢ 5 ∈ ℝ
2	1	recni 8196	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2201  ℂcc 8035  5c5 9202

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 2212  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212  df-2 9207  df-3 9208  df-4 9209  df-5 9210

This theorem is referenced by:  6m1e5  9271  5p2e7  9295  5p3e8  9296  5p4e9  9297  5p5e10  9686  5t2e10  9715  5recm6rec  9759  ef01bndlem  12340  5ndvds3  12518  5ndvds6  12519  dec5dvds  13008  dec5nprm  13010  2exp11  13032  2exp16  13033  lgsdir2lem1  15786  2lgslem3c  15853  2lgsoddprmlem3d  15868  ex-fac  16381