Theorem 5cn 12269

Description: The number 5 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
5cn	⊢ 5 ∈ ℂ

Proof of Theorem 5cn

Step	Hyp	Ref	Expression
1		df-5 12247	. 2 ⊢ 5 = (4 + 1)
2		4cn 12266	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  4c4 12238  5c5 12239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245  df-4 12246  df-5 12247

This theorem is referenced by:  6cn  12272  6m1e5  12307  5p2e7  12332  5p3e8  12333  5p4e9  12334  5p5e10  12715  5t2e10  12744  5recm6rec  12787  bpoly4  16024  ef01bndlem  16151  5ndvds3  16382  5ndvds6  16383  dec5dvds  17035  dec5nprm  17037  2exp11  17060  2exp16  17061  prmlem1  17078  17prm  17087  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  log2ublem3  26912  log2ub  26913  ppiub  27167  bclbnd  27243  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  2lgslem3c  27361  2lgsoddprmlem3d  27376  ex-fac  30521  fib6  34550  hgt750lem2  34796  12lcm5e60  42447  lcmineqlem23  42490  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  sqn5i  42717  4t5e20  42723  sq5  42726  235t711  42737  ex-decpmul  42738  inductionexd  44582  cos5t  47327  goldrasin  47330  goldracos5teq  47333  goldratmolem2  47334  ceil5half3  47794  fmtno5lem1  48016  fmtno5lem2  48017  257prm  48024  fmtno4prmfac193  48036  fmtno4nprmfac193  48037  flsqrt5  48057  139prmALT  48059  127prm  48062  5tcu2e40  48078  41prothprmlem2  48081  41prothprm  48082  2exp340mod341  48209  gbpart8  48244  gpg5order  48536  linevalexample  48871  ackval3012  49168  5m4e1  50272