Theorem 3cn 12328

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 12310	. 2 ⊢ 3 = (2 + 1)
2		2cn 12322	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11221	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 3 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2142  (class class class)co 7412  ℂcc 11104  1c1 11107   + caddc 11109  2c2 12301  3c3 12302

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11164  ax-addcl 11166

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837  df-2 12309  df-3 12310

This theorem is used by:  3ex  12329  4cn  12332  4m1e3  12375  3p2e5  12397  3p3e6  12398  4p4e8  12401  5p4e9  12404  3t1e3  12411  3t2e6  12412  2t3e6  12413  3t3e9  12414  8th4div3  12470  halfthird  12471  halfpm6th  12472  6p4e10  12794  9t8e72  12850  sq3  14241  expnass  14251  01sqrexlem7  15306  caurcvgr  15732  bpoly2  16117  bpoly3  16118  bpoly4  16119  ef01bndlem  16246  sin01bnd  16247  cos01bnd  16248  cos1bnd  16249  cos2bnd  16250  cos01gt0  16253  rpnnen2lem3  16278  rpnnen2lem11  16286  3dvdsdec  16396  3dvds2dec  16397  5ndvds3  16477  3lcm2e6woprm  16679  2exp16  17156  13prm  17182  17prm  17183  19prm  17184  37prm  17187  43prm  17188  83prm  17189  139prm  17190  163prm  17191  317prm  17192  631prm  17193  1259lem1  17197  1259lem2  17198  1259lem3  17199  1259lem4  17200  1259lem5  17201  1259prm  17202  2503lem1  17203  2503lem2  17204  2503lem3  17205  2503prm  17206  4001lem1  17207  4001lem2  17208  4001lem3  17209  4001lem4  17210  4001prm  17211  tangtx  26681  sincos6thpi  26692  sincos3rdpi  26693  pigt3  26694  pige3ALT  26696  2logb9irrALT  26974  ang180lem2  26986  1cubr  27018  dcubic1lem  27019  dcubic2  27020  dcubic1  27021  dcubic  27022  mcubic  27023  cubic2  27024  cubic  27025  binom4  27026  quart1cl  27030  quart1lem  27031  quart1  27032  quartlem1  27033  quartlem3  27035  log2cnv  27120  log2tlbnd  27121  log2ublem2  27123  log2ublem3  27124  log2ub  27125  basellem5  27260  basellem8  27263  basellem9  27264  ppiub  27379  chtub  27387  bclbnd  27455  bposlem6  27464  bposlem8  27466  bposlem9  27467  lgsdir2lem1  27500  lgsdir2lem5  27504  2lgslem3b  27572  2lgslem3d  27574  2lgsoddprmlem3c  27587  2lgsoddprmlem3d  27588  addsqnreup  27618  pntibndlem1  27764  pntlemk  27781  ex-opab  30794  ex-exp  30812  ex-dvds  30818  ex-gcd  30819  ex-lcm  30820  ex-prmo  30821  ex-ind-dvds  30823  ply1dg3rt0irred  33883  2sqr3minply  34179  2sqr3nconstr  34180  cos9thpiminplylem2  34182  cos9thpiminplylem3  34183  cos9thpiminplylem4  34184  cos9thpiminplylem5  34185  cos9thpiminply  34187  cos9thpinconstrlem1  34188  cos9thpinconstrlem2  34189  cos9thpinconstr  34190  fib5  34804  fib6  34805  hgt750lem  35047  hgt750lem2  35048  hgt750leme  35054  problem4  36168  problem5  36169  sinccvglem  36172  mblfinlem3  38338  itg2addnclem2  38351  itg2addnclem3  38352  heiborlem6  38495  heiborlem7  38496  3lexlogpow2ineq2  42854  3lexlogpow5ineq5  42855  aks4d1p1  42871  2ap1caineq  42940  25or6to4  43001  3rdpwhole  43081  235t711  43094  ex-decpmul  43095  tan3rdpi  43141  sin2t3rdpi  43142  cos2t3rdpi  43143  sin4t3rdpi  43144  cos4t3rdpi  43145  cu3addd  43440  3cubeslem3l  43445  3cubeslem3r  43446  jm2.23  43751  inductionexd  44909  lhe4.4ex1a  45067  stoweidlem13  46755  stoweidlem26  46768  stoweidlem34  46776  wallispilem4  46810  wallispi2lem1  46813  sin5tlem1  47638  sin5tlem2  47639  sin5tlem3  47640  sin5tlem4  47641  sin5tlem5  47642  sin5t  47643  goldrasin  47647  ceil5half3  48111  fmtno5lem1  48333  fmtno5lem2  48334  257prm  48341  fmtno4prmfac  48352  fmtno4nprmfac193  48354  139prmALT  48376  127prm  48379  mod42tp1mod8  48382  3exp4mod41  48396  41prothprmlem2  48398  ppivalnn4  48407  6even  48504  11t31e341  48525  2exp340mod341  48526  gbpart8  48561  sbgoldbwt  48570  sbgoldbst  48571  evengpop3  48591  evengpoap3  48592  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  2t6m3t4e0  49156  linevalexample  49203  zlmodzxzequa  49304  zlmodzxzequap  49307  ackval3  49491  ackval2012  49499  ackval3012  49500  ackval41  49503  ackval42  49504