Theorem 7cn 12306

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 12279	. 2 ⊢ 7 = (6 + 1)
2		6cn 12303	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11125	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11182	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2141  (class class class)co 7391  ℂcc 11065  1c1 11068   + caddc 11070  6c6 12270  7c7 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125  ax-addcl 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279

This theorem is referenced by:  8cn  12309  8m1e7  12344  7p2e9  12372  7p3e10  12762  7t2e14  12796  7t4e28  12798  7t7e49  12801  cos2bnd  16211  23prm  17146  139prm  17151  163prm  17152  317prm  17153  631prm  17154  1259lem1  17158  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  1259prm  17163  2503lem1  17164  2503lem2  17165  2503lem3  17166  4001lem1  17168  4001lem4  17171  4001prm  17172  log2ublem3  27001  log2ub  27002  bclbnd  27332  bposlem8  27343  2lgslem3d  27451  ex-prmo  30618  hgt750lem  34906  hgt750lem2  34907  60lcm7e420  42588  3exp7  42631  3lexlogpow5ineq1  42632  aks4d1p1  42654  sq7  42866  235t711  42875  ex-decpmul  42876  3cubeslem3r  43229  fmtno5lem4  48126  257prm  48131  fmtno4nprmfac193  48144  fmtno5fac  48152  m3prm  48162  139prmALT  48166  127prm  48169  m7prm  48170  ppivalnn4  48197  2exp340mod341  48316  8exp8mod9  48319