Theorem 5cn 12458

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 12435	. 2 ⊢ 5 = (4 + 1)
2		4cn 12455	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11285	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11342	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2860	1 ⊢ 5 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   + caddc 11230  4c4 12426  5c5 12427

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285  ax-addcl 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-2 12432  df-3 12433  df-4 12434  df-5 12435

This theorem is used by:  6cn  12461  6m1e5  12500  5p2e7  12525  5p3e8  12526  5p4e9  12527  5p5e10  12917  5t2e10  12946  5recm6rec  12991  bpoly4  16254  ef01bndlem  16381  5ndvds3  16612  5ndvds6  16613  dec5dvds  17271  dec5nprm  17273  2exp11  17296  2exp16  17297  prmlem1  17314  17prm  17324  139prm  17331  163prm  17332  317prm  17333  631prm  17334  1259lem1  17338  1259lem2  17339  1259lem3  17340  1259lem4  17341  2503lem1  17344  2503lem2  17345  2503lem3  17346  4001lem1  17348  4001lem2  17349  4001lem3  17350  4001lem4  17351  4001prm  17352  log2ublem3  27306  log2ub  27307  ppiub  27561  bclbnd  27637  bposlem4  27644  bposlem5  27645  bposlem6  27646  bposlem8  27648  bposlem9  27649  lgsdir2lem1  27682  2lgslem3c  27755  2lgsoddprmlem3d  27770  ex-fac  31082  fib6  35108  hgt750lem2  35351  12lcm5e60  43250  lcmineqlem23  43293  3lexlogpow5ineq1  43296  3lexlogpow5ineq5  43302  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  25or6to4  43448  1p6e7  43506  2p7e9  43513  sqn5i  43535  4t5e20  43541  sq5  43544  235t711  43555  ex-decpmul  43556  inductionexd  45347  cos5t  48130  goldrasin  48134  goldracos5teq  48137  goldratmolem2  48138  goldratmolem3  48139  ceil5half3  48621  fmtno5lem1  48843  fmtno5lem2  48844  257prm  48851  fmtno4prmfac193  48863  fmtno4nprmfac193  48864  flsqrt5  48884  139prmALT  48886  127prm  48889  5tcu2e40  48905  41prothprmlem2  48908  41prothprm  48909  2exp340mod341  49036  gbpart8  49071  gpg5order  49363  linevalexample  49712  ackval3012  50009  5m4e1  51215