Theorem 3cn 12349

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
3cn	⊢ 3 ∈ ℂ

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		df-3 12331	. 2 ⊢ 3 = (2 + 1)
2		2cn 12343	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11242	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 3 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125  1c1 11128   + caddc 11130  2c2 12322  3c3 12323

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 2147  ax-9 2155  ax-ext 2732  ax-1cn 11185  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12330  df-3 12331

This theorem is used by:  3ex  12350  4cn  12353  4m1e3  12396  3p2e5  12418  3p3e6  12419  4p4e8  12422  5p4e9  12425  3t1e3  12432  3t2e6  12433  2t3e6  12434  3t3e9  12435  8th4div3  12491  halfthird  12492  halfpm6th  12493  6p4e10  12816  9t8e72  12872  sq3  14265  expnass  14275  01sqrexlem7  15338  caurcvgr  15764  bpoly2  16146  bpoly3  16147  bpoly4  16148  ef01bndlem  16275  sin01bnd  16276  cos01bnd  16277  cos1bnd  16278  cos2bnd  16279  cos01gt0  16282  rpnnen2lem3  16307  rpnnen2lem11  16315  3dvdsdec  16425  3dvds2dec  16426  5ndvds3  16506  3lcm2e6woprm  16708  2exp16  17185  13prm  17211  17prm  17212  19prm  17213  37prm  17216  43prm  17217  83prm  17218  139prm  17219  163prm  17220  317prm  17221  631prm  17222  1259lem1  17226  1259lem2  17227  1259lem3  17228  1259lem4  17229  1259lem5  17230  1259prm  17231  2503lem1  17232  2503lem2  17233  2503lem3  17234  2503prm  17235  4001lem1  17236  4001lem2  17237  4001lem3  17238  4001lem4  17239  4001prm  17240  tangtx  26746  sincos6thpi  26756  sincos3rdpi  26757  pigt3  26758  pige3ALT  26760  2logb9irrALT  27038  ang180lem2  27050  1cubr  27082  dcubic1lem  27083  dcubic2  27084  dcubic1  27085  dcubic  27086  mcubic  27087  cubic2  27088  cubic  27089  binom4  27090  quart1cl  27094  quart1lem  27095  quart1  27096  quartlem1  27097  quartlem3  27099  log2cnv  27184  log2tlbnd  27185  log2ublem2  27187  log2ublem3  27188  log2ub  27189  basellem5  27324  basellem8  27327  basellem9  27328  ppiub  27443  chtub  27451  bclbnd  27519  bposlem6  27528  bposlem8  27530  bposlem9  27531  lgsdir2lem1  27564  lgsdir2lem5  27568  2lgslem3b  27636  2lgslem3d  27638  2lgsoddprmlem3c  27651  2lgsoddprmlem3d  27652  addsqnreup  27682  pntibndlem1  27828  pntlemk  27845  ex-opab  30915  ex-exp  30933  ex-dvds  30939  ex-gcd  30940  ex-lcm  30941  ex-prmo  30942  ex-ind-dvds  30944  ply1dg3rt0irred  33997  2sqr3minply  34293  2sqr3nconstr  34294  cos9thpiminplylem2  34296  cos9thpiminplylem3  34297  cos9thpiminplylem4  34298  cos9thpiminplylem5  34299  cos9thpiminply  34301  cos9thpinconstrlem1  34302  cos9thpinconstrlem2  34303  cos9thpinconstr  34304  fib5  34919  fib6  34920  hgt750lem  35162  hgt750lem2  35163  hgt750leme  35169  problem4  36250  problem5  36251  sinccvglem  36254  mblfinlem3  38411  itg2addnclem2  38424  itg2addnclem3  38425  heiborlem6  38569  heiborlem7  38570  3lexlogpow2ineq2  42928  3lexlogpow5ineq5  42929  aks4d1p1  42945  2ap1caineq  43014  25or6to4  43075  1p4e5  43130  2p5e7  43137  3p4e7  43140  3p5e8  43141  3p6e9  43142  3rdpwhole  43170  235t711  43183  ex-decpmul  43184  tan3rdpi  43230  sin2t3rdpi  43231  cos2t3rdpi  43232  sin4t3rdpi  43233  cos4t3rdpi  43234  cu3addd  43529  3cubeslem3l  43534  3cubeslem3r  43535  jm2.23  43840  inductionexd  44998  lhe4.4ex1a  45156  stoweidlem13  46844  stoweidlem26  46857  stoweidlem34  46865  wallispilem4  46899  wallispi2lem1  46902  sin5tlem1  47740  sin5tlem2  47741  sin5tlem3  47742  sin5tlem4  47743  sin5tlem5  47744  sin5t  47745  goldrasin  47750  ceil5half3  48237  fmtno5lem1  48459  fmtno5lem2  48460  257prm  48467  fmtno4prmfac  48478  fmtno4nprmfac193  48480  139prmALT  48502  127prm  48505  mod42tp1mod8  48508  3exp4mod41  48522  41prothprmlem2  48524  ppivalnn4  48533  6even  48630  11t31e341  48651  2exp340mod341  48652  gbpart8  48687  sbgoldbwt  48696  sbgoldbst  48697  evengpop3  48717  evengpoap3  48718  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  2t6m3t4e0  49281  linevalexample  49328  zlmodzxzequa  49429  zlmodzxzequap  49432  ackval3  49616  ackval2012  49624  ackval3012  49625  ackval41  49628  ackval42  49629