Theorem 7cn 12346

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 12319	. 2 ⊢ 7 = (6 + 1)
2		6cn 12343	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11169	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11226	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 7 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7416  ℂcc 11109  1c1 11112   + caddc 11114  6c6 12310  7c7 12311

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11169  ax-addcl 11171

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12314  df-3 12315  df-4 12316  df-5 12317  df-6 12318  df-7 12319

This theorem is used by:  8cn  12349  8m1e7  12384  7p2e9  12412  7p3e10  12802  7t2e14  12836  7t4e28  12838  7t7e49  12841  cos2bnd  16261  23prm  17196  83prm  17200  139prm  17201  163prm  17202  317prm  17203  631prm  17204  1259lem1  17208  1259lem2  17209  1259lem3  17210  1259lem4  17211  1259lem5  17212  1259prm  17213  2503lem1  17214  2503lem2  17215  2503lem3  17216  4001lem1  17218  4001lem4  17221  4001prm  17222  log2ublem3  27142  log2ub  27143  bclbnd  27473  bposlem8  27484  2lgslem3d  27592  ex-prmo  30839  hgt750lem  35062  hgt750lem2  35063  60lcm7e420  42810  3exp7  42853  3lexlogpow5ineq1  42854  aks4d1p1  42876  25or6to4  43006  sq7  43090  235t711  43099  ex-decpmul  43100  3cubeslem3r  43451  fmtno5lem4  48341  257prm  48346  fmtno4nprmfac193  48359  fmtno5fac  48367  m3prm  48377  139prmALT  48381  127prm  48384  m7prm  48385  ppivalnn4  48412  2exp340mod341  48531  8exp8mod9  48534