Theorem 8cn 11269

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

Assertion

Ref	Expression
8cn	⊢ 8 ∈ ℂ

Proof of Theorem 8cn

Step	Hyp	Ref	Expression
1		8re 11268	. 2 ⊢ 8 ∈ ℝ
2	1	recni 10215	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2127  ℂcc 10097  8c8 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-i2m1 10167  ax-1ne0 10168  ax-rrecex 10171  ax-cnre 10172

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804  df-2 11242  df-3 11243  df-4 11244  df-5 11245  df-6 11246  df-7 11247  df-8 11248

This theorem is referenced by:  9m1e8  11306  8p2e10OLD  11337  8p2e10  11773  8t2e16  11817  8t5e40  11820  8t5e40OLD  11821  cos2bnd  15088  2exp16  15970  139prm  16004  163prm  16005  317prm  16006  631prm  16007  1259lem2  16012  1259lem3  16013  1259lem4  16014  1259lem5  16015  2503lem2  16018  2503lem3  16019  2503prm  16020  4001lem1  16021  4001lem2  16022  4001prm  16025  quart1cl  24751  quart1lem  24752  quart1  24753  quartlem1  24754  log2tlbnd  24842  log2ublem3  24845  log2ub  24846  bposlem8  25186  lgsdir2lem1  25220  lgsdir2lem3  25222  lgsdir2lem5  25224  2lgslem3a  25291  2lgslem3b  25292  2lgslem3c  25293  2lgslem3d  25294  2lgslem3a1  25295  2lgslem3b1  25296  2lgslem3c1  25297  2lgslem3d1  25298  2lgsoddprmlem1  25303  2lgsoddprmlem2  25304  2lgsoddprmlem3a  25305  2lgsoddprmlem3b  25306  2lgsoddprmlem3c  25307  2lgsoddprmlem3d  25308  ex-exp  27589  hgt750lem2  31010  fmtno5lem4  41947  257prm  41952  fmtnoprmfac2lem1  41957  fmtno4prmfac  41963  fmtno4nprmfac193  41965  fmtno5faclem3  41972  m3prm  41985  139prmALT  41990  127prm  41994  m7prm  41995  2exp11  41996  5tcu2e40  42011  evengpop3  42165  tgoldbachlt  42183  tgoldbachltOLD  42189