Theorem 7cn 12336

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 12309	. 2 ⊢ 7 = (6 + 1)
2		6cn 12333	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11159	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11216	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   + caddc 11104  6c6 12300  7c7 12301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addcl 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12304  df-3 12305  df-4 12306  df-5 12307  df-6 12308  df-7 12309

This theorem is referenced by:  8cn  12339  8m1e7  12374  7p2e9  12402  7p3e10  12792  7t2e14  12826  7t4e28  12828  7t7e49  12831  cos2bnd  16245  23prm  17180  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem1  17198  2503lem2  17199  2503lem3  17200  4001lem1  17202  4001lem4  17205  4001prm  17206  log2ublem3  27094  log2ub  27095  bclbnd  27425  bposlem8  27436  2lgslem3d  27544  ex-prmo  30791  hgt750lem  35019  hgt750lem2  35020  60lcm7e420  42758  3exp7  42801  3lexlogpow5ineq1  42802  aks4d1p1  42824  25or6to4  42954  sq7  43038  235t711  43047  ex-decpmul  43048  3cubeslem3r  43401  fmtno5lem4  48291  257prm  48296  fmtno4nprmfac193  48309  fmtno5fac  48317  m3prm  48327  139prmALT  48331  127prm  48334  m7prm  48335  ppivalnn4  48362  2exp340mod341  48481  8exp8mod9  48484