Theorem 6cn 8916

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

Assertion

Ref	Expression
6cn	⊢ 6 ∈ ℂ

Proof of Theorem 6cn

Step	Hyp	Ref	Expression
1		6re 8915	. 2 ⊢ 6 ∈ ℝ
2	1	recni 7891	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2128  ℂcc 7731  6c6 8889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-resscn 7825  ax-1re 7827  ax-addrcl 7830

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115  df-2 8893  df-3 8894  df-4 8895  df-5 8896  df-6 8897

This theorem is referenced by:  7m1e6  8958  6p2e8  8983  6p3e9  8984  halfpm6th  9054  6p4e10  9367  6t2e12  9399  6t3e18  9400  6t5e30  9402  5recm6rec  9439  efi4p  11618  ef01bndlem  11657  cos01bnd  11659  3lcm2e6woprm  11967  6lcm4e12  11968  sincos6thpi  13205  sincos3rdpi  13206  ex-exp  13345  ex-bc  13347  ex-gcd  13349