Theorem 8cn 11144

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 11143	. 2 ⊢ 8 ∈ ℝ
2	1	recni 10090	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2030  ℂcc 9972  8c8 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123

This theorem is referenced by:  9m1e8  11181  8p2e10OLD  11212  8p2e10  11648  8t2e16  11692  8t5e40  11695  8t5e40OLD  11696  cos2bnd  14962  2exp16  15844  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001prm  15899  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem1  24629  log2tlbnd  24717  log2ublem3  24720  log2ub  24721  bposlem8  25061  lgsdir2lem1  25095  lgsdir2lem3  25097  lgsdir2lem5  25099  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  2lgsoddprmlem1  25178  2lgsoddprmlem2  25179  2lgsoddprmlem3a  25180  2lgsoddprmlem3b  25181  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  ex-exp  27437  hgt750lem2  30858  fmtno5lem4  41793  257prm  41798  fmtnoprmfac2lem1  41803  fmtno4prmfac  41809  fmtno4nprmfac193  41811  fmtno5faclem3  41818  m3prm  41831  139prmALT  41836  127prm  41840  m7prm  41841  2exp11  41842  5tcu2e40  41857  evengpop3  42011  tgoldbachlt  42029  tgoldbachltOLD  42035