Theorem 7cn 12275

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 12249	. 2 ⊢ 7 = (6 + 1)
2		6cn 12272	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  6c6 12240  7c7 12241

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249

This theorem is referenced by:  8cn  12278  8m1e7  12309  7p2e9  12337  7p3e10  12719  7t2e14  12753  7t4e28  12755  7t7e49  12758  cos2bnd  16155  23prm  17089  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem4  17114  4001prm  17115  log2ublem3  26912  log2ub  26913  bclbnd  27243  bposlem8  27254  2lgslem3d  27362  ex-prmo  30529  hgt750lem  34795  hgt750lem2  34796  60lcm7e420  42449  3exp7  42492  3lexlogpow5ineq1  42493  aks4d1p1  42515  sq7  42728  235t711  42737  ex-decpmul  42738  3cubeslem3r  43119  fmtno5lem4  48019  257prm  48024  fmtno4nprmfac193  48037  fmtno5fac  48045  m3prm  48055  139prmALT  48059  127prm  48062  m7prm  48063  ppivalnn4  48090  2exp340mod341  48209  8exp8mod9  48212