Theorem 6cn 9003

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 9002	. 2 ⊢ 6 ∈ ℝ
2	1	recni 7971	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2148  ℂcc 7811  6c6 8976

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144  df-2 8980  df-3 8981  df-4 8982  df-5 8983  df-6 8984

This theorem is referenced by:  7m1e6  9045  6p2e8  9070  6p3e9  9071  halfpm6th  9141  6p4e10  9457  6t2e12  9489  6t3e18  9490  6t5e30  9492  5recm6rec  9529  efi4p  11727  ef01bndlem  11766  cos01bnd  11768  3lcm2e6woprm  12088  6lcm4e12  12089  sincos6thpi  14348  sincos3rdpi  14349  2lgsoddprmlem3d  14543  ex-exp  14564  ex-bc  14566  ex-gcd  14568