Theorem 7cn 12251

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 12225	. 2 ⊢ 7 = (6 + 1)
2		6cn 12248	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  6c6 12216  7c7 12217

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 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225

This theorem is referenced by:  8cn  12254  8m1e7  12285  7p2e9  12313  7p3e10  12694  7t2e14  12728  7t4e28  12730  7t7e49  12733  cos2bnd  16125  23prm  17058  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem4  17083  4001prm  17084  log2ublem3  26926  log2ub  26927  bclbnd  27259  bposlem8  27270  2lgslem3d  27378  ex-prmo  30546  hgt750lem  34828  hgt750lem2  34829  60lcm7e420  42377  3exp7  42420  3lexlogpow5ineq1  42421  aks4d1p1  42443  sq7  42663  235t711  42672  ex-decpmul  42673  3cubeslem3r  43041  fmtno5lem4  47913  257prm  47918  fmtno4nprmfac193  47931  fmtno5fac  47939  m3prm  47949  139prmALT  47953  127prm  47956  m7prm  47957  2exp340mod341  48090  8exp8mod9  48093