Theorem 5cn 11726

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 11704	. 2 ⊢ 5 = (4 + 1)
2		4cn 11723	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 10595	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10647	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535  1c1 10538   + caddc 10540  4c4 11695  5c5 11696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-2 11701  df-3 11702  df-4 11703  df-5 11704

This theorem is referenced by:  6cn  11729  6m1e5  11769  5p2e7  11794  5p3e8  11795  5p4e9  11796  5p5e10  12170  5t2e10  12199  5recm6rec  12243  bpoly4  15413  ef01bndlem  15537  dec5dvds  16400  dec5nprm  16402  2exp16  16424  prmlem1  16441  17prm  16450  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  2503lem1  16470  2503lem2  16471  2503lem3  16472  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  log2ublem3  25526  log2ub  25527  ppiub  25780  bclbnd  25856  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem8  25867  bposlem9  25868  lgsdir2lem1  25901  2lgslem3c  25974  2lgsoddprmlem3d  25989  ex-fac  28230  fib6  31664  hgt750lem2  31923  sqn5i  39191  235t711  39197  ex-decpmul  39198  inductionexd  40525  fmtno5lem1  43735  fmtno5lem2  43736  257prm  43743  fmtno4prmfac193  43755  fmtno4nprmfac193  43756  flsqrt5  43777  139prmALT  43779  127prm  43783  2exp11  43785  5tcu2e40  43800  41prothprmlem2  43803  41prothprm  43804  2exp340mod341  43918  gbpart8  43953  linevalexample  44470  5m4e1  44918