Theorem 7cn 12302

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 12276	. 2 ⊢ 7 = (6 + 1)
2		6cn 12299	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11216	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2829	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  1c1 11107   + caddc 11109  6c6 12267  7c7 12268

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 2703  ax-1cn 11164  ax-addcl 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276

This theorem is referenced by:  8cn  12305  8m1e7  12341  7p2e9  12369  7p3e10  12748  7t2e14  12782  7t4e28  12784  7t7e49  12787  cos2bnd  16127  23prm  17048  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem4  17073  4001prm  17074  log2ublem3  26442  log2ub  26443  bclbnd  26772  bposlem8  26783  2lgslem3d  26891  ex-prmo  29701  hgt750lem  33651  hgt750lem2  33652  60lcm7e420  40863  3exp7  40906  3lexlogpow5ineq1  40907  aks4d1p1  40929  235t711  41200  ex-decpmul  41201  3cubeslem3r  41410  fmtno5lem4  46210  257prm  46215  fmtno4nprmfac193  46228  fmtno5fac  46236  m3prm  46246  139prmALT  46250  127prm  46253  m7prm  46254  2exp340mod341  46387  8exp8mod9  46390