Theorem 5cn 12205

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 12183	. 2 ⊢ 5 = (4 + 1)
2		4cn 12202	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11056	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11110	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996  1c1 10999   + caddc 11001  4c4 12174  5c5 12175

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-1cn 11056  ax-addcl 11058

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-clel 2804  df-2 12180  df-3 12181  df-4 12182  df-5 12183

This theorem is referenced by:  6cn  12208  6m1e5  12243  5p2e7  12268  5p3e8  12269  5p4e9  12270  5p5e10  12651  5t2e10  12680  5recm6rec  12723  bpoly4  15958  ef01bndlem  16085  5ndvds3  16316  5ndvds6  16317  dec5dvds  16968  dec5nprm  16970  2exp11  16993  2exp16  16994  prmlem1  17011  17prm  17020  139prm  17027  163prm  17028  317prm  17029  631prm  17030  1259lem1  17034  1259lem2  17035  1259lem3  17036  1259lem4  17037  2503lem1  17040  2503lem2  17041  2503lem3  17042  4001lem1  17044  4001lem2  17045  4001lem3  17046  4001lem4  17047  4001prm  17048  log2ublem3  26878  log2ub  26879  ppiub  27135  bclbnd  27211  bposlem4  27218  bposlem5  27219  bposlem6  27220  bposlem8  27222  bposlem9  27223  lgsdir2lem1  27256  2lgslem3c  27329  2lgsoddprmlem3d  27344  ex-fac  30421  fib6  34409  hgt750lem2  34655  12lcm5e60  42020  lcmineqlem23  42063  3lexlogpow5ineq1  42066  3lexlogpow5ineq5  42072  aks4d1p1p4  42083  aks4d1p1p6  42085  aks4d1p1p7  42086  sqn5i  42297  4t5e20  42303  sq5  42306  235t711  42317  ex-decpmul  42318  inductionexd  44167  ceil5half3  47350  fmtno5lem1  47563  fmtno5lem2  47564  257prm  47571  fmtno4prmfac193  47583  fmtno4nprmfac193  47584  flsqrt5  47604  139prmALT  47606  127prm  47609  5tcu2e40  47625  41prothprmlem2  47628  41prothprm  47629  2exp340mod341  47743  gbpart8  47778  gpg5order  48070  linevalexample  48406  ackval3012  48703  5m4e1  49808