Theorem 1cnd 11197

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11093  1c1 11096

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

This theorem is referenced by:  adddirp1d  11230  1p1times  11376  addcom  11391  addcomd  11407  muladd11r  11418  pncan1  11633  npcan1  11634  muls1d  11669  mulsubfacd  11670  recrec  11907  rec11  11908  rec11r  11909  rereccl  11928  subrecd  12039  nn1m1nn  12249  nnadd1com  12254  nnaddcom  12255  nnadddir  12287  nnmul1com  12288  nnmulcom  12289  add1p1  12490  sub1m1  12491  cnm2m1cnm3  12492  xp1d2m1eqxm1d2  12493  div4p1lem1div2  12494  nn0n0n1ge2  12567  zneo  12674  rpnnen1lem5  13000  lincmb01cmp  13517  iccf1o  13518  xov1plusxeqvd  13520  zpnn0elfzo1  13764  ubmelm1fzo  13788  fzosplitpr  13802  fzosplitprm1  13803  fzom1ne1  13810  fzoshftral  13812  fladdz  13854  2tnp1ge0ge0  13858  ltdifltdiv  13863  dfceil2  13868  negmod  13948  modnegd  13958  addmodlteq  13978  binom2sub1  14253  binom3  14256  zesq  14258  sqoddm1div8  14275  bcm1k  14347  bcp1n  14348  bcp1m1  14352  bcpasc  14353  bcn2m1  14356  hashfz  14460  hashfzo  14462  hashfzp1  14464  hashf1lem2  14489  hashf1  14490  hashdifsnp1  14539  lswccatn0lsw  14625  ccatws1lenp1b  14655  revccat  14799  repswrevw  14820  cshwidxm1  14840  cshwidxn  14842  cshweqrep  14854  cshimadifsn0  14863  swrds2m  14974  swrd2lsw  14985  relexpaddnn  15084  sgn0bi  15136  absexpz  15352  reccn2  15644  rlimno1  15701  isercolllem1  15712  isercoll2  15716  iseraltlem2  15730  iseraltlem3  15731  fsump1  15803  fsumconst1  15838  hashiun  15870  hash2iun1dif1  15872  indsumhash  15877  binomlem  15879  bcxmas  15885  incexc  15887  incexc2  15888  climcndslem1  15899  arisum  15910  arisum2  15911  trireciplem  15912  pwdif  15918  pwm1geoser  15919  geolim2  15921  georeclim  15922  mertenslem1  15934  prodfrec  15945  ntrivcvg  15947  ntrivcvgtail  15950  prodrblem  15979  prodmolem2a  15984  fprodntriv  15992  prod1  15994  fprodser  15999  fprodcl  16002  fprodm1  16017  fprodp1  16019  fprodclf  16042  risefacval2  16060  fallfacval2  16061  risefacp1  16078  fallfacp1  16079  risefacfac  16084  fallfacfwd  16085  binomfallfaclem2  16089  fallfacval4  16092  bpolydiflem  16103  ef0lem  16127  tanaddlem  16217  tanadd  16218  cos01bnd  16237  oddm1even  16396  oddp1even  16397  oexpneg  16398  ltoddhalfle  16414  halfleoddlt  16415  nn0ob  16437  pwp1fsum  16444  flodddiv4  16468  bitsp1o  16486  bitsf1  16499  sadcp1  16508  qredeu  16711  prmdiv  16839  prmdiveq  16840  vfermltlALT  16857  pc2dvds  16934  4sqlem11  17010  4sqlem12  17011  vdwapun  17029  vdwlem3  17038  vdwlem6  17041  vdwlem9  17044  ramub1lem2  17082  prmop1  17093  prmdvdsprmo  17097  prmgaplem8  17113  cshwshashnsame  17158  chnub  18673  chnlt  18674  chnccat  18677  chnrev  18678  gsumsgrpccat  18894  psgnunilem5  19559  psgnunilem2  19560  sylow1lem1  19663  efgredlemc  19810  odadd2  19914  ablsimpgfindlem1  20174  omndmul2  20198  srgbinomlem3  20305  srgbinomlem4  20306  cncrng  21543  gzrngunit  21583  zringunit  21616  prmirredlem  21622  pzriprnglem12  21642  freshmansdream  21724  mhppwdeg  22313  psdmul  22329  cayhamlem1  23023  expcn  25031  iirevcn  25089  iihalf2cn  25093  icchmeo  25100  icopnfcnv  25101  icopnfhmeo  25102  evth  25118  pcoass  25183  pjthlem1  25596  ovolunlem1a  25655  ovolunlem1  25656  opnmbllem  25760  mbfi1fseqlem6  25879  bddibl  25999  dvnadd  26088  dvmptid  26116  dvmptdiv  26133  dvcnvlem  26135  dveflem  26138  dvef  26139  dvsincos  26140  dvlipcn  26153  dvivthlem1  26167  lhop2  26174  dvcvx  26179  dvfsumle  26180  dvfsumabs  26182  dvfsumlem1  26185  dvfsumlem2  26186  itgpowd  26209  ply1divex  26294  fta1glem1  26325  dgrcolem1  26430  dgrcolem2  26431  vieta1lem1  26471  aaliou3lem2  26506  aaliou3lem8  26508  dvtaylp  26533  dvntaylp  26534  taylthlem1  26536  taylthlem2  26537  abelthlem1  26594  abelthlem2  26595  abelthlem6  26599  abelthlem7  26601  logdivlti  26785  advlog  26819  advlogexp  26820  logtayl  26825  cxpmul2  26854  dvcxp1  26905  dvcxp2  26906  dvcncxp1  26908  dvcnsqrt  26909  loglesqrt  26926  relogbdiv  26944  ang180lem4  26977  ang180lem5  26978  isosctrlem2  26984  isosctrlem3  26985  affineequiv  26988  affineequiv2  26989  affineequiv3  26990  angpieqvdlem  26993  chordthmlem2  26998  chordthmlem3  26999  chordthmlem5  27001  dcubic2  27009  dcubic  27011  quart1lem  27020  quart1  27021  quart  27026  asinlem  27033  asinlem3  27036  atansopn  27097  dvatan  27100  leibpi  27107  birthdaylem2  27117  efrlim  27134  cxplim  27136  divsqrtsumlem  27144  logdifbnd  27158  emcllem2  27161  emcllem3  27162  emcllem5  27164  zetacvg  27179  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  lgam1  27228  gamfac  27231  wilthlem2  27233  wilthimp  27236  ftalem5  27241  basellem3  27247  basellem5  27249  basellem8  27252  basellem9  27253  sqff1o  27346  muinv  27357  logfaclbnd  27386  logfacrlim  27388  logexprlim  27389  perfectlem2  27394  dchr1cl  27415  dchrinvcl  27417  dchrfi  27419  dchr1  27421  dchrsum2  27432  bcmono  27441  bcp1ctr  27443  bclbnd  27444  bposlem9  27456  gausslemma2dlem1a  27529  gausslemma2dlem5  27535  lgseisenlem4  27542  lgsquadlem1  27544  m1lgs  27552  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgslem3d1  27567  2lgsoddprmlem1  27572  2sqlem8  27590  2sq2  27597  addsqn2reu  27605  addsqrexnreu  27606  addsqnreup  27607  addsq2nreurex  27608  chtppilim  27639  rpvmasumlem  27651  dchrisumlem1  27653  dchrisum0re  27677  dchrisum0lem2a  27681  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  2vmadivsumlem  27704  selberg4lem1  27724  pntrsumo1  27729  selberg34r  27735  pntrlog2bndlem2  27742  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntibndlem2  27755  pntlemg  27762  pntlemr  27766  pntlemf  27769  pntlemk  27770  pntlemo  27771  pntlem3  27773  ostth2lem2  27798  ttgcontlem1  29234  cusgrsize2inds  29803  wlklenvclwlk  30003  pthdadjvtx  30077  crctcshwlkn0lem1  30159  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  wlklnwwlkln2lem  30231  wlknwwlksnbij  30237  wwlksnred  30241  wwlksnext  30242  wwlksnextbi  30243  wwlksnredwwlkn  30244  wwlksnextwrd  30246  wwlksnextinj  30248  wwlksnextproplem2  30259  wwlksnextproplem3  30260  clwwlkccatlem  30340  clwlkclwwlklem2a1  30343  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwlkclwwlklem3  30352  clwlkclwwlk  30353  clwwisshclwwslemlem  30364  clwwisshclwws  30366  clwwlkel  30397  clwwlkf  30398  clwwlkwwlksb  30405  clwwlkext2edg  30407  wwlksext2clwwlk  30408  clwwlknonex2lem1  30458  clwwlknonex2lem2  30459  eucrct2eupth  30596  numclwwlk1lem2foalem  30702  numclwwlk1lem2fo  30709  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  numclwwlk6  30741  smcnlem  31049  receqid  33089  fzm1ne1  33133  bcm1n  33140  ltesubnnd  33167  oexpled  33180  wrdt2ind  33273  gsummptp1  33377  gsummulsubdishift1  33388  psgnfzto1stlem  33420  cycpmco2lem3  33448  cycpmco2lem4  33449  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmco2  33453  archirngz  33509  archiabllem1a  33511  archiabllem2c  33515  gsumind  33665  esplyind  33965  esplyindfv  33966  esplyfvn  33967  vietadeg1  33968  vietalem  33969  ccfldextdgrr  34062  constrfin  34136  nn0constr  34151  iconstr  34156  constrrecl  34159  constrimcl  34160  constrreinvcl  34162  constrinvcl  34163  constrresqrtcl  34167  2sqr3minply  34170  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminply  34178  cos9thpinconstrlem1  34179  1smat1  34194  madjusmdetlem2  34218  madjusmdetlem4  34220  dya2icoseg  34667  iwrdsplit  34777  fibp1  34791  ballotlemfp1  34882  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemic  34897  ballotlem1c  34898  ballotlemsgt1  34901  ballotlemsdom  34902  ballotlemsel1i  34903  ballotlemsi  34905  ballotlemsima  34906  ballotlem1ri  34925  signstfvn  34956  signsvtn0  34957  signstfveq0  34964  signsvfn  34969  signsvtn  34971  signshf  34975  hashreprin  35007  circlemeth  35027  logdivsqrle  35037  revpfxsfxrev  35607  revwlk  35617  swrdwlk  35619  subfacp1lem1  35671  subfacp1lem5  35676  cvxpconn  35734  sinccvglem  36164  divcnvlin  36225  bcm1nt  36229  bcprod  36230  bccolsum  36231  iprodgam  36234  faclimlem1  36235  faclimlem2  36236  faclimlem3  36237  faclim  36238  iprodfac  36239  faclim2  36240  fwddifnp1  36657  dnizphlfeqhlf  37085  dnibndlem3  37089  dnibndlem13  37099  unblimceq0  37116  knoppndvlem6  37126  knoppndvlem9  37129  knoppndvlem14  37134  knoppndvlem15  37135  knoppndvlem16  37136  knoppndvlem17  37137  bj-bary1lem1  37975  irrdiff  37990  qdiff  37991  poimirlem25  38316  poimirlem26  38317  poimirlem32  38323  opnmbllem0  38327  itg2addnclem2  38343  dvasin  38375  dvacos  38376  areacirclem1  38379  areacirclem4  38382  areacirc  38384  bfp  38495  fzsplitnd  42769  lcmfunnnd  42799  lcmineqlem1  42816  lcmineqlem3  42818  lcmineqlem4  42819  lcmineqlem7  42822  lcmineqlem8  42823  lcmineqlem10  42825  lcmineqlem11  42826  lcmineqlem12  42827  lcmineqlem18  42833  lcmineqlem19  42834  lcmineqlem22  42837  lcmineqlem23  42838  dvrelogpow2b  42855  aks4d1p1p4  42858  aks4d1p1p6  42860  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p1  42863  aks4d1p3  42865  aks4d1p7d1  42869  primrootsunit1  42884  posbezout  42887  primrootscoprbij  42889  primrootspoweq0  42893  aks6d1c1  42903  hashscontpow1  42908  2np3bcnp1  42931  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  sticksstones16  42949  sticksstones22  42955  aks6d1c6lem3  42959  aks6d1c7lem1  42967  unitscyglem5  42986  3rdpwhole  43073  fz1sump1  43091  oddnumth  43092  nicomachus  43093  sumcubes  43094  tan3rdpi  43133  redvmptabs  43141  readvrec  43143  reixi  43204  sn-mullid  43217  sn-0tie0  43245  renegmulnnass  43259  fiabv  43324  fltnltalem  43414  fltnlta  43415  3cubeslem1  43435  3cubeslem2  43436  3cubeslem4  43440  pell1qrge1  43617  rmspecfund  43656  acongeq  43730  jm2.18  43735  jm2.19lem3  43738  jm2.25  43746  jm2.16nn0  43751  jm3.1lem1  43764  jm3.1lem2  43765  areaquad  43963  relexpmulnn  44455  relexpaddss  44464  cvgdvgrat  45043  radcnvrat  45044  hashnzfzclim  45052  ofdivrec  45056  expgrowthi  45063  bccm1k  45072  dvradcnv2  45077  binomcxplemwb  45078  binomcxplemnn0  45079  binomcxplemrat  45080  binomcxplemfrat  45081  binomcxplemdvbinom  45083  binomcxplemnotnn0  45086  refsum2cnlem1  45777  fzisoeu  46039  fperiodmullem  46042  fzdifsuc2  46049  xralrple2  46090  nnsplit  46094  infleinflem2  46106  fmul01lt1lem2  46321  fprodcn  46336  clim1fr1  46337  isumneg  46338  climneg  46346  sumnnodd  46366  reclimc  46387  coseq0  46598  coskpi2  46600  cosknegpi  46603  fprodcncf  46634  fprodsubrecnncnvlem  46641  fprodaddrecnncnvlem  46643  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnxpaek  46676  dvnmul  46677  dvmptfprod  46679  dvnprodlem3  46682  itgsinexp  46689  itgiccshift  46714  itgperiod  46715  itgsbtaddcnst  46716  stoweidlem1  46735  stoweidlem7  46741  stoweidlem10  46744  stoweidlem11  46745  stoweidlem14  46748  stoweidlem17  46751  stoweidlem34  46768  stoweidlem42  46776  wallispilem3  46801  wallispilem5  46803  wallispi  46804  wallispi2lem1  46805  wallispi2lem2  46806  wallispi2  46807  stirlinglem1  46808  stirlinglem3  46810  stirlinglem4  46811  stirlinglem5  46812  stirlinglem6  46813  stirlinglem7  46814  stirlinglem8  46815  stirlinglem10  46817  stirlinglem11  46818  stirlinglem12  46819  stirlinglem13  46820  stirlinglem15  46822  dirkertrigeqlem2  46833  dirkertrigeqlem3  46834  dirkertrigeq  46835  dirkercncflem1  46837  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem11  46852  fourierdlem15  46856  fourierdlem26  46867  fourierdlem36  46877  fourierdlem40  46881  fourierdlem41  46882  fourierdlem42  46883  fourierdlem48  46888  fourierdlem49  46889  fourierdlem56  46896  fourierdlem58  46898  fourierdlem59  46899  fourierdlem62  46902  fourierdlem64  46904  fourierdlem65  46905  fourierdlem78  46918  fourierdlem79  46919  sqwvfoura  46962  fourierswlem  46964  fouriersw  46965  etransclem23  46991  etransclem24  46992  etransclem28  46996  etransclem35  47003  etransclem38  47006  nnfoctbdjlem  47189  smfmullem1  47525  sigaradd  47600  chnerlem2  47619  sin3t  47628  cos3t  47629  sin5tlem1  47630  sin5tlem2  47631  sin5tlem4  47633  cos5t  47636  cjnpoly  47646  deccarry  48068  ceilbi  48094  flmrecm1  48100  m1modne  48111  m1modmmod  48121  modm1nep2  48131  modm1nem2  48132  fargshiftf1  48210  fargshiftfo  48211  fmtnof1  48307  sqrtpwpw2p  48310  fmtnorec2lem  48314  fmtnorec4  48321  fmtnoprmfac1lem  48336  fmtnoprmfac1  48337  fmtnoprmfac2  48339  2pwp1prm  48361  mod42tp1mod8  48374  sfprmdvdsmersenne  48375  lighneallem3  48379  lighneallem4  48382  ppivalnnprm  48397  ppivalnnnprmge6  48398  onego  48431  zofldiv2ALTV  48447  oexpnegALTV  48462  opoeALTV  48468  opeoALTV  48469  epee  48490  perfectALTVlem1  48506  fppr2odd  48516  fpprwppr  48524  gpg3nbgrvtx0  48861  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  0nodd  48955  2nodd  48957  nnsgrpnmnd  48963  1neven  49023  altgsumbc  49152  pw2m1lepw2m1  49320  zofldiv2  49331  nnpw2pmod  49383  blen1b  49388  blennn0em1  49391  dignn0flhalflem1  49415  dignn0flhalflem2  49416  nn0sumshdiglemB  49420  nn0sumshdiglem1  49421  nn0sumshdiglem2  49422  itcovalpclem2  49471  ackval1  49481  ackval2  49482  ackval3  49483  affineid  49504  1subrec1sub  49505  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  rrx2vlinest  49541