Theorem 1cnd 11315

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 11271	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11211  1c1 11214

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1cn 11271

This theorem is used by:  adddirp1d  11348  1p1times  11494  addcom  11509  addcomd  11525  muladd11r  11536  pncan1  11753  npcan1  11754  muls1d  11789  mulsubfacd  11790  recrec  12027  rec11  12028  rec11r  12029  rereccl  12048  subrecd  12159  nn1m1nn  12369  nnadd1com  12374  nnaddcom  12375  nnadddir  12407  nnmul1com  12408  nnmulcom  12409  add1p1  12610  sub1m1  12611  cnm2m1cnm3  12612  xp1d2m1eqxm1d2  12613  div4p1lem1div2  12614  nn0n0n1ge2  12687  zneo  12795  rpnnen1lem5  13122  lincmb01cmp  13639  iccf1o  13640  xov1plusxeqvd  13642  zpnn0elfzo1  13887  ubmelm1fzo  13911  fzosplitpr  13925  fzosplitprm1  13926  fzom1ne1  13933  fzoshftral  13935  fladdz  13978  2tnp1ge0ge0  13982  ltdifltdiv  13987  dfceil2  13992  negmod  14072  modnegd  14082  addmodlteq  14102  binom2sub1  14378  binom3  14381  zesq  14383  sqoddm1div8  14400  bcm1k  14472  bcp1n  14473  bcp1m1  14477  bcpasc  14478  bcn2m1  14481  hashfz  14585  hashfzo  14587  hashfzp1  14589  hashf1lem2  14614  hashf1  14615  hashdifsnp1  14664  lswccatn0lsw  14751  ccatws1lenp1b  14783  revccat  14929  revpfxsfxrev  14931  repswrevw  14952  cshwidxm1  14972  cshwidxn  14974  cshweqrep  14986  cshimadifsn0  14995  swrds2m  15107  swrd2lsw  15120  relexpaddnn  15219  sgn0bi  15271  absexpz  15487  reccn2  15779  rlimno1  15836  isercolllem1  15847  isercoll2  15851  iseraltlem2  15865  iseraltlem3  15866  fsump1  15937  fsumconst1  15972  hashiun  16004  hash2iun1dif1  16006  indsumhash  16011  binomlem  16013  bcxmas  16019  incexc  16021  incexc2  16022  climcndslem1  16033  arisum  16044  arisum2  16045  trireciplem  16046  pwdif  16052  pwm1geoser  16053  geolim2  16055  georeclim  16056  mertenslem1  16068  prodfrec  16079  ntrivcvg  16081  ntrivcvgtail  16084  prodrblem  16111  prodmolem2a  16116  fprodntriv  16124  prod1  16126  fprodser  16131  fprodcl  16134  fprodm1  16149  fprodp1  16151  fprodclf  16174  risefacval2  16192  fallfacval2  16193  risefacp1  16210  fallfacp1  16211  risefacfac  16216  fallfacfwd  16217  binomfallfaclem2  16221  fallfacval4  16224  bpolydiflem  16235  ef0lem  16259  tanaddlem  16349  tanadd  16350  cos01bnd  16369  oddm1even  16528  oddp1even  16529  oexpneg  16530  ltoddhalfle  16546  halfleoddlt  16547  nn0ob  16569  pwp1fsum  16576  flodddiv4  16600  bitsp1o  16618  bitsf1  16631  sadcp1  16640  qredeu  16848  prmdiv  16977  prmdiveq  16978  vfermltlALT  16995  pc2dvds  17072  4sqlem11  17148  4sqlem12  17149  vdwapun  17167  vdwlem3  17176  vdwlem6  17179  vdwlem9  17182  ramub1lem2  17220  prmop1  17231  prmdvdsprmo  17235  prmgaplem8  17251  cshwshashnsame  17296  chnub  18811  chnlt  18812  chnccat  18815  chnrev  18816  gsumsgrpccat  19051  psgnunilem5  19723  psgnunilem2  19724  sylow1lem1  19827  efgredlemc  19974  odadd2  20078  ablsimpgfindlem1  20338  omndmul2  20362  srgbinomlem3  20469  srgbinomlem4  20470  cncrng  21714  gzrngunit  21754  zringunit  21787  prmirredlem  21793  pzriprnglem12  21813  freshmansdream  21895  mhppwdeg  22486  psdmul  22502  cayhamlem1  23199  expcn  25208  iirevcn  25266  iihalf2cn  25270  icchmeo  25277  icopnfcnv  25278  icopnfhmeo  25279  evth  25295  pcoass  25360  pjthlem1  25773  ovolunlem1a  25832  ovolunlem1  25833  opnmbllem  25937  mbfi1fseqlem6  26056  bddibl  26175  dvnadd  26264  dvmptid  26292  dvmptdiv  26309  dvcnvlem  26311  dveflem  26314  dvef  26315  dvsincos  26316  dvlipcn  26329  dvivthlem1  26343  lhop2  26350  dvcvx  26355  dvfsumle  26356  dvfsumabs  26358  dvfsumlem1  26361  dvfsumlem2  26362  itgpowd  26385  ply1divex  26470  fta1glem1  26501  dgrcolem1  26607  dgrcolem2  26608  vieta1lem1  26648  aaliou3lem2  26685  aaliou3lem8  26687  dvtaylp  26712  dvntaylp  26713  taylthlem1  26715  taylthlem2  26716  abelthlem1  26773  abelthlem2  26774  abelthlem6  26778  abelthlem7  26780  logdivlti  26963  advlog  26997  advlogexp  26998  logtayl  27003  cxpmul2  27032  dvcxp1  27083  dvcxp2  27084  dvcncxp1  27086  dvcnsqrt  27087  loglesqrt  27104  relogbdiv  27122  ang180lem4  27155  ang180lem5  27156  isosctrlem2  27162  isosctrlem3  27163  affineequiv  27166  affineequiv2  27167  affineequiv3  27168  angpieqvdlem  27171  chordthmlem2  27176  chordthmlem3  27177  chordthmlem5  27179  dcubic2  27187  dcubic  27189  quart1lem  27198  quart1  27199  quart  27204  asinlem  27211  asinlem3  27214  atansopn  27275  dvatan  27278  leibpi  27285  birthdaylem2  27295  efrlim  27312  cxplim  27314  divsqrtsumlem  27322  logdifbnd  27336  emcllem2  27339  emcllem3  27340  emcllem5  27342  zetacvg  27357  lgamgulmlem2  27372  lgamgulmlem3  27373  lgamgulmlem4  27374  lgamgulmlem5  27375  lgamgulmlem6  27376  lgamgulm2  27378  lgamcvg2  27397  gamcvg  27398  gamcvg2lem  27401  lgam1  27406  gamfac  27409  wilthlem2  27411  wilthimp  27414  ftalem5  27419  basellem3  27425  basellem5  27427  basellem8  27430  basellem9  27431  sqff1o  27524  muinv  27535  logfaclbnd  27564  logfacrlim  27566  logexprlim  27567  perfectlem2  27572  dchr1cl  27593  dchrinvcl  27595  dchrfi  27597  dchr1  27599  dchrsum2  27610  bcmono  27619  bcp1ctr  27621  bclbnd  27622  bposlem9  27634  gausslemma2dlem1a  27707  gausslemma2dlem5  27713  lgseisenlem4  27720  lgsquadlem1  27722  m1lgs  27730  2lgslem3a  27738  2lgslem3b  27739  2lgslem3c  27740  2lgslem3d  27741  2lgslem3d1  27745  2lgsoddprmlem1  27750  2sqlem8  27768  2sq2  27775  addsqn2reu  27783  addsqrexnreu  27784  addsqnreup  27785  addsq2nreurex  27786  chtppilim  27817  rpvmasumlem  27829  dchrisumlem1  27831  dchrisum0re  27855  dchrisum0lem2a  27859  mudivsum  27872  mulogsumlem  27873  mulogsum  27874  2vmadivsumlem  27882  selberg4lem1  27902  pntrsumo1  27907  selberg34r  27913  pntrlog2bndlem2  27920  pntrlog2bndlem4  27922  pntrlog2bndlem5  27923  pntrlog2bndlem6  27925  pntibndlem2  27933  pntlemg  27940  pntlemr  27944  pntlemf  27947  pntlemk  27948  pntlemo  27949  pntlem3  27951  ostth2lem2  27976  ttgcontlem1  29477  cusgrsize2inds  30049  wlklenvclwlk  30249  revwlk  30282  swrdwlk  30283  pthdadjvtx  30328  crctcshwlkn0lem1  30414  crctcshwlkn0lem4  30417  crctcshwlkn0lem5  30418  wlklnwwlkln2lem  30486  wlknwwlksnbij  30492  wwlksnred  30496  wwlksnext  30497  wwlksnextbi  30498  wwlksnredwwlkn  30499  wwlksnextwrd  30501  wwlksnextinj  30503  wwlksnextproplem2  30514  wwlksnextproplem3  30515  clwwlkccatlem  30595  clwlkclwwlklem2a1  30598  clwlkclwwlklem2a4  30603  clwlkclwwlklem2a  30604  clwlkclwwlklem2  30606  clwlkclwwlklem3  30607  clwlkclwwlk  30608  clwwisshclwwslemlem  30619  clwwisshclwws  30621  clwwlkel  30652  clwwlkf  30653  clwwlkwwlksb  30660  clwwlkext2edg  30662  wwlksext2clwwlk  30663  clwwlknonex2lem1  30713  clwwlknonex2lem2  30714  eucrct2eupth  30861  numclwwlk1lem2foalem  30967  numclwwlk1lem2fo  30974  numclwlk2lem2f  30993  numclwlk2lem2f1o  30995  numclwwlk6  31006  smcnlem  31314  receqid  33392  fzm1ne1  33436  bcm1n  33443  ltesubnnd  33470  oexpled  33483  wrdt2ind  33572  gsummptp1  33674  gsummulsubdishift1  33685  psgnfzto1stlem  33717  cycpmco2lem3  33745  cycpmco2lem4  33746  cycpmco2lem5  33747  cycpmco2lem6  33748  cycpmco2lem7  33749  cycpmco2  33750  archirngz  33806  archiabllem1a  33808  archiabllem2c  33812  gsumind  33962  esplyind  34263  esplyindfv  34264  esplyfvn  34265  vietadeg1  34266  vietalem  34267  ccfldextdgrr  34360  constrfin  34434  nn0constr  34449  iconstr  34454  constrrecl  34457  constrimcl  34458  constrreinvcl  34460  constrinvcl  34461  constrresqrtcl  34465  2sqr3minply  34468  cos9thpiminplylem1  34470  cos9thpiminplylem2  34471  cos9thpiminplylem3  34472  cos9thpiminply  34476  cos9thpinconstrlem1  34477  1smat1  34492  madjusmdetlem2  34516  madjusmdetlem4  34518  dya2icoseg  34965  iwrdsplit  35075  fibp1  35089  ballotlemfp1  35180  ballotlemfc0  35181  ballotlemfcc  35182  ballotlemic  35195  ballotlem1c  35196  ballotlemsgt1  35199  ballotlemsdom  35200  ballotlemsel1i  35201  ballotlemsi  35203  ballotlemsima  35204  ballotlem1ri  35223  signstfvn  35254  signsvtn0  35255  signstfveq0  35262  signsvfn  35267  signsvtn  35269  signshf  35273  hashreprin  35305  circlemeth  35325  logdivsqrle  35335  subfacp1lem1  36068  subfacp1lem5  36073  cvxpconn  36131  sinccvglem  36561  divcnvlin  36628  bcm1nt  36632  bcprod  36633  bccolsum  36634  iprodgam  36637  faclimlem1  36638  faclimlem2  36639  faclimlem3  36640  faclim  36641  iprodfac  36642  faclim2  36643  fwddifnp1  37060  dnizphlfeqhlf  37472  dnibndlem3  37476  dnibndlem13  37486  unblimceq0  37503  knoppndvlem6  37513  knoppndvlem9  37516  knoppndvlem14  37521  knoppndvlem15  37522  knoppndvlem16  37523  knoppndvlem17  37524  bj-bary1lem1  38375  irrdiff  38390  qdiff  38391  poimirlem25  38706  poimirlem26  38707  poimirlem32  38713  opnmbllem0  38717  itg2addnclem2  38733  dvasin  38765  dvacos  38766  areacirclem1  38769  areacirclem4  38772  areacirc  38774  bfp  38901  fzsplitnd  43175  lcmfunnnd  43205  lcmineqlem1  43222  lcmineqlem3  43224  lcmineqlem4  43225  lcmineqlem7  43228  lcmineqlem8  43229  lcmineqlem10  43231  lcmineqlem11  43232  lcmineqlem12  43233  lcmineqlem18  43239  lcmineqlem19  43240  lcmineqlem22  43243  lcmineqlem23  43244  dvrelogpow2b  43261  aks4d1p1p4  43264  aks4d1p1p6  43266  aks4d1p1p7  43267  aks4d1p1p5  43268  aks4d1p1  43269  aks4d1p3  43271  aks4d1p7d1  43275  primrootsunit1  43290  posbezout  43293  primrootscoprbij  43295  primrootspoweq0  43299  aks6d1c1  43309  hashscontpow1  43314  2np3bcnp1  43337  sticksstones10  43348  sticksstones12a  43350  sticksstones12  43351  sticksstones16  43355  sticksstones22  43361  aks6d1c6lem3  43365  aks6d1c7lem1  43373  unitscyglem5  43392  3rdpwhole  43492  fz1sump1  43510  oddnumth  43511  nicomachus  43512  sumcubes  43513  tan3rdpi  43546  redvmptabs  43554  readvrec  43556  reixi  43617  sn-mullid  43630  sn-0tie0  43658  renegmulnnass  43672  fiabv  43743  fltnltalem  43816  fltnlta  43817  3cubeslem1  43837  3cubeslem2  43838  3cubeslem4  43842  pell1qrge1  44020  rmspecfund  44059  acongeq  44133  jm2.18  44138  jm2.19lem3  44141  jm2.25  44149  jm2.16nn0  44154  jm3.1lem1  44167  jm3.1lem2  44168  areaquad  44361  relexpmulnn  44852  relexpaddss  44861  cvgdvgrat  45440  radcnvrat  45441  hashnzfzclim  45449  ofdivrec  45453  expgrowthi  45460  bccm1k  45469  dvradcnv2  45474  binomcxplemwb  45475  binomcxplemnn0  45476  binomcxplemrat  45477  binomcxplemfrat  45478  binomcxplemdvbinom  45480  binomcxplemnotnn0  45483  refsum2cnlem1  46196  fzisoeu  46458  fperiodmullem  46461  fzdifsuc2  46468  xralrple2  46508  nnsplit  46512  infleinflem2  46524  fmul01lt1lem2  46739  fprodcn  46754  clim1fr1  46755  isumneg  46756  climneg  46764  sumnnodd  46784  reclimc  46805  coseq0  47016  coskpi2  47018  cosknegpi  47021  fprodcncf  47052  fprodsubrecnncnvlem  47059  fprodaddrecnncnvlem  47061  ioodvbdlimc1lem2  47084  ioodvbdlimc2lem  47086  dvnxpaek  47094  dvnmul  47095  dvmptfprod  47097  dvnprodlem3  47100  itgsinexp  47107  itgiccshift  47132  itgperiod  47133  itgsbtaddcnst  47134  stoweidlem1  47153  stoweidlem7  47159  stoweidlem10  47162  stoweidlem11  47163  stoweidlem14  47166  stoweidlem17  47169  stoweidlem34  47186  stoweidlem42  47194  wallispilem3  47219  wallispilem5  47221  wallispi  47222  wallispi2lem1  47223  wallispi2lem2  47224  wallispi2  47225  stirlinglem1  47226  stirlinglem3  47228  stirlinglem4  47229  stirlinglem5  47230  stirlinglem6  47231  stirlinglem7  47232  stirlinglem8  47233  stirlinglem10  47235  stirlinglem11  47236  stirlinglem12  47237  stirlinglem13  47238  stirlinglem15  47240  dirkertrigeqlem2  47251  dirkertrigeqlem3  47252  dirkertrigeq  47253  dirkercncflem1  47255  dirkercncflem2  47256  dirkercncflem4  47258  fourierdlem11  47270  fourierdlem15  47274  fourierdlem26  47285  fourierdlem36  47295  fourierdlem40  47299  fourierdlem41  47300  fourierdlem42  47301  fourierdlem48  47306  fourierdlem49  47307  fourierdlem56  47314  fourierdlem58  47316  fourierdlem59  47317  fourierdlem62  47320  fourierdlem64  47322  fourierdlem65  47323  fourierdlem78  47336  fourierdlem79  47337  sqwvfoura  47380  fourierswlem  47382  fouriersw  47383  etransclem23  47409  etransclem24  47410  etransclem28  47414  etransclem35  47421  etransclem38  47424  nnfoctbdjlem  47607  smfmullem1  47943  sigaradd  48018  chnerlem2  48035  sin3t  48059  cos3t  48060  sin5tlem1  48061  sin5tlem2  48062  sin5tlem4  48064  cos5t  48067  goldratval  48078  cjnpoly  48081  deccarry  48523  ceilbi  48549  flmrecm1  48555  m1modne  48566  m1modmmod  48576  modm1nep2  48586  modm1nem2  48587  fargshiftf1  48665  fargshiftfo  48666  fmtnof1  48762  sqrtpwpw2p  48765  fmtnorec2lem  48769  fmtnorec4  48776  fmtnoprmfac1lem  48791  fmtnoprmfac1  48792  fmtnoprmfac2  48794  2pwp1prm  48816  mod42tp1mod8  48829  sfprmdvdsmersenne  48830  lighneallem3  48834  lighneallem4  48837  ppivalnnprm  48852  ppivalnnnprmge6  48853  onego  48886  zofldiv2ALTV  48902  oexpnegALTV  48917  opoeALTV  48923  opeoALTV  48924  epee  48945  perfectALTVlem1  48961  fppr2odd  48971  fpprwppr  48979  gpg3nbgrvtx0  49316  pgnbgreunbgrlem2lem1  49354  pgnbgreunbgrlem2lem2  49355  0nodd  49409  2nodd  49411  nnsgrpnmnd  49417  1neven  49477  altgsumbc  49606  pw2m1lepw2m1  49774  zofldiv2  49785  nnpw2pmod  49837  blen1b  49842  blennn0em1  49845  dignn0flhalflem1  49869  dignn0flhalflem2  49870  nn0sumshdiglemB  49874  nn0sumshdiglem1  49875  nn0sumshdiglem2  49876  itcovalpclem2  49925  ackval1  49935  ackval2  49936  ackval3  49937  affineid  49958  1subrec1sub  49959  eenglngeehlnmlem1  49992  eenglngeehlnmlem2  49993  rrx2vlinest  49995  dvsec  51073  dvcsc  51074