Theorem 5cn 12220

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 12198	. 2 ⊢ 5 = (4 + 1)
2		4cn 12217	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11071	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11125	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2829	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   + caddc 11016  4c4 12189  5c5 12190

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 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-addcl 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-2 12195  df-3 12196  df-4 12197  df-5 12198

This theorem is referenced by:  6cn  12223  6m1e5  12258  5p2e7  12283  5p3e8  12284  5p4e9  12285  5p5e10  12665  5t2e10  12694  5recm6rec  12737  bpoly4  15968  ef01bndlem  16095  5ndvds3  16326  5ndvds6  16327  dec5dvds  16978  dec5nprm  16980  2exp11  17003  2exp16  17004  prmlem1  17021  17prm  17030  139prm  17037  163prm  17038  317prm  17039  631prm  17040  1259lem1  17044  1259lem2  17045  1259lem3  17046  1259lem4  17047  2503lem1  17050  2503lem2  17051  2503lem3  17052  4001lem1  17054  4001lem2  17055  4001lem3  17056  4001lem4  17057  4001prm  17058  log2ublem3  26886  log2ub  26887  ppiub  27143  bclbnd  27219  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem8  27230  bposlem9  27231  lgsdir2lem1  27264  2lgslem3c  27337  2lgsoddprmlem3d  27352  ex-fac  30433  fib6  34440  hgt750lem2  34686  12lcm5e60  42121  lcmineqlem23  42164  3lexlogpow5ineq1  42167  3lexlogpow5ineq5  42173  aks4d1p1p4  42184  aks4d1p1p6  42186  aks4d1p1p7  42187  sqn5i  42403  4t5e20  42409  sq5  42412  235t711  42423  ex-decpmul  42424  inductionexd  44272  ceil5half3  47464  fmtno5lem1  47677  fmtno5lem2  47678  257prm  47685  fmtno4prmfac193  47697  fmtno4nprmfac193  47698  flsqrt5  47718  139prmALT  47720  127prm  47723  5tcu2e40  47739  41prothprmlem2  47742  41prothprm  47743  2exp340mod341  47857  gbpart8  47892  gpg5order  48184  linevalexample  48520  ackval3012  48817  5m4e1  49922