Theorem 1cnd 10625

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 10524  1c1 10527

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

This theorem is referenced by:  adddirp1d  10656  1p1times  10800  addcom  10815  addcomd  10831  muladd11r  10842  pncan1  11053  npcan1  11054  muls1d  11089  mulsubfacd  11090  recrec  11326  rec11  11327  rec11r  11328  rereccl  11347  subrec  11458  nn1m1nn  11646  add1p1  11876  sub1m1  11877  cnm2m1cnm3  11878  xp1d2m1eqxm1d2  11879  div4p1lem1div2  11880  nn0n0n1ge2  11950  zneo  12053  rpnnen1lem5  12368  lincmb01cmp  12873  iccf1o  12874  xov1plusxeqvd  12876  zpnn0elfzo1  13106  ubmelm1fzo  13128  fzosplitpr  13141  fzosplitprm1  13142  fzoshftral  13149  fladdz  13190  2tnp1ge0ge0  13194  ltdifltdiv  13199  dfceil2  13204  negmod  13279  modnegd  13289  addmodlteq  13309  binom2sub1  13578  binom3  13581  zesq  13583  sqoddm1div8  13600  bcm1k  13671  bcp1n  13672  bcp1m1  13676  bcpasc  13677  bcn2m1  13680  hashfz  13784  hashfzo  13786  hashfzp1  13788  hashf1lem2  13810  hashf1  13811  hashdifsnp1  13850  lswccatn0lsw  13936  ccatws1lenp1b  13966  revccat  14119  repswrevw  14140  cshwidxm1  14160  cshwidxn  14162  cshweqrep  14174  cshimadifsn0  14183  swrds2m  14294  swrd2lsw  14305  relexpaddnn  14402  absexpz  14657  reccn2  14945  rlimno1  15002  isercolllem1  15013  isercoll2  15017  iseraltlem2  15031  iseraltlem3  15032  hashiun  15169  hash2iun1dif1  15171  binomlem  15176  bcxmas  15182  incexc  15184  incexc2  15185  climcndslem1  15196  arisum  15207  arisum2  15208  trireciplem  15209  pwdif  15215  pwm1geoser  15216  pwm1geoserOLD  15217  geolim2  15219  georeclim  15220  mertenslem1  15232  prodfrec  15243  ntrivcvg  15245  ntrivcvgtail  15248  prodrblem  15275  prodmolem2a  15280  fprodntriv  15288  prod1  15290  fprodser  15295  fprodcl  15298  fprodm1  15313  fprodp1  15315  fprodclf  15338  risefacval2  15356  fallfacval2  15357  risefacp1  15375  fallfacp1  15376  risefacfac  15381  fallfacfwd  15382  binomfallfaclem2  15386  fallfacval4  15389  bpolydiflem  15400  ef0lem  15424  tanaddlem  15511  tanadd  15512  cos01bnd  15531  oddm1even  15684  oddp1even  15685  oexpneg  15686  ltoddhalfle  15702  halfleoddlt  15703  nn0ob  15725  pwp1fsum  15732  flodddiv4  15754  bitsp1o  15772  bitsf1  15785  sadcp1  15794  qredeu  15992  prmdiv  16112  prmdiveq  16113  vfermltlALT  16129  pc2dvds  16205  4sqlem11  16281  4sqlem12  16282  vdwapun  16300  vdwlem3  16309  vdwlem6  16312  vdwlem9  16315  ramub1lem2  16353  prmop1  16364  prmdvdsprmo  16368  prmgaplem8  16384  cshwshashnsame  16429  gsumsgrpccat  17996  gsumccatOLD  17997  psgnunilem5  18614  psgnunilem2  18615  sylow1lem1  18715  efgredlemc  18863  odadd2  18962  ablsimpgfindlem1  19222  srgbinomlem3  19285  srgbinomlem4  19286  cncrng  20112  gzrngunit  20157  zringunit  20181  prmirredlem  20186  cayhamlem1  21471  expcn  23477  iirevcn  23535  iihalf2cn  23539  icchmeo  23546  icopnfcnv  23547  icopnfhmeo  23548  evth  23564  pcoass  23629  pjthlem1  24041  ovolunlem1a  24100  ovolunlem1  24101  opnmbllem  24205  mbfi1fseqlem6  24324  bddibl  24443  dvnadd  24532  dvmptid  24560  dvmptdiv  24577  dvcnvlem  24579  dveflem  24582  dvef  24583  dvsincos  24584  dvlipcn  24597  dvivthlem1  24611  lhop2  24618  dvcvx  24623  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem2  24630  itgpowd  24653  ply1divex  24737  fta1glem1  24766  dgrcolem1  24870  dgrcolem2  24871  vieta1lem1  24906  aaliou3lem2  24939  aaliou3lem8  24941  dvtaylp  24965  dvntaylp  24966  taylthlem1  24968  taylthlem2  24969  abelthlem1  25026  abelthlem2  25027  abelthlem6  25031  abelthlem7  25033  logdivlti  25211  advlog  25245  advlogexp  25246  logtayl  25251  cxpmul2  25280  dvcxp1  25329  dvcxp2  25330  dvcncxp1  25332  dvcnsqrt  25333  loglesqrt  25347  relogbdiv  25365  ang180lem4  25398  ang180lem5  25399  isosctrlem2  25405  isosctrlem3  25406  affineequiv  25409  affineequiv2  25410  affineequiv3  25411  angpieqvdlem  25414  chordthmlem2  25419  chordthmlem3  25420  chordthmlem5  25422  dcubic2  25430  dcubic  25432  quart1lem  25441  quart1  25442  quart  25447  asinlem  25454  asinlem3  25457  atansopn  25518  dvatan  25521  leibpi  25528  birthdaylem2  25538  efrlim  25555  cxplim  25557  divsqrtsumlem  25565  logdifbnd  25579  emcllem2  25582  emcllem3  25583  emcllem5  25585  zetacvg  25600  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgamcvg2  25640  gamcvg  25641  gamcvg2lem  25644  lgam1  25649  gamfac  25652  wilthlem2  25654  wilthimp  25657  ftalem5  25662  basellem3  25668  basellem5  25670  basellem8  25673  basellem9  25674  sqff1o  25767  muinv  25778  logfaclbnd  25806  logfacrlim  25808  logexprlim  25809  perfectlem2  25814  dchr1cl  25835  dchrinvcl  25837  dchrfi  25839  dchr1  25841  dchrsum2  25852  bcmono  25861  bcp1ctr  25863  bclbnd  25864  bposlem9  25876  gausslemma2dlem1a  25949  gausslemma2dlem5  25955  lgseisenlem4  25962  lgsquadlem1  25964  m1lgs  25972  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgslem3d1  25987  2lgsoddprmlem1  25992  2sqlem8  26010  2sq2  26017  addsqn2reu  26025  addsqrexnreu  26026  addsqnreup  26027  addsq2nreurex  26028  chtppilim  26059  rpvmasumlem  26071  dchrisumlem1  26073  dchrisum0re  26097  dchrisum0lem2a  26101  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  2vmadivsumlem  26124  selberg4lem1  26144  pntrsumo1  26149  selberg34r  26155  pntrlog2bndlem2  26162  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntibndlem2  26175  pntlemg  26182  pntlemr  26186  pntlemf  26189  pntlemk  26190  pntlemo  26191  pntlem3  26193  ostth2lem2  26218  ttgcontlem1  26679  cusgrsize2inds  27243  wlklenvclwlk  27444  wlklenvclwlkOLD  27445  pthdadjvtx  27519  crctcshwlkn0lem1  27596  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  wlklnwwlkln2lem  27668  wlknwwlksnbij  27674  wwlksnred  27678  wwlksnext  27679  wwlksnextbi  27680  wwlksnredwwlkn  27681  wwlksnextwrd  27683  wwlksnextinj  27685  wwlksnextproplem2  27696  wwlksnextproplem3  27697  clwwlkccatlem  27774  clwlkclwwlklem2a1  27777  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwlkclwwlklem3  27786  clwlkclwwlk  27787  clwwisshclwwslemlem  27798  clwwisshclwws  27800  clwwlkel  27831  clwwlkf  27832  clwwlkwwlksb  27839  clwwlkext2edg  27841  wwlksext2clwwlk  27842  clwwlknonex2lem1  27892  clwwlknonex2lem2  27893  eucrct2eupth  28030  numclwwlk1lem2foalem  28136  numclwwlk1lem2fo  28143  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  numclwwlk6  28175  smcnlem  28480  fzm1ne1  30538  bcm1n  30544  fzom1ne1  30550  ltesubnnd  30564  wrdt2ind  30653  omndmul2  30763  psgnfzto1stlem  30792  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  archirngz  30868  archiabllem1a  30870  archiabllem2c  30874  freshmansdream  30909  ccfldextdgrr  31145  1smat1  31157  madjusmdetlem2  31181  madjusmdetlem4  31183  dya2icoseg  31645  iwrdsplit  31755  fibp1  31769  ballotlemfp1  31859  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemic  31874  ballotlem1c  31875  ballotlemsgt1  31878  ballotlemsdom  31879  ballotlemsel1i  31880  ballotlemsi  31882  ballotlemsima  31883  ballotlem1ri  31902  sgn0bi  31915  signstfvn  31949  signsvtn0  31950  signstfveq0  31957  signsvfn  31962  signsvtn  31964  signshf  31968  hashreprin  32001  circlemeth  32021  logdivsqrle  32031  revpfxsfxrev  32475  revwlk  32484  swrdwlk  32486  subfacp1lem1  32539  subfacp1lem5  32544  cvxpconn  32602  sinccvglem  33028  divcnvlin  33077  bcm1nt  33082  bcprod  33083  bccolsum  33084  iprodgam  33087  faclimlem1  33088  faclimlem2  33089  faclimlem3  33090  faclim  33091  iprodfac  33092  faclim2  33093  fwddifnp1  33739  dnizphlfeqhlf  33928  dnibndlem3  33932  dnibndlem13  33942  unblimceq0  33959  knoppndvlem6  33969  knoppndvlem9  33972  knoppndvlem14  33977  knoppndvlem15  33978  knoppndvlem16  33979  knoppndvlem17  33980  bj-bary1lem1  34725  irrdiff  34740  poimirlem25  35082  poimirlem26  35083  poimirlem32  35089  opnmbllem0  35093  itg2addnclem2  35109  dvasin  35141  dvacos  35142  areacirclem1  35145  areacirclem4  35148  areacirc  35150  bfp  35262  fzsplitnd  39270  lcmfunnnd  39300  lcmineqlem1  39317  lcmineqlem3  39319  lcmineqlem4  39320  lcmineqlem7  39323  lcmineqlem8  39324  lcmineqlem10  39326  lcmineqlem11  39327  lcmineqlem12  39328  lcmineqlem18  39334  lcmineqlem19  39335  lcmineqlem22  39338  lcmineqlem23  39339  2np3bcnp1  39348  metakunt8  39357  metakunt12  39361  metakunt15  39364  metakunt16  39365  metakunt28  39377  nnadd1com  39468  nnaddcom  39469  nnadddir  39471  nnmul1com  39472  nnmulcom  39473  reixi  39559  sn-mulid2  39572  sn-0tie0  39576  fltnltalem  39618  fltnlta  39619  3cubeslem1  39625  3cubeslem2  39626  3cubeslem4  39630  pell1qrge1  39811  rmspecfund  39850  acongeq  39924  jm2.18  39929  jm2.19lem3  39932  jm2.25  39940  jm2.16nn0  39945  jm3.1lem1  39958  jm3.1lem2  39959  areaquad  40166  relexpmulnn  40410  relexpaddss  40419  cvgdvgrat  41017  radcnvrat  41018  hashnzfzclim  41026  ofdivrec  41030  expgrowthi  41037  bccm1k  41046  dvradcnv2  41051  binomcxplemwb  41052  binomcxplemnn0  41053  binomcxplemrat  41054  binomcxplemfrat  41055  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  refsum2cnlem1  41666  fzisoeu  41932  fperiodmullem  41935  fzdifsuc2  41942  xralrple2  41986  nnsplit  41990  infleinflem2  42003  fmul01lt1lem2  42227  fprodcn  42242  clim1fr1  42243  isumneg  42244  climneg  42252  sumnnodd  42272  reclimc  42295  coseq0  42506  coskpi2  42508  cosknegpi  42511  fprodcncf  42542  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnxpaek  42584  dvnmul  42585  dvmptfprod  42587  dvnprodlem3  42590  itgsinexp  42597  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stoweidlem1  42643  stoweidlem7  42649  stoweidlem10  42652  stoweidlem11  42653  stoweidlem14  42656  stoweidlem17  42659  stoweidlem34  42676  stoweidlem42  42684  wallispilem3  42709  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  wallispi2  42715  stirlinglem1  42716  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem6  42721  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  stirlinglem15  42730  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem11  42760  fourierdlem15  42764  fourierdlem26  42775  fourierdlem36  42785  fourierdlem40  42789  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem56  42804  fourierdlem58  42806  fourierdlem59  42807  fourierdlem62  42810  fourierdlem64  42812  fourierdlem65  42813  fourierdlem78  42826  fourierdlem79  42827  sqwvfoura  42870  fourierswlem  42872  fouriersw  42873  etransclem23  42899  etransclem24  42900  etransclem28  42904  etransclem35  42911  etransclem38  42914  nnfoctbdjlem  43094  smfmullem1  43423  sigaradd  43480  deccarry  43868  fargshiftf1  43958  fargshiftfo  43959  fmtnof1  44052  sqrtpwpw2p  44055  fmtnorec2lem  44059  fmtnorec4  44066  fmtnoprmfac1lem  44081  fmtnoprmfac1  44082  fmtnoprmfac2  44084  2pwp1prm  44106  mod42tp1mod8  44120  sfprmdvdsmersenne  44121  lighneallem3  44125  lighneallem4  44128  onego  44164  zofldiv2ALTV  44180  oexpnegALTV  44195  opoeALTV  44201  opeoALTV  44202  epee  44223  perfectALTVlem1  44239  fppr2odd  44249  fpprwppr  44257  0nodd  44430  2nodd  44432  nnsgrpnmnd  44438  1neven  44556  altgsumbc  44754  pw2m1lepw2m1  44929  m1modmmod  44935  zofldiv2  44945  nnpw2pmod  44997  blen1b  45002  blennn0em1  45005  dignn0flhalflem1  45029  dignn0flhalflem2  45030  nn0sumshdiglemB  45034  nn0sumshdiglem1  45035  nn0sumshdiglem2  45036  itcovalpclem2  45085  ackval1  45095  ackval2  45096  ackval3  45097  affineid  45118  1subrec1sub  45119  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  rrx2vlinest  45155