Theorem 7cn 12441

Description: The number 7 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
7cn	⊢ 7 ∈ ℂ

Proof of Theorem 7cn

Step	Hyp	Ref	Expression
1		df-7 12414	. 2 ⊢ 7 = (6 + 1)
2		6cn 12438	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11262	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11319	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 7 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7421  ℂcc 11202  1c1 11205   + caddc 11207  6c6 12405  7c7 12406

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11262  ax-addcl 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-2 12409  df-3 12410  df-4 12411  df-5 12412  df-6 12413  df-7 12414

This theorem is used by:  8cn  12444  8m1e7  12479  7p2e9  12507  7p3e10  12898  7t2e14  12932  7t4e28  12934  7t7e49  12937  cos2bnd  16362  23prm  17303  83prm  17307  139prm  17308  163prm  17309  317prm  17310  631prm  17311  1259lem1  17315  1259lem2  17316  1259lem3  17317  1259lem4  17318  1259lem5  17319  1259prm  17320  2503lem1  17321  2503lem2  17322  2503lem3  17323  4001lem1  17325  4001lem4  17328  4001prm  17329  log2ublem3  27282  log2ub  27283  bclbnd  27613  bposlem8  27624  2lgslem3d  27732  ex-prmo  31066  hgt750lem  35327  hgt750lem2  35328  60lcm7e420  43154  3exp7  43197  3lexlogpow5ineq1  43198  aks4d1p1  43220  25or6to4  43350  1p8e9  43409  sq7  43447  235t711  43456  ex-decpmul  43457  3cubeslem3r  43791  fmtno5lem4  48735  257prm  48740  fmtno4nprmfac193  48753  fmtno5fac  48761  m3prm  48771  139prmALT  48775  127prm  48778  m7prm  48779  ppivalnn4  48806  2exp340mod341  48925  8exp8mod9  48928