Theorem 7cn 11719

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 11693	. 2 ⊢ 7 = (6 + 1)
2		6cn 11716	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 10584	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10636	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2886	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   + caddc 10529  6c6 11684  7c7 11685

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addcl 10586

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693

This theorem is referenced by:  8cn  11722  8m1e7  11758  7p2e9  11786  7p3e10  12161  7t2e14  12195  7t4e28  12197  7t7e49  12200  cos2bnd  15533  23prm  16444  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem4  16469  4001prm  16470  log2ublem3  25534  log2ub  25535  bclbnd  25864  bposlem8  25875  2lgslem3d  25983  ex-prmo  28244  hgt750lem  32032  hgt750lem2  32033  60lcm7e420  39298  3lexlogpow5ineq1  39341  235t711  39485  ex-decpmul  39486  3cubeslem3r  39628  fmtno5lem4  44073  257prm  44078  fmtno4nprmfac193  44091  fmtno5fac  44099  m3prm  44109  139prmALT  44113  127prm  44116  m7prm  44117  2exp340mod341  44251  8exp8mod9  44254