Theorem 1cnd 11238

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11135  1c1 11138

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

This theorem is referenced by:  adddirp1d  11269  1p1times  11414  addcom  11429  addcomd  11445  muladd11r  11456  pncan1  11669  npcan1  11670  muls1d  11705  mulsubfacd  11706  recrec  11946  rec11  11947  rec11r  11948  rereccl  11967  subrecd  12078  nn1m1nn  12269  add1p1  12500  sub1m1  12501  cnm2m1cnm3  12502  xp1d2m1eqxm1d2  12503  div4p1lem1div2  12504  nn0n0n1ge2  12577  zneo  12684  rpnnen1lem5  13005  lincmb01cmp  13517  iccf1o  13518  xov1plusxeqvd  13520  zpnn0elfzo1  13760  ubmelm1fzo  13784  fzosplitpr  13797  fzosplitprm1  13798  fzoshftral  13805  fladdz  13847  2tnp1ge0ge0  13851  ltdifltdiv  13856  dfceil2  13861  negmod  13939  modnegd  13949  addmodlteq  13969  binom2sub1  14242  binom3  14245  zesq  14247  sqoddm1div8  14264  bcm1k  14336  bcp1n  14337  bcp1m1  14341  bcpasc  14342  bcn2m1  14345  hashfz  14448  hashfzo  14450  hashfzp1  14452  hashf1lem2  14477  hashf1  14478  hashdifsnp1  14527  lswccatn0lsw  14611  ccatws1lenp1b  14641  revccat  14786  repswrevw  14807  cshwidxm1  14827  cshwidxn  14829  cshweqrep  14841  cshimadifsn0  14851  swrds2m  14962  swrd2lsw  14973  relexpaddnn  15072  absexpz  15326  reccn2  15615  rlimno1  15672  isercolllem1  15683  isercoll2  15687  iseraltlem2  15701  iseraltlem3  15702  fsump1  15774  hashiun  15840  hash2iun1dif1  15842  binomlem  15847  bcxmas  15853  incexc  15855  incexc2  15856  climcndslem1  15867  arisum  15878  arisum2  15879  trireciplem  15880  pwdif  15886  pwm1geoser  15887  geolim2  15889  georeclim  15890  mertenslem1  15902  prodfrec  15913  ntrivcvg  15915  ntrivcvgtail  15918  prodrblem  15947  prodmolem2a  15952  fprodntriv  15960  prod1  15962  fprodser  15967  fprodcl  15970  fprodm1  15985  fprodp1  15987  fprodclf  16010  risefacval2  16028  fallfacval2  16029  risefacp1  16047  fallfacp1  16048  risefacfac  16053  fallfacfwd  16054  binomfallfaclem2  16058  fallfacval4  16061  bpolydiflem  16072  ef0lem  16096  tanaddlem  16184  tanadd  16185  cos01bnd  16204  oddm1even  16362  oddp1even  16363  oexpneg  16364  ltoddhalfle  16380  halfleoddlt  16381  nn0ob  16403  pwp1fsum  16410  flodddiv4  16434  bitsp1o  16452  bitsf1  16465  sadcp1  16474  qredeu  16677  prmdiv  16804  prmdiveq  16805  vfermltlALT  16822  pc2dvds  16899  4sqlem11  16975  4sqlem12  16976  vdwapun  16994  vdwlem3  17003  vdwlem6  17006  vdwlem9  17009  ramub1lem2  17047  prmop1  17058  prmdvdsprmo  17062  prmgaplem8  17078  cshwshashnsame  17123  gsumsgrpccat  18822  psgnunilem5  19480  psgnunilem2  19481  sylow1lem1  19584  efgredlemc  19731  odadd2  19835  ablsimpgfindlem1  20095  srgbinomlem3  20193  srgbinomlem4  20194  cncrng  21363  cncrngOLD  21364  gzrngunit  21413  zringunit  21439  prmirredlem  21445  pzriprnglem12  21465  freshmansdream  21547  mhppwdeg  22102  psdmul  22118  cayhamlem1  22820  expcn  24832  expcnOLD  24834  iirevcn  24893  iihalf2cn  24898  iihalf2cnOLD  24899  icchmeo  24907  icchmeoOLD  24908  icopnfcnv  24909  icopnfhmeo  24910  evth  24927  pcoass  24993  pjthlem1  25407  ovolunlem1a  25467  ovolunlem1  25468  opnmbllem  25572  mbfi1fseqlem6  25691  bddibl  25811  dvnadd  25901  dvmptid  25931  dvmptdiv  25948  dvcnvlem  25950  dveflem  25953  dvef  25954  dvsincos  25955  dvlipcn  25969  dvivthlem1  25983  lhop2  25990  dvcvx  25995  dvfsumle  25996  dvfsumleOLD  25997  dvfsumabs  25999  dvfsumlem1  26002  dvfsumlem2  26003  dvfsumlem2OLD  26004  itgpowd  26027  ply1divex  26112  fta1glem1  26143  dgrcolem1  26249  dgrcolem2  26250  vieta1lem1  26288  aaliou3lem2  26321  aaliou3lem8  26323  dvtaylp  26348  dvntaylp  26349  taylthlem1  26351  taylthlem2  26352  taylthlem2OLD  26353  abelthlem1  26411  abelthlem2  26412  abelthlem6  26416  abelthlem7  26418  logdivlti  26598  advlog  26632  advlogexp  26633  logtayl  26638  cxpmul2  26667  dvcxp1  26718  dvcxp2  26719  dvcncxp1  26721  dvcnsqrt  26722  loglesqrt  26740  relogbdiv  26758  ang180lem4  26791  ang180lem5  26792  isosctrlem2  26798  isosctrlem3  26799  affineequiv  26802  affineequiv2  26803  affineequiv3  26804  angpieqvdlem  26807  chordthmlem2  26812  chordthmlem3  26813  chordthmlem5  26815  dcubic2  26823  dcubic  26825  quart1lem  26834  quart1  26835  quart  26840  asinlem  26847  asinlem3  26850  atansopn  26911  dvatan  26914  leibpi  26921  birthdaylem2  26931  efrlim  26948  efrlimOLD  26949  cxplim  26951  divsqrtsumlem  26959  logdifbnd  26973  emcllem2  26976  emcllem3  26977  emcllem5  26979  zetacvg  26994  lgamgulmlem2  27009  lgamgulmlem3  27010  lgamgulmlem4  27011  lgamgulmlem5  27012  lgamgulmlem6  27013  lgamgulm2  27015  lgamcvg2  27034  gamcvg  27035  gamcvg2lem  27038  lgam1  27043  gamfac  27046  wilthlem2  27048  wilthimp  27051  ftalem5  27056  basellem3  27062  basellem5  27064  basellem8  27067  basellem9  27068  sqff1o  27161  muinv  27172  logfaclbnd  27202  logfacrlim  27204  logexprlim  27205  perfectlem2  27210  dchr1cl  27231  dchrinvcl  27233  dchrfi  27235  dchr1  27237  dchrsum2  27248  bcmono  27257  bcp1ctr  27259  bclbnd  27260  bposlem9  27272  gausslemma2dlem1a  27345  gausslemma2dlem5  27351  lgseisenlem4  27358  lgsquadlem1  27360  m1lgs  27368  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2lgslem3d1  27383  2lgsoddprmlem1  27388  2sqlem8  27406  2sq2  27413  addsqn2reu  27421  addsqrexnreu  27422  addsqnreup  27423  addsq2nreurex  27424  chtppilim  27455  rpvmasumlem  27467  dchrisumlem1  27469  dchrisum0re  27493  dchrisum0lem2a  27497  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  2vmadivsumlem  27520  selberg4lem1  27540  pntrsumo1  27545  selberg34r  27551  pntrlog2bndlem2  27558  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntibndlem2  27571  pntlemg  27578  pntlemr  27582  pntlemf  27585  pntlemk  27586  pntlemo  27587  pntlem3  27589  ostth2lem2  27614  ttgcontlem1  28830  cusgrsize2inds  29399  wlklenvclwlk  29601  pthdadjvtx  29676  crctcshwlkn0lem1  29758  crctcshwlkn0lem4  29761  crctcshwlkn0lem5  29762  wlklnwwlkln2lem  29830  wlknwwlksnbij  29836  wwlksnred  29840  wwlksnext  29841  wwlksnextbi  29842  wwlksnredwwlkn  29843  wwlksnextwrd  29845  wwlksnextinj  29847  wwlksnextproplem2  29858  wwlksnextproplem3  29859  clwwlkccatlem  29936  clwlkclwwlklem2a1  29939  clwlkclwwlklem2a4  29944  clwlkclwwlklem2a  29945  clwlkclwwlklem2  29947  clwlkclwwlklem3  29948  clwlkclwwlk  29949  clwwisshclwwslemlem  29960  clwwisshclwws  29962  clwwlkel  29993  clwwlkf  29994  clwwlkwwlksb  30001  clwwlkext2edg  30003  wwlksext2clwwlk  30004  clwwlknonex2lem1  30054  clwwlknonex2lem2  30055  eucrct2eupth  30192  numclwwlk1lem2foalem  30298  numclwwlk1lem2fo  30305  numclwlk2lem2f  30324  numclwlk2lem2f1o  30326  numclwwlk6  30337  smcnlem  30644  fzm1ne1  32729  bcm1n  32736  fzom1ne1  32742  ltesubnnd  32764  wrdt2ind  32878  chnub  32941  chnlt  32942  omndmul2  33028  psgnfzto1stlem  33059  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2lem7  33091  cycpmco2  33092  archirngz  33135  archiabllem1a  33137  archiabllem2c  33141  ccfldextdgrr  33659  constrfin  33726  nn0constr  33741  iconstr  33746  2sqr3minply  33749  1smat1  33762  madjusmdetlem2  33786  madjusmdetlem4  33788  dya2icoseg  34238  iwrdsplit  34348  fibp1  34362  ballotlemfp1  34453  ballotlemfc0  34454  ballotlemfcc  34455  ballotlemic  34468  ballotlem1c  34469  ballotlemsgt1  34472  ballotlemsdom  34473  ballotlemsel1i  34474  ballotlemsi  34476  ballotlemsima  34477  ballotlem1ri  34496  sgn0bi  34509  signstfvn  34543  signsvtn0  34544  signstfveq0  34551  signsvfn  34556  signsvtn  34558  signshf  34562  hashreprin  34594  circlemeth  34614  logdivsqrle  34624  revpfxsfxrev  35080  revwlk  35089  swrdwlk  35091  subfacp1lem1  35143  subfacp1lem5  35148  cvxpconn  35206  sinccvglem  35636  divcnvlin  35692  bcm1nt  35696  bcprod  35697  bccolsum  35698  iprodgam  35701  faclimlem1  35702  faclimlem2  35703  faclimlem3  35704  faclim  35705  iprodfac  35706  faclim2  35707  fwddifnp1  36125  dnizphlfeqhlf  36436  dnibndlem3  36440  dnibndlem13  36450  unblimceq0  36467  knoppndvlem6  36477  knoppndvlem9  36480  knoppndvlem14  36485  knoppndvlem15  36486  knoppndvlem16  36487  knoppndvlem17  36488  bj-bary1lem1  37271  irrdiff  37286  poimirlem25  37611  poimirlem26  37612  poimirlem32  37618  opnmbllem0  37622  itg2addnclem2  37638  dvasin  37670  dvacos  37671  areacirclem1  37674  areacirclem4  37677  areacirc  37679  bfp  37790  fzsplitnd  41942  lcmfunnnd  41972  lcmineqlem1  41989  lcmineqlem3  41991  lcmineqlem4  41992  lcmineqlem7  41995  lcmineqlem8  41996  lcmineqlem10  41998  lcmineqlem11  41999  lcmineqlem12  42000  lcmineqlem18  42006  lcmineqlem19  42007  lcmineqlem22  42010  lcmineqlem23  42011  dvrelogpow2b  42028  aks4d1p1p4  42031  aks4d1p1p6  42033  aks4d1p1p7  42034  aks4d1p1p5  42035  aks4d1p1  42036  aks4d1p3  42038  aks4d1p7d1  42042  primrootsunit1  42057  posbezout  42060  primrootscoprbij  42062  primrootspoweq0  42066  aks6d1c1  42076  hashscontpow1  42081  2np3bcnp1  42104  sticksstones10  42115  sticksstones12a  42117  sticksstones12  42118  sticksstones16  42122  sticksstones22  42128  aks6d1c6lem3  42132  aks6d1c7lem1  42140  unitscyglem5  42159  metakunt8  42172  metakunt12  42176  metakunt15  42179  metakunt16  42180  metakunt28  42192  nnadd1com  42265  nnaddcom  42266  nnadddir  42268  nnmul1com  42269  nnmulcom  42270  fz1sump1  42307  oddnumth  42308  nicomachus  42309  sumcubes  42310  tan3rdpi  42349  redvmptabs  42353  readvrec  42355  reixi  42415  sn-mullid  42428  sn-0tie0  42432  renegmulnnass  42446  fiabv  42509  fltnltalem  42635  fltnlta  42636  3cubeslem1  42658  3cubeslem2  42659  3cubeslem4  42663  pell1qrge1  42844  rmspecfund  42883  acongeq  42958  jm2.18  42963  jm2.19lem3  42966  jm2.25  42974  jm2.16nn0  42979  jm3.1lem1  42992  jm3.1lem2  42993  areaquad  43191  relexpmulnn  43684  relexpaddss  43693  cvgdvgrat  44289  radcnvrat  44290  hashnzfzclim  44298  ofdivrec  44302  expgrowthi  44309  bccm1k  44318  dvradcnv2  44323  binomcxplemwb  44324  binomcxplemnn0  44325  binomcxplemrat  44326  binomcxplemfrat  44327  binomcxplemdvbinom  44329  binomcxplemnotnn0  44332  refsum2cnlem1  44999  fzisoeu  45269  fperiodmullem  45272  fzdifsuc2  45279  xralrple2  45322  nnsplit  45326  infleinflem2  45339  fmul01lt1lem2  45557  fprodcn  45572  clim1fr1  45573  isumneg  45574  climneg  45582  sumnnodd  45602  reclimc  45625  coseq0  45836  coskpi2  45838  cosknegpi  45841  fprodcncf  45872  fprodsubrecnncnvlem  45879  fprodaddrecnncnvlem  45881  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  dvnxpaek  45914  dvnmul  45915  dvmptfprod  45917  dvnprodlem3  45920  itgsinexp  45927  itgiccshift  45952  itgperiod  45953  itgsbtaddcnst  45954  stoweidlem1  45973  stoweidlem7  45979  stoweidlem10  45982  stoweidlem11  45983  stoweidlem14  45986  stoweidlem17  45989  stoweidlem34  46006  stoweidlem42  46014  wallispilem3  46039  wallispilem5  46041  wallispi  46042  wallispi2lem1  46043  wallispi2lem2  46044  wallispi2  46045  stirlinglem1  46046  stirlinglem3  46048  stirlinglem4  46049  stirlinglem5  46050  stirlinglem6  46051  stirlinglem7  46052  stirlinglem8  46053  stirlinglem10  46055  stirlinglem11  46056  stirlinglem12  46057  stirlinglem13  46058  stirlinglem15  46060  dirkertrigeqlem2  46071  dirkertrigeqlem3  46072  dirkertrigeq  46073  dirkercncflem1  46075  dirkercncflem2  46076  dirkercncflem4  46078  fourierdlem11  46090  fourierdlem15  46094  fourierdlem26  46105  fourierdlem36  46115  fourierdlem40  46119  fourierdlem41  46120  fourierdlem42  46121  fourierdlem48  46126  fourierdlem49  46127  fourierdlem56  46134  fourierdlem58  46136  fourierdlem59  46137  fourierdlem62  46140  fourierdlem64  46142  fourierdlem65  46143  fourierdlem78  46156  fourierdlem79  46157  sqwvfoura  46200  fourierswlem  46202  fouriersw  46203  etransclem23  46229  etransclem24  46230  etransclem28  46234  etransclem35  46241  etransclem38  46244  nnfoctbdjlem  46427  smfmullem1  46763  sigaradd  46838  deccarry  47281  m1modne  47308  fargshiftf1  47386  fargshiftfo  47387  fmtnof1  47480  sqrtpwpw2p  47483  fmtnorec2lem  47487  fmtnorec4  47494  fmtnoprmfac1lem  47509  fmtnoprmfac1  47510  fmtnoprmfac2  47512  2pwp1prm  47534  mod42tp1mod8  47547  sfprmdvdsmersenne  47548  lighneallem3  47552  lighneallem4  47555  onego  47591  zofldiv2ALTV  47607  oexpnegALTV  47622  opoeALTV  47628  opeoALTV  47629  epee  47650  perfectALTVlem1  47666  fppr2odd  47676  fpprwppr  47684  gpg3nbgrvtx0  47990  0nodd  48044  2nodd  48046  nnsgrpnmnd  48052  1neven  48112  altgsumbc  48226  pw2m1lepw2m1  48395  m1modmmod  48400  zofldiv2  48410  nnpw2pmod  48462  blen1b  48467  blennn0em1  48470  dignn0flhalflem1  48494  dignn0flhalflem2  48495  nn0sumshdiglemB  48499  nn0sumshdiglem1  48500  nn0sumshdiglem2  48501  itcovalpclem2  48550  ackval1  48560  ackval2  48561  ackval3  48562  affineid  48583  1subrec1sub  48584  eenglngeehlnmlem1  48616  eenglngeehlnmlem2  48617  rrx2vlinest  48620