Theorem 1cnd 11130

Description: One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 11087	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11027  1c1 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 11087

This theorem is referenced by:  adddirp1d  11162  1p1times  11308  addcom  11323  addcomd  11339  muladd11r  11350  pncan1  11565  npcan1  11566  muls1d  11601  mulsubfacd  11602  recrec  11843  rec11  11844  rec11r  11845  rereccl  11864  subrecd  11975  nn1m1nn  12186  nnadd1com  12191  nnaddcom  12192  nnadddir  12224  nnmul1com  12225  nnmulcom  12226  add1p1  12419  sub1m1  12420  cnm2m1cnm3  12421  xp1d2m1eqxm1d2  12422  div4p1lem1div2  12423  nn0n0n1ge2  12496  zneo  12603  rpnnen1lem5  12922  lincmb01cmp  13439  iccf1o  13440  xov1plusxeqvd  13442  zpnn0elfzo1  13685  ubmelm1fzo  13709  fzosplitpr  13723  fzosplitprm1  13724  fzom1ne1  13731  fzoshftral  13733  fladdz  13775  2tnp1ge0ge0  13779  ltdifltdiv  13784  dfceil2  13789  negmod  13869  modnegd  13879  addmodlteq  13899  binom2sub1  14174  binom3  14177  zesq  14179  sqoddm1div8  14196  bcm1k  14268  bcp1n  14269  bcp1m1  14273  bcpasc  14274  bcn2m1  14277  hashfz  14380  hashfzo  14382  hashfzp1  14384  hashf1lem2  14409  hashf1  14410  hashdifsnp1  14459  lswccatn0lsw  14545  ccatws1lenp1b  14575  revccat  14719  repswrevw  14740  cshwidxm1  14760  cshwidxn  14762  cshweqrep  14774  cshimadifsn0  14783  swrds2m  14894  swrd2lsw  14905  relexpaddnn  15004  absexpz  15258  reccn2  15550  rlimno1  15607  isercolllem1  15618  isercoll2  15622  iseraltlem2  15636  iseraltlem3  15637  fsump1  15709  fsumconst1  15744  hashiun  15776  hash2iun1dif1  15778  indsumhash  15783  binomlem  15785  bcxmas  15791  incexc  15793  incexc2  15794  climcndslem1  15805  arisum  15816  arisum2  15817  trireciplem  15818  pwdif  15824  pwm1geoser  15825  geolim2  15827  georeclim  15828  mertenslem1  15840  prodfrec  15851  ntrivcvg  15853  ntrivcvgtail  15856  prodrblem  15885  prodmolem2a  15890  fprodntriv  15898  prod1  15900  fprodser  15905  fprodcl  15908  fprodm1  15923  fprodp1  15925  fprodclf  15948  risefacval2  15966  fallfacval2  15967  risefacp1  15985  fallfacp1  15986  risefacfac  15991  fallfacfwd  15992  binomfallfaclem2  15996  fallfacval4  15999  bpolydiflem  16010  ef0lem  16034  tanaddlem  16124  tanadd  16125  cos01bnd  16144  oddm1even  16303  oddp1even  16304  oexpneg  16305  ltoddhalfle  16321  halfleoddlt  16322  nn0ob  16344  pwp1fsum  16351  flodddiv4  16375  bitsp1o  16393  bitsf1  16406  sadcp1  16415  qredeu  16618  prmdiv  16746  prmdiveq  16747  vfermltlALT  16764  pc2dvds  16841  4sqlem11  16917  4sqlem12  16918  vdwapun  16936  vdwlem3  16945  vdwlem6  16948  vdwlem9  16951  ramub1lem2  16989  prmop1  17000  prmdvdsprmo  17004  prmgaplem8  17020  cshwshashnsame  17065  chnub  18579  chnlt  18580  chnccat  18583  chnrev  18584  gsumsgrpccat  18799  psgnunilem5  19460  psgnunilem2  19461  sylow1lem1  19564  efgredlemc  19711  odadd2  19815  ablsimpgfindlem1  20075  omndmul2  20099  srgbinomlem3  20200  srgbinomlem4  20201  cncrng  21368  gzrngunit  21408  zringunit  21441  prmirredlem  21447  pzriprnglem12  21467  freshmansdream  21549  mhppwdeg  22138  psdmul  22154  cayhamlem1  22849  expcn  24857  iirevcn  24915  iihalf2cn  24919  icchmeo  24926  icopnfcnv  24927  icopnfhmeo  24928  evth  24944  pcoass  25009  pjthlem1  25422  ovolunlem1a  25481  ovolunlem1  25482  opnmbllem  25586  mbfi1fseqlem6  25705  bddibl  25825  dvnadd  25914  dvmptid  25942  dvmptdiv  25959  dvcnvlem  25961  dveflem  25964  dvef  25965  dvsincos  25966  dvlipcn  25979  dvivthlem1  25993  lhop2  26000  dvcvx  26005  dvfsumle  26006  dvfsumabs  26008  dvfsumlem1  26011  dvfsumlem2  26012  itgpowd  26035  ply1divex  26120  fta1glem1  26151  dgrcolem1  26256  dgrcolem2  26257  vieta1lem1  26294  aaliou3lem2  26327  aaliou3lem8  26329  dvtaylp  26353  dvntaylp  26354  taylthlem1  26356  taylthlem2  26357  abelthlem1  26414  abelthlem2  26415  abelthlem6  26419  abelthlem7  26421  logdivlti  26602  advlog  26636  advlogexp  26637  logtayl  26642  cxpmul2  26671  dvcxp1  26722  dvcxp2  26723  dvcncxp1  26725  dvcnsqrt  26726  loglesqrt  26743  relogbdiv  26761  ang180lem4  26794  ang180lem5  26795  isosctrlem2  26801  isosctrlem3  26802  affineequiv  26805  affineequiv2  26806  affineequiv3  26807  angpieqvdlem  26810  chordthmlem2  26815  chordthmlem3  26816  chordthmlem5  26818  dcubic2  26826  dcubic  26828  quart1lem  26837  quart1  26838  quart  26843  asinlem  26850  asinlem3  26853  atansopn  26914  dvatan  26917  leibpi  26924  birthdaylem2  26934  efrlim  26951  cxplim  26953  divsqrtsumlem  26961  logdifbnd  26975  emcllem2  26978  emcllem3  26979  emcllem5  26981  zetacvg  26996  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  lgam1  27045  gamfac  27048  wilthlem2  27050  wilthimp  27053  ftalem5  27058  basellem3  27064  basellem5  27066  basellem8  27069  basellem9  27070  sqff1o  27163  muinv  27174  logfaclbnd  27203  logfacrlim  27205  logexprlim  27206  perfectlem2  27211  dchr1cl  27232  dchrinvcl  27234  dchrfi  27236  dchr1  27238  dchrsum2  27249  bcmono  27258  bcp1ctr  27260  bclbnd  27261  bposlem9  27273  gausslemma2dlem1a  27346  gausslemma2dlem5  27352  lgseisenlem4  27359  lgsquadlem1  27361  m1lgs  27369  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgslem3d1  27384  2lgsoddprmlem1  27389  2sqlem8  27407  2sq2  27414  addsqn2reu  27422  addsqrexnreu  27423  addsqnreup  27424  addsq2nreurex  27425  chtppilim  27456  rpvmasumlem  27468  dchrisumlem1  27470  dchrisum0re  27494  dchrisum0lem2a  27498  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  2vmadivsumlem  27521  selberg4lem1  27541  pntrsumo1  27546  selberg34r  27552  pntrlog2bndlem2  27559  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntibndlem2  27572  pntlemg  27579  pntlemr  27583  pntlemf  27586  pntlemk  27587  pntlemo  27588  pntlem3  27590  ostth2lem2  27615  ttgcontlem1  28971  cusgrsize2inds  29540  wlklenvclwlk  29740  pthdadjvtx  29814  crctcshwlkn0lem1  29896  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  wlklnwwlkln2lem  29968  wlknwwlksnbij  29974  wwlksnred  29978  wwlksnext  29979  wwlksnextbi  29980  wwlksnredwwlkn  29981  wwlksnextwrd  29983  wwlksnextinj  29985  wwlksnextproplem2  29996  wwlksnextproplem3  29997  clwwlkccatlem  30077  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlklem3  30089  clwlkclwwlk  30090  clwwisshclwwslemlem  30101  clwwisshclwws  30103  clwwlkel  30134  clwwlkf  30135  clwwlkwwlksb  30142  clwwlkext2edg  30144  wwlksext2clwwlk  30145  clwwlknonex2lem1  30195  clwwlknonex2lem2  30196  eucrct2eupth  30333  numclwwlk1lem2foalem  30439  numclwwlk1lem2fo  30446  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  numclwwlk6  30478  smcnlem  30786  receqid  32836  fzm1ne1  32880  bcm1n  32887  ltesubnnd  32915  sgn0bi  32932  oexpled  32939  wrdt2ind  33032  gsummptp1  33138  gsummulsubdishift1  33149  psgnfzto1stlem  33181  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  archirngz  33270  archiabllem1a  33272  archiabllem2c  33276  gsumind  33428  esplyind  33759  esplyindfv  33760  esplyfvn  33761  vietadeg1  33762  vietalem  33763  ccfldextdgrr  33856  constrfin  33930  nn0constr  33945  iconstr  33950  constrrecl  33953  constrimcl  33954  constrreinvcl  33956  constrinvcl  33957  constrresqrtcl  33961  2sqr3minply  33964  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  1smat1  33988  madjusmdetlem2  34012  madjusmdetlem4  34014  dya2icoseg  34461  iwrdsplit  34571  fibp1  34585  ballotlemfp1  34676  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemic  34691  ballotlem1c  34692  ballotlemsgt1  34695  ballotlemsdom  34696  ballotlemsel1i  34697  ballotlemsi  34699  ballotlemsima  34700  ballotlem1ri  34719  signstfvn  34753  signsvtn0  34754  signstfveq0  34761  signsvfn  34766  signsvtn  34768  signshf  34772  hashreprin  34804  circlemeth  34824  logdivsqrle  34834  revpfxsfxrev  35344  revwlk  35353  swrdwlk  35355  subfacp1lem1  35407  subfacp1lem5  35412  cvxpconn  35470  sinccvglem  35900  divcnvlin  35961  bcm1nt  35965  bcprod  35966  bccolsum  35967  iprodgam  35970  faclimlem1  35971  faclimlem2  35972  faclimlem3  35973  faclim  35974  iprodfac  35975  faclim2  35976  fwddifnp1  36393  dnizphlfeqhlf  36782  dnibndlem3  36786  dnibndlem13  36796  unblimceq0  36813  knoppndvlem6  36823  knoppndvlem9  36826  knoppndvlem14  36831  knoppndvlem15  36832  knoppndvlem16  36833  knoppndvlem17  36834  bj-bary1lem1  37671  irrdiff  37686  qdiff  37687  poimirlem25  38012  poimirlem26  38013  poimirlem32  38019  opnmbllem0  38023  itg2addnclem2  38039  dvasin  38071  dvacos  38072  areacirclem1  38075  areacirclem4  38078  areacirc  38080  bfp  38191  fzsplitnd  42467  lcmfunnnd  42497  lcmineqlem1  42514  lcmineqlem3  42516  lcmineqlem4  42517  lcmineqlem7  42520  lcmineqlem8  42521  lcmineqlem10  42523  lcmineqlem11  42524  lcmineqlem12  42525  lcmineqlem18  42531  lcmineqlem19  42532  lcmineqlem22  42535  lcmineqlem23  42536  dvrelogpow2b  42553  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p3  42563  aks4d1p7d1  42567  primrootsunit1  42582  posbezout  42585  primrootscoprbij  42587  primrootspoweq0  42591  aks6d1c1  42601  hashscontpow1  42606  2np3bcnp1  42629  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  sticksstones16  42647  sticksstones22  42653  aks6d1c6lem3  42657  aks6d1c7lem1  42665  unitscyglem5  42684  3rdpwhole  42769  fz1sump1  42787  oddnumth  42788  nicomachus  42789  sumcubes  42790  tan3rdpi  42829  redvmptabs  42837  readvrec  42839  reixi  42900  sn-mullid  42913  sn-0tie0  42941  renegmulnnass  42955  fiabv  43022  fltnltalem  43112  fltnlta  43113  3cubeslem1  43133  3cubeslem2  43134  3cubeslem4  43138  pell1qrge1  43315  rmspecfund  43354  acongeq  43428  jm2.18  43433  jm2.19lem3  43436  jm2.25  43444  jm2.16nn0  43449  jm3.1lem1  43462  jm3.1lem2  43463  areaquad  43661  relexpmulnn  44153  relexpaddss  44162  cvgdvgrat  44757  radcnvrat  44758  hashnzfzclim  44766  ofdivrec  44770  expgrowthi  44777  bccm1k  44786  dvradcnv2  44791  binomcxplemwb  44792  binomcxplemnn0  44793  binomcxplemrat  44794  binomcxplemfrat  44795  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  refsum2cnlem1  45485  fzisoeu  45748  fperiodmullem  45751  fzdifsuc2  45758  xralrple2  45799  nnsplit  45803  infleinflem2  45815  fmul01lt1lem2  46030  fprodcn  46045  clim1fr1  46046  isumneg  46047  climneg  46055  sumnnodd  46075  reclimc  46096  coseq0  46307  coskpi2  46309  cosknegpi  46312  fprodcncf  46343  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnxpaek  46385  dvnmul  46386  dvmptfprod  46388  dvnprodlem3  46391  itgsinexp  46398  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  stoweidlem1  46444  stoweidlem7  46450  stoweidlem10  46453  stoweidlem11  46454  stoweidlem14  46457  stoweidlem17  46460  stoweidlem34  46477  stoweidlem42  46485  wallispilem3  46510  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem8  46524  stirlinglem10  46526  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem15  46531  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncflem1  46546  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem11  46561  fourierdlem15  46565  fourierdlem26  46576  fourierdlem36  46586  fourierdlem40  46590  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem56  46605  fourierdlem58  46607  fourierdlem59  46608  fourierdlem62  46611  fourierdlem64  46613  fourierdlem65  46614  fourierdlem78  46627  fourierdlem79  46628  sqwvfoura  46671  fourierswlem  46673  fouriersw  46674  etransclem23  46700  etransclem24  46701  etransclem28  46705  etransclem35  46712  etransclem38  46715  nnfoctbdjlem  46898  smfmullem1  47234  sigaradd  47309  chnerlem2  47328  sin3t  47334  cos3t  47335  sin5tlem1  47336  sin5tlem2  47337  sin5tlem4  47339  cos5t  47342  cjnpoly  47352  deccarry  47774  ceilbi  47800  flmrecm1  47806  m1modne  47817  m1modmmod  47827  modm1nep2  47837  modm1nem2  47838  fargshiftf1  47916  fargshiftfo  47917  fmtnof1  48013  sqrtpwpw2p  48016  fmtnorec2lem  48020  fmtnorec4  48027  fmtnoprmfac1lem  48042  fmtnoprmfac1  48043  fmtnoprmfac2  48045  2pwp1prm  48067  mod42tp1mod8  48080  sfprmdvdsmersenne  48081  lighneallem3  48085  lighneallem4  48088  ppivalnnprm  48103  ppivalnnnprmge6  48104  onego  48137  zofldiv2ALTV  48153  oexpnegALTV  48168  opoeALTV  48174  opeoALTV  48175  epee  48196  perfectALTVlem1  48212  fppr2odd  48222  fpprwppr  48230  gpg3nbgrvtx0  48567  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  0nodd  48661  2nodd  48663  nnsgrpnmnd  48669  1neven  48729  altgsumbc  48843  pw2m1lepw2m1  49011  zofldiv2  49022  nnpw2pmod  49074  blen1b  49079  blennn0em1  49082  dignn0flhalflem1  49106  dignn0flhalflem2  49107  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  nn0sumshdiglem2  49113  itcovalpclem2  49162  ackval1  49172  ackval2  49173  ackval3  49174  affineid  49195  1subrec1sub  49196  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2vlinest  49232