Theorem 5cn 12355

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 12333	. 2 ⊢ 5 = (4 + 1)
2		4cn 12352	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11214	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11268	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154  1c1 11157   + caddc 11159  4c4 12324  5c5 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-1cn 11214  ax-addcl 11216

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-clel 2815  df-2 12330  df-3 12331  df-4 12332  df-5 12333

This theorem is referenced by:  6cn  12358  6m1e5  12398  5p2e7  12423  5p3e8  12424  5p4e9  12425  5p5e10  12806  5t2e10  12835  5recm6rec  12878  bpoly4  16096  ef01bndlem  16221  5ndvds3  16451  5ndvds6  16452  dec5dvds  17103  dec5nprm  17105  2exp11  17128  2exp16  17129  prmlem1  17146  17prm  17155  139prm  17162  163prm  17163  317prm  17164  631prm  17165  1259lem1  17169  1259lem2  17170  1259lem3  17171  1259lem4  17172  2503lem1  17175  2503lem2  17176  2503lem3  17177  4001lem1  17179  4001lem2  17180  4001lem3  17181  4001lem4  17182  4001prm  17183  log2ublem3  26992  log2ub  26993  ppiub  27249  bclbnd  27325  bposlem4  27332  bposlem5  27333  bposlem6  27334  bposlem8  27336  bposlem9  27337  lgsdir2lem1  27370  2lgslem3c  27443  2lgsoddprmlem3d  27458  ex-fac  30471  fib6  34409  hgt750lem2  34668  12lcm5e60  42010  lcmineqlem23  42053  3lexlogpow5ineq1  42056  3lexlogpow5ineq5  42062  aks4d1p1p4  42073  aks4d1p1p6  42075  aks4d1p1p7  42076  sqn5i  42325  4t5e20  42331  sq5  42333  235t711  42344  ex-decpmul  42345  inductionexd  44173  ceil5half3  47347  fmtno5lem1  47545  fmtno5lem2  47546  257prm  47553  fmtno4prmfac193  47565  fmtno4nprmfac193  47566  flsqrt5  47586  139prmALT  47588  127prm  47591  5tcu2e40  47607  41prothprmlem2  47610  41prothprm  47611  2exp340mod341  47725  gbpart8  47760  gpg5order  48019  linevalexample  48317  ackval3012  48618  5m4e1  49371