Theorem 1cnd 11302

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11198  1c1 11201

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

This theorem is used by:  adddirp1d  11335  1p1times  11481  addcom  11496  addcomd  11512  muladd11r  11523  pncan1  11740  npcan1  11741  muls1d  11776  mulsubfacd  11777  recrec  12014  rec11  12015  rec11r  12016  rereccl  12035  subrecd  12146  nn1m1nn  12356  nnadd1com  12361  nnaddcom  12362  nnadddir  12394  nnmul1com  12395  nnmulcom  12396  add1p1  12597  sub1m1  12598  cnm2m1cnm3  12599  xp1d2m1eqxm1d2  12600  div4p1lem1div2  12601  nn0n0n1ge2  12674  zneo  12782  rpnnen1lem5  13109  lincmb01cmp  13626  iccf1o  13627  xov1plusxeqvd  13629  zpnn0elfzo1  13874  ubmelm1fzo  13898  fzosplitpr  13912  fzosplitprm1  13913  fzom1ne1  13920  fzoshftral  13922  fladdz  13965  2tnp1ge0ge0  13969  ltdifltdiv  13974  dfceil2  13979  negmod  14059  modnegd  14069  addmodlteq  14089  binom2sub1  14365  binom3  14368  zesq  14370  sqoddm1div8  14387  bcm1k  14459  bcp1n  14460  bcp1m1  14464  bcpasc  14465  bcn2m1  14468  hashfz  14572  hashfzo  14574  hashfzp1  14576  hashf1lem2  14601  hashf1  14602  hashdifsnp1  14651  lswccatn0lsw  14738  ccatws1lenp1b  14769  revccat  14915  revpfxsfxrev  14917  repswrevw  14938  cshwidxm1  14958  cshwidxn  14960  cshweqrep  14972  cshimadifsn0  14981  swrds2m  15092  swrd2lsw  15105  relexpaddnn  15204  sgn0bi  15256  absexpz  15472  reccn2  15764  rlimno1  15821  isercolllem1  15832  isercoll2  15836  iseraltlem2  15850  iseraltlem3  15851  fsump1  15922  fsumconst1  15957  hashiun  15989  hash2iun1dif1  15991  indsumhash  15996  binomlem  15998  bcxmas  16004  incexc  16006  incexc2  16007  climcndslem1  16018  arisum  16029  arisum2  16030  trireciplem  16031  pwdif  16037  pwm1geoser  16038  geolim2  16040  georeclim  16041  mertenslem1  16053  prodfrec  16064  ntrivcvg  16066  ntrivcvgtail  16069  prodrblem  16096  prodmolem2a  16101  fprodntriv  16109  prod1  16111  fprodser  16116  fprodcl  16119  fprodm1  16134  fprodp1  16136  fprodclf  16159  risefacval2  16177  fallfacval2  16178  risefacp1  16195  fallfacp1  16196  risefacfac  16201  fallfacfwd  16202  binomfallfaclem2  16206  fallfacval4  16209  bpolydiflem  16220  ef0lem  16244  tanaddlem  16334  tanadd  16335  cos01bnd  16354  oddm1even  16513  oddp1even  16514  oexpneg  16515  ltoddhalfle  16531  halfleoddlt  16532  nn0ob  16554  pwp1fsum  16561  flodddiv4  16585  bitsp1o  16603  bitsf1  16616  sadcp1  16625  qredeu  16833  prmdiv  16962  prmdiveq  16963  vfermltlALT  16980  pc2dvds  17057  4sqlem11  17133  4sqlem12  17134  vdwapun  17152  vdwlem3  17161  vdwlem6  17164  vdwlem9  17167  ramub1lem2  17205  prmop1  17216  prmdvdsprmo  17220  prmgaplem8  17236  cshwshashnsame  17281  chnub  18796  chnlt  18797  chnccat  18800  chnrev  18801  gsumsgrpccat  19036  psgnunilem5  19708  psgnunilem2  19709  sylow1lem1  19812  efgredlemc  19959  odadd2  20063  ablsimpgfindlem1  20323  omndmul2  20347  srgbinomlem3  20454  srgbinomlem4  20455  cncrng  21699  gzrngunit  21739  zringunit  21772  prmirredlem  21778  pzriprnglem12  21798  freshmansdream  21880  mhppwdeg  22471  psdmul  22487  cayhamlem1  23184  expcn  25193  iirevcn  25251  iihalf2cn  25255  icchmeo  25262  icopnfcnv  25263  icopnfhmeo  25264  evth  25280  pcoass  25345  pjthlem1  25758  ovolunlem1a  25817  ovolunlem1  25818  opnmbllem  25922  mbfi1fseqlem6  26041  bddibl  26160  dvnadd  26249  dvmptid  26277  dvmptdiv  26294  dvcnvlem  26296  dveflem  26299  dvef  26300  dvsincos  26301  dvlipcn  26314  dvivthlem1  26328  lhop2  26335  dvcvx  26340  dvfsumle  26341  dvfsumabs  26343  dvfsumlem1  26346  dvfsumlem2  26347  itgpowd  26370  ply1divex  26455  fta1glem1  26486  dgrcolem1  26592  dgrcolem2  26593  vieta1lem1  26633  aaliou3lem2  26670  aaliou3lem8  26672  dvtaylp  26697  dvntaylp  26698  taylthlem1  26700  taylthlem2  26701  abelthlem1  26758  abelthlem2  26759  abelthlem6  26763  abelthlem7  26765  logdivlti  26948  advlog  26982  advlogexp  26983  logtayl  26988  cxpmul2  27017  dvcxp1  27068  dvcxp2  27069  dvcncxp1  27071  dvcnsqrt  27072  loglesqrt  27089  relogbdiv  27107  ang180lem4  27140  ang180lem5  27141  isosctrlem2  27147  isosctrlem3  27148  affineequiv  27151  affineequiv2  27152  affineequiv3  27153  angpieqvdlem  27156  chordthmlem2  27161  chordthmlem3  27162  chordthmlem5  27164  dcubic2  27172  dcubic  27174  quart1lem  27183  quart1  27184  quart  27189  asinlem  27196  asinlem3  27199  atansopn  27260  dvatan  27263  leibpi  27270  birthdaylem2  27280  efrlim  27297  cxplim  27299  divsqrtsumlem  27307  logdifbnd  27321  emcllem2  27324  emcllem3  27325  emcllem5  27327  zetacvg  27342  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem4  27359  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgamcvg2  27382  gamcvg  27383  gamcvg2lem  27386  lgam1  27391  gamfac  27394  wilthlem2  27396  wilthimp  27399  ftalem5  27404  basellem3  27410  basellem5  27412  basellem8  27415  basellem9  27416  sqff1o  27509  muinv  27520  logfaclbnd  27549  logfacrlim  27551  logexprlim  27552  perfectlem2  27557  dchr1cl  27578  dchrinvcl  27580  dchrfi  27582  dchr1  27584  dchrsum2  27595  bcmono  27604  bcp1ctr  27606  bclbnd  27607  bposlem9  27619  gausslemma2dlem1a  27692  gausslemma2dlem5  27698  lgseisenlem4  27705  lgsquadlem1  27707  m1lgs  27715  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2lgslem3d1  27730  2lgsoddprmlem1  27735  2sqlem8  27753  2sq2  27760  addsqn2reu  27768  addsqrexnreu  27769  addsqnreup  27770  addsq2nreurex  27771  chtppilim  27802  rpvmasumlem  27814  dchrisumlem1  27816  dchrisum0re  27840  dchrisum0lem2a  27844  mudivsum  27857  mulogsumlem  27858  mulogsum  27859  2vmadivsumlem  27867  selberg4lem1  27887  pntrsumo1  27892  selberg34r  27898  pntrlog2bndlem2  27905  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntibndlem2  27918  pntlemg  27925  pntlemr  27929  pntlemf  27932  pntlemk  27933  pntlemo  27934  pntlem3  27936  ostth2lem2  27961  ttgcontlem1  29462  cusgrsize2inds  30034  wlklenvclwlk  30234  revwlk  30267  swrdwlk  30268  pthdadjvtx  30313  crctcshwlkn0lem1  30399  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  wlklnwwlkln2lem  30471  wlknwwlksnbij  30477  wwlksnred  30481  wwlksnext  30482  wwlksnextbi  30483  wwlksnredwwlkn  30484  wwlksnextwrd  30486  wwlksnextinj  30488  wwlksnextproplem2  30499  wwlksnextproplem3  30500  clwwlkccatlem  30580  clwlkclwwlklem2a1  30583  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  clwlkclwwlklem3  30592  clwlkclwwlk  30593  clwwisshclwwslemlem  30604  clwwisshclwws  30606  clwwlkel  30637  clwwlkf  30638  clwwlkwwlksb  30645  clwwlkext2edg  30647  wwlksext2clwwlk  30648  clwwlknonex2lem1  30698  clwwlknonex2lem2  30699  eucrct2eupth  30846  numclwwlk1lem2foalem  30952  numclwwlk1lem2fo  30959  numclwlk2lem2f  30978  numclwlk2lem2f1o  30980  numclwwlk6  30991  smcnlem  31299  receqid  33336  fzm1ne1  33380  bcm1n  33387  ltesubnnd  33414  oexpled  33427  wrdt2ind  33516  gsummptp1  33618  gsummulsubdishift1  33629  psgnfzto1stlem  33661  cycpmco2lem3  33689  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2lem7  33693  cycpmco2  33694  archirngz  33750  archiabllem1a  33752  archiabllem2c  33756  gsumind  33906  esplyind  34207  esplyindfv  34208  esplyfvn  34209  vietadeg1  34210  vietalem  34211  ccfldextdgrr  34304  constrfin  34378  nn0constr  34393  iconstr  34398  constrrecl  34401  constrimcl  34402  constrreinvcl  34404  constrinvcl  34405  constrresqrtcl  34409  2sqr3minply  34412  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  cos9thpiminplylem3  34416  cos9thpiminply  34420  cos9thpinconstrlem1  34421  1smat1  34436  madjusmdetlem2  34460  madjusmdetlem4  34462  dya2icoseg  34909  iwrdsplit  35019  fibp1  35033  ballotlemfp1  35124  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemic  35139  ballotlem1c  35140  ballotlemsgt1  35143  ballotlemsdom  35144  ballotlemsel1i  35145  ballotlemsi  35147  ballotlemsima  35148  ballotlem1ri  35167  signstfvn  35198  signsvtn0  35199  signstfveq0  35206  signsvfn  35211  signsvtn  35213  signshf  35217  hashreprin  35249  circlemeth  35269  logdivsqrle  35279  subfacp1lem1  35944  subfacp1lem5  35949  cvxpconn  36007  sinccvglem  36437  divcnvlin  36498  bcm1nt  36502  bcprod  36503  bccolsum  36504  iprodgam  36507  faclimlem1  36508  faclimlem2  36509  faclimlem3  36510  faclim  36511  iprodfac  36512  faclim2  36513  fwddifnp1  36930  dnizphlfeqhlf  37342  dnibndlem3  37346  dnibndlem13  37356  unblimceq0  37373  knoppndvlem6  37383  knoppndvlem9  37386  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem16  37393  knoppndvlem17  37394  bj-bary1lem1  38232  irrdiff  38247  qdiff  38248  poimirlem25  38563  poimirlem26  38564  poimirlem32  38570  opnmbllem0  38574  itg2addnclem2  38590  dvasin  38622  dvacos  38623  areacirclem1  38626  areacirclem4  38629  areacirc  38631  bfp  38758  fzsplitnd  43032  lcmfunnnd  43062  lcmineqlem1  43079  lcmineqlem3  43081  lcmineqlem4  43082  lcmineqlem7  43085  lcmineqlem8  43086  lcmineqlem10  43088  lcmineqlem11  43089  lcmineqlem12  43090  lcmineqlem18  43096  lcmineqlem19  43097  lcmineqlem22  43100  lcmineqlem23  43101  dvrelogpow2b  43118  aks4d1p1p4  43121  aks4d1p1p6  43123  aks4d1p1p7  43124  aks4d1p1p5  43125  aks4d1p1  43126  aks4d1p3  43128  aks4d1p7d1  43132  primrootsunit1  43147  posbezout  43150  primrootscoprbij  43152  primrootspoweq0  43156  aks6d1c1  43166  hashscontpow1  43171  2np3bcnp1  43194  sticksstones10  43205  sticksstones12a  43207  sticksstones12  43208  sticksstones16  43212  sticksstones22  43218  aks6d1c6lem3  43222  aks6d1c7lem1  43230  unitscyglem5  43249  3rdpwhole  43349  fz1sump1  43367  oddnumth  43368  nicomachus  43369  sumcubes  43370  tan3rdpi  43403  redvmptabs  43411  readvrec  43413  reixi  43474  sn-mullid  43487  sn-0tie0  43515  renegmulnnass  43529  fiabv  43600  fltnltalem  43673  fltnlta  43674  3cubeslem1  43694  3cubeslem2  43695  3cubeslem4  43699  pell1qrge1  43876  rmspecfund  43915  acongeq  43989  jm2.18  43994  jm2.19lem3  43997  jm2.25  44005  jm2.16nn0  44010  jm3.1lem1  44023  jm3.1lem2  44024  areaquad  44217  relexpmulnn  44708  relexpaddss  44717  cvgdvgrat  45296  radcnvrat  45297  hashnzfzclim  45305  ofdivrec  45309  expgrowthi  45316  bccm1k  45325  dvradcnv2  45330  binomcxplemwb  45331  binomcxplemnn0  45332  binomcxplemrat  45333  binomcxplemfrat  45334  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  refsum2cnlem1  46053  fzisoeu  46315  fperiodmullem  46318  fzdifsuc2  46325  xralrple2  46365  nnsplit  46369  infleinflem2  46381  fmul01lt1lem2  46596  fprodcn  46611  clim1fr1  46612  isumneg  46613  climneg  46621  sumnnodd  46641  reclimc  46662  coseq0  46873  coskpi2  46875  cosknegpi  46878  fprodcncf  46909  fprodsubrecnncnvlem  46916  fprodaddrecnncnvlem  46918  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnxpaek  46951  dvnmul  46952  dvmptfprod  46954  dvnprodlem3  46957  itgsinexp  46964  itgiccshift  46989  itgperiod  46990  itgsbtaddcnst  46991  stoweidlem1  47010  stoweidlem7  47016  stoweidlem10  47019  stoweidlem11  47020  stoweidlem14  47023  stoweidlem17  47026  stoweidlem34  47043  stoweidlem42  47051  wallispilem3  47076  wallispilem5  47078  wallispi  47079  wallispi2lem1  47080  wallispi2lem2  47081  wallispi2  47082  stirlinglem1  47083  stirlinglem3  47085  stirlinglem4  47086  stirlinglem5  47087  stirlinglem6  47088  stirlinglem7  47089  stirlinglem8  47090  stirlinglem10  47092  stirlinglem11  47093  stirlinglem12  47094  stirlinglem13  47095  stirlinglem15  47097  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkercncflem1  47112  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem11  47127  fourierdlem15  47131  fourierdlem26  47142  fourierdlem36  47152  fourierdlem40  47156  fourierdlem41  47157  fourierdlem42  47158  fourierdlem48  47163  fourierdlem49  47164  fourierdlem56  47171  fourierdlem58  47173  fourierdlem59  47174  fourierdlem62  47177  fourierdlem64  47179  fourierdlem65  47180  fourierdlem78  47193  fourierdlem79  47194  sqwvfoura  47237  fourierswlem  47239  fouriersw  47240  etransclem23  47266  etransclem24  47267  etransclem28  47271  etransclem35  47278  etransclem38  47281  nnfoctbdjlem  47464  smfmullem1  47800  sigaradd  47875  chnerlem2  47892  sin3t  47916  cos3t  47917  sin5tlem1  47918  sin5tlem2  47919  sin5tlem4  47921  cos5t  47924  goldratval  47935  cjnpoly  47938  deccarry  48380  ceilbi  48406  flmrecm1  48412  m1modne  48423  m1modmmod  48433  modm1nep2  48443  modm1nem2  48444  fargshiftf1  48522  fargshiftfo  48523  fmtnof1  48619  sqrtpwpw2p  48622  fmtnorec2lem  48626  fmtnorec4  48633  fmtnoprmfac1lem  48648  fmtnoprmfac1  48649  fmtnoprmfac2  48651  2pwp1prm  48673  mod42tp1mod8  48686  sfprmdvdsmersenne  48687  lighneallem3  48691  lighneallem4  48694  ppivalnnprm  48709  ppivalnnnprmge6  48710  onego  48743  zofldiv2ALTV  48759  oexpnegALTV  48774  opoeALTV  48780  opeoALTV  48781  epee  48802  perfectALTVlem1  48818  fppr2odd  48828  fpprwppr  48836  gpg3nbgrvtx0  49173  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  0nodd  49266  2nodd  49268  nnsgrpnmnd  49274  1neven  49334  altgsumbc  49463  pw2m1lepw2m1  49631  zofldiv2  49642  nnpw2pmod  49694  blen1b  49699  blennn0em1  49702  dignn0flhalflem1  49726  dignn0flhalflem2  49727  nn0sumshdiglemB  49731  nn0sumshdiglem1  49732  nn0sumshdiglem2  49733  itcovalpclem2  49782  ackval1  49792  ackval2  49793  ackval3  49794  affineid  49815  1subrec1sub  49816  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  rrx2vlinest  49852  dvsec  50855  dvcsc  50856