Theorem 5cn 12250

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 12228	. 2 ⊢ 5 = (4 + 1)
2		4cn 12247	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11118	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11170	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2828	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058  1c1 11061   + caddc 11063  4c4 12219  5c5 12220

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-addcl 11120

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-2 12225  df-3 12226  df-4 12227  df-5 12228

This theorem is referenced by:  6cn  12253  6m1e5  12293  5p2e7  12318  5p3e8  12319  5p4e9  12320  5p5e10  12698  5t2e10  12727  5recm6rec  12771  bpoly4  15953  ef01bndlem  16077  dec5dvds  16947  dec5nprm  16949  2exp11  16973  2exp16  16974  prmlem1  16991  17prm  17000  139prm  17007  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem3  17016  1259lem4  17017  2503lem1  17020  2503lem2  17021  2503lem3  17022  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001lem4  17027  4001prm  17028  log2ublem3  26335  log2ub  26336  ppiub  26589  bclbnd  26665  bposlem4  26672  bposlem5  26673  bposlem6  26674  bposlem8  26676  bposlem9  26677  lgsdir2lem1  26710  2lgslem3c  26783  2lgsoddprmlem3d  26798  ex-fac  29458  fib6  33095  hgt750lem2  33354  12lcm5e60  40538  lcmineqlem23  40581  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1p4  40601  aks4d1p1p6  40603  aks4d1p1p7  40604  sqn5i  40857  235t711  40863  ex-decpmul  40864  inductionexd  42549  fmtno5lem1  45865  fmtno5lem2  45866  257prm  45873  fmtno4prmfac193  45885  fmtno4nprmfac193  45886  flsqrt5  45906  139prmALT  45908  127prm  45911  5tcu2e40  45927  41prothprmlem2  45930  41prothprm  45931  2exp340mod341  46045  gbpart8  46080  linevalexample  46596  ackval3012  46898  5m4e1  47364