Theorem 5cn 12352

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 12330	. 2 ⊢ 5 = (4 + 1)
2		4cn 12349	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11211	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11265	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151  1c1 11154   + caddc 11156  4c4 12321  5c5 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814  df-2 12327  df-3 12328  df-4 12329  df-5 12330

This theorem is referenced by:  6cn  12355  6m1e5  12395  5p2e7  12420  5p3e8  12421  5p4e9  12422  5p5e10  12802  5t2e10  12831  5recm6rec  12875  bpoly4  16092  ef01bndlem  16217  5ndvds3  16447  5ndvds6  16448  dec5dvds  17098  dec5nprm  17100  2exp11  17124  2exp16  17125  prmlem1  17142  17prm  17151  139prm  17158  163prm  17159  317prm  17160  631prm  17161  1259lem1  17165  1259lem2  17166  1259lem3  17167  1259lem4  17168  2503lem1  17171  2503lem2  17172  2503lem3  17173  4001lem1  17175  4001lem2  17176  4001lem3  17177  4001lem4  17178  4001prm  17179  log2ublem3  27006  log2ub  27007  ppiub  27263  bclbnd  27339  bposlem4  27346  bposlem5  27347  bposlem6  27348  bposlem8  27350  bposlem9  27351  lgsdir2lem1  27384  2lgslem3c  27457  2lgsoddprmlem3d  27472  ex-fac  30480  fib6  34388  hgt750lem2  34646  12lcm5e60  41990  lcmineqlem23  42033  3lexlogpow5ineq1  42036  3lexlogpow5ineq5  42042  aks4d1p1p4  42053  aks4d1p1p6  42055  aks4d1p1p7  42056  sqn5i  42299  4t5e20  42305  sq5  42307  235t711  42318  ex-decpmul  42319  inductionexd  44145  ceil5half3  47280  fmtno5lem1  47478  fmtno5lem2  47479  257prm  47486  fmtno4prmfac193  47498  fmtno4nprmfac193  47499  flsqrt5  47519  139prmALT  47521  127prm  47524  5tcu2e40  47540  41prothprmlem2  47543  41prothprm  47544  2exp340mod341  47658  gbpart8  47693  gpg5order  47949  linevalexample  48241  ackval3012  48542  5m4e1  49028