Theorem 1cnd 10979

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  1c1 10881

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

This theorem is referenced by:  adddirp1d  11010  1p1times  11155  addcom  11170  addcomd  11186  muladd11r  11197  pncan1  11408  npcan1  11409  muls1d  11444  mulsubfacd  11445  recrec  11681  rec11  11682  rec11r  11683  rereccl  11702  subrec  11813  nn1m1nn  12003  add1p1  12233  sub1m1  12234  cnm2m1cnm3  12235  xp1d2m1eqxm1d2  12236  div4p1lem1div2  12237  nn0n0n1ge2  12309  zneo  12412  rpnnen1lem5  12730  lincmb01cmp  13236  iccf1o  13237  xov1plusxeqvd  13239  zpnn0elfzo1  13470  ubmelm1fzo  13492  fzosplitpr  13505  fzosplitprm1  13506  fzoshftral  13513  fladdz  13554  2tnp1ge0ge0  13558  ltdifltdiv  13563  dfceil2  13568  negmod  13645  modnegd  13655  addmodlteq  13675  binom2sub1  13945  binom3  13948  zesq  13950  sqoddm1div8  13967  bcm1k  14038  bcp1n  14039  bcp1m1  14043  bcpasc  14044  bcn2m1  14047  hashfz  14151  hashfzo  14153  hashfzp1  14155  hashf1lem2  14179  hashf1  14180  hashdifsnp1  14219  lswccatn0lsw  14305  ccatws1lenp1b  14335  revccat  14488  repswrevw  14509  cshwidxm1  14529  cshwidxn  14531  cshweqrep  14543  cshimadifsn0  14552  swrds2m  14663  swrd2lsw  14674  relexpaddnn  14771  absexpz  15026  reccn2  15315  rlimno1  15374  isercolllem1  15385  isercoll2  15389  iseraltlem2  15403  iseraltlem3  15404  hashiun  15543  hash2iun1dif1  15545  binomlem  15550  bcxmas  15556  incexc  15558  incexc2  15559  climcndslem1  15570  arisum  15581  arisum2  15582  trireciplem  15583  pwdif  15589  pwm1geoser  15590  geolim2  15592  georeclim  15593  mertenslem1  15605  prodfrec  15616  ntrivcvg  15618  ntrivcvgtail  15621  prodrblem  15648  prodmolem2a  15653  fprodntriv  15661  prod1  15663  fprodser  15668  fprodcl  15671  fprodm1  15686  fprodp1  15688  fprodclf  15711  risefacval2  15729  fallfacval2  15730  risefacp1  15748  fallfacp1  15749  risefacfac  15754  fallfacfwd  15755  binomfallfaclem2  15759  fallfacval4  15762  bpolydiflem  15773  ef0lem  15797  tanaddlem  15884  tanadd  15885  cos01bnd  15904  oddm1even  16061  oddp1even  16062  oexpneg  16063  ltoddhalfle  16079  halfleoddlt  16080  nn0ob  16102  pwp1fsum  16109  flodddiv4  16131  bitsp1o  16149  bitsf1  16162  sadcp1  16171  qredeu  16372  prmdiv  16495  prmdiveq  16496  vfermltlALT  16512  pc2dvds  16589  4sqlem11  16665  4sqlem12  16666  vdwapun  16684  vdwlem3  16693  vdwlem6  16696  vdwlem9  16699  ramub1lem2  16737  prmop1  16748  prmdvdsprmo  16752  prmgaplem8  16768  cshwshashnsame  16814  gsumsgrpccat  18487  gsumccatOLD  18488  psgnunilem5  19111  psgnunilem2  19112  sylow1lem1  19212  efgredlemc  19360  odadd2  19459  ablsimpgfindlem1  19719  srgbinomlem3  19787  srgbinomlem4  19788  cncrng  20628  gzrngunit  20673  zringunit  20697  prmirredlem  20703  mhppwdeg  21349  cayhamlem1  22024  expcn  24044  iirevcn  24102  iihalf2cn  24106  icchmeo  24113  icopnfcnv  24114  icopnfhmeo  24115  evth  24131  pcoass  24196  pjthlem1  24610  ovolunlem1a  24669  ovolunlem1  24670  opnmbllem  24774  mbfi1fseqlem6  24894  bddibl  25013  dvnadd  25102  dvmptid  25130  dvmptdiv  25147  dvcnvlem  25149  dveflem  25152  dvef  25153  dvsincos  25154  dvlipcn  25167  dvivthlem1  25181  lhop2  25188  dvcvx  25193  dvfsumle  25194  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem2  25200  itgpowd  25223  ply1divex  25310  fta1glem1  25339  dgrcolem1  25443  dgrcolem2  25444  vieta1lem1  25479  aaliou3lem2  25512  aaliou3lem8  25514  dvtaylp  25538  dvntaylp  25539  taylthlem1  25541  taylthlem2  25542  abelthlem1  25599  abelthlem2  25600  abelthlem6  25604  abelthlem7  25606  logdivlti  25784  advlog  25818  advlogexp  25819  logtayl  25824  cxpmul2  25853  dvcxp1  25902  dvcxp2  25903  dvcncxp1  25905  dvcnsqrt  25906  loglesqrt  25920  relogbdiv  25938  ang180lem4  25971  ang180lem5  25972  isosctrlem2  25978  isosctrlem3  25979  affineequiv  25982  affineequiv2  25983  affineequiv3  25984  angpieqvdlem  25987  chordthmlem2  25992  chordthmlem3  25993  chordthmlem5  25995  dcubic2  26003  dcubic  26005  quart1lem  26014  quart1  26015  quart  26020  asinlem  26027  asinlem3  26030  atansopn  26091  dvatan  26094  leibpi  26101  birthdaylem2  26111  efrlim  26128  cxplim  26130  divsqrtsumlem  26138  logdifbnd  26152  emcllem2  26155  emcllem3  26156  emcllem5  26158  zetacvg  26173  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamgulm2  26194  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  lgam1  26222  gamfac  26225  wilthlem2  26227  wilthimp  26230  ftalem5  26235  basellem3  26241  basellem5  26243  basellem8  26246  basellem9  26247  sqff1o  26340  muinv  26351  logfaclbnd  26379  logfacrlim  26381  logexprlim  26382  perfectlem2  26387  dchr1cl  26408  dchrinvcl  26410  dchrfi  26412  dchr1  26414  dchrsum2  26425  bcmono  26434  bcp1ctr  26436  bclbnd  26437  bposlem9  26449  gausslemma2dlem1a  26522  gausslemma2dlem5  26528  lgseisenlem4  26535  lgsquadlem1  26537  m1lgs  26545  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2lgslem3d1  26560  2lgsoddprmlem1  26565  2sqlem8  26583  2sq2  26590  addsqn2reu  26598  addsqrexnreu  26599  addsqnreup  26600  addsq2nreurex  26601  chtppilim  26632  rpvmasumlem  26644  dchrisumlem1  26646  dchrisum0re  26670  dchrisum0lem2a  26674  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  2vmadivsumlem  26697  selberg4lem1  26717  pntrsumo1  26722  selberg34r  26728  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntibndlem2  26748  pntlemg  26755  pntlemr  26759  pntlemf  26762  pntlemk  26763  pntlemo  26764  pntlem3  26766  ostth2lem2  26791  ttgcontlem1  27261  cusgrsize2inds  27829  wlklenvclwlk  28031  wlklenvclwlkOLD  28032  pthdadjvtx  28107  crctcshwlkn0lem1  28184  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  wlklnwwlkln2lem  28256  wlknwwlksnbij  28262  wwlksnred  28266  wwlksnext  28267  wwlksnextbi  28268  wwlksnredwwlkn  28269  wwlksnextwrd  28271  wwlksnextinj  28273  wwlksnextproplem2  28284  wwlksnextproplem3  28285  clwwlkccatlem  28362  clwlkclwwlklem2a1  28365  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwlkclwwlklem3  28374  clwlkclwwlk  28375  clwwisshclwwslemlem  28386  clwwisshclwws  28388  clwwlkel  28419  clwwlkf  28420  clwwlkwwlksb  28427  clwwlkext2edg  28429  wwlksext2clwwlk  28430  clwwlknonex2lem1  28480  clwwlknonex2lem2  28481  eucrct2eupth  28618  numclwwlk1lem2foalem  28724  numclwwlk1lem2fo  28731  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  numclwwlk6  28763  smcnlem  29068  fzm1ne1  31119  bcm1n  31125  fzom1ne1  31131  ltesubnnd  31145  wrdt2ind  31234  omndmul2  31347  psgnfzto1stlem  31376  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  archirngz  31452  archiabllem1a  31454  archiabllem2c  31458  freshmansdream  31493  ccfldextdgrr  31751  1smat1  31763  madjusmdetlem2  31787  madjusmdetlem4  31789  dya2icoseg  32253  iwrdsplit  32363  fibp1  32377  ballotlemfp1  32467  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemic  32482  ballotlem1c  32483  ballotlemsgt1  32486  ballotlemsdom  32487  ballotlemsel1i  32488  ballotlemsi  32490  ballotlemsima  32491  ballotlem1ri  32510  sgn0bi  32523  signstfvn  32557  signsvtn0  32558  signstfveq0  32565  signsvfn  32570  signsvtn  32572  signshf  32576  hashreprin  32609  circlemeth  32629  logdivsqrle  32639  revpfxsfxrev  33086  revwlk  33095  swrdwlk  33097  subfacp1lem1  33150  subfacp1lem5  33155  cvxpconn  33213  sinccvglem  33639  divcnvlin  33707  bcm1nt  33712  bcprod  33713  bccolsum  33714  iprodgam  33717  faclimlem1  33718  faclimlem2  33719  faclimlem3  33720  faclim  33721  iprodfac  33722  faclim2  33723  fwddifnp1  34476  dnizphlfeqhlf  34665  dnibndlem3  34669  dnibndlem13  34679  unblimceq0  34696  knoppndvlem6  34706  knoppndvlem9  34709  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem16  34716  knoppndvlem17  34717  bj-bary1lem1  35491  irrdiff  35506  poimirlem25  35811  poimirlem26  35812  poimirlem32  35818  opnmbllem0  35822  itg2addnclem2  35838  dvasin  35870  dvacos  35871  areacirclem1  35874  areacirclem4  35877  areacirc  35879  bfp  35991  fzsplitnd  39998  lcmfunnnd  40027  lcmineqlem1  40044  lcmineqlem3  40046  lcmineqlem4  40047  lcmineqlem7  40050  lcmineqlem8  40051  lcmineqlem10  40053  lcmineqlem11  40054  lcmineqlem12  40055  lcmineqlem18  40061  lcmineqlem19  40062  lcmineqlem22  40065  lcmineqlem23  40066  dvrelogpow2b  40083  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p3  40093  aks4d1p7d1  40097  2np3bcnp1  40107  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones16  40125  sticksstones22  40131  metakunt8  40139  metakunt12  40143  metakunt15  40146  metakunt16  40147  metakunt28  40159  nnadd1com  40304  nnaddcom  40305  nnadddir  40307  nnmul1com  40308  nnmulcom  40309  reixi  40411  sn-mulid2  40424  sn-0tie0  40428  fltnltalem  40506  fltnlta  40507  3cubeslem1  40513  3cubeslem2  40514  3cubeslem4  40518  pell1qrge1  40699  rmspecfund  40738  acongeq  40812  jm2.18  40817  jm2.19lem3  40820  jm2.25  40828  jm2.16nn0  40833  jm3.1lem1  40846  jm3.1lem2  40847  areaquad  41054  relexpmulnn  41324  relexpaddss  41333  cvgdvgrat  41938  radcnvrat  41939  hashnzfzclim  41947  ofdivrec  41951  expgrowthi  41958  bccm1k  41967  dvradcnv2  41972  binomcxplemwb  41973  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  refsum2cnlem1  42587  fzisoeu  42846  fperiodmullem  42849  fzdifsuc2  42856  xralrple2  42900  nnsplit  42904  infleinflem2  42917  fmul01lt1lem2  43133  fprodcn  43148  clim1fr1  43149  isumneg  43150  climneg  43158  sumnnodd  43178  reclimc  43201  coseq0  43412  coskpi2  43414  cosknegpi  43417  fprodcncf  43448  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnxpaek  43490  dvnmul  43491  dvmptfprod  43493  dvnprodlem3  43496  itgsinexp  43503  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem1  43549  stoweidlem7  43555  stoweidlem10  43558  stoweidlem11  43559  stoweidlem14  43562  stoweidlem17  43565  stoweidlem34  43582  stoweidlem42  43590  wallispilem3  43615  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem15  43636  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem11  43666  fourierdlem15  43670  fourierdlem26  43681  fourierdlem36  43691  fourierdlem40  43695  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem56  43710  fourierdlem58  43712  fourierdlem59  43713  fourierdlem62  43716  fourierdlem64  43718  fourierdlem65  43719  fourierdlem78  43732  fourierdlem79  43733  sqwvfoura  43776  fourierswlem  43778  fouriersw  43779  etransclem23  43805  etransclem24  43806  etransclem28  43810  etransclem35  43817  etransclem38  43820  nnfoctbdjlem  44000  smfmullem1  44336  sigaradd  44393  deccarry  44814  fargshiftf1  44904  fargshiftfo  44905  fmtnof1  44998  sqrtpwpw2p  45001  fmtnorec2lem  45005  fmtnorec4  45012  fmtnoprmfac1lem  45027  fmtnoprmfac1  45028  fmtnoprmfac2  45030  2pwp1prm  45052  mod42tp1mod8  45065  sfprmdvdsmersenne  45066  lighneallem3  45070  lighneallem4  45073  onego  45109  zofldiv2ALTV  45125  oexpnegALTV  45140  opoeALTV  45146  opeoALTV  45147  epee  45168  perfectALTVlem1  45184  fppr2odd  45194  fpprwppr  45202  0nodd  45375  2nodd  45377  nnsgrpnmnd  45383  1neven  45501  altgsumbc  45699  pw2m1lepw2m1  45872  m1modmmod  45878  zofldiv2  45888  nnpw2pmod  45940  blen1b  45945  blennn0em1  45948  dignn0flhalflem1  45972  dignn0flhalflem2  45973  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978  nn0sumshdiglem2  45979  itcovalpclem2  46028  ackval1  46038  ackval2  46039  ackval3  46040  affineid  46061  1subrec1sub  46062  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2vlinest  46098