Theorem 1cnd 11227

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

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

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

This theorem is used by:  adddirp1d  11260  1p1times  11406  addcom  11421  addcomd  11437  muladd11r  11448  pncan1  11663  npcan1  11664  muls1d  11699  mulsubfacd  11700  recrec  11937  rec11  11938  rec11r  11939  rereccl  11958  subrecd  12069  nn1m1nn  12279  nnadd1com  12284  nnaddcom  12285  nnadddir  12317  nnmul1com  12318  nnmulcom  12319  add1p1  12520  sub1m1  12521  cnm2m1cnm3  12522  xp1d2m1eqxm1d2  12523  div4p1lem1div2  12524  nn0n0n1ge2  12597  zneo  12705  rpnnen1lem5  13032  lincmb01cmp  13549  iccf1o  13550  xov1plusxeqvd  13552  zpnn0elfzo1  13796  ubmelm1fzo  13820  fzosplitpr  13834  fzosplitprm1  13835  fzom1ne1  13842  fzoshftral  13844  fladdz  13887  2tnp1ge0ge0  13891  ltdifltdiv  13896  dfceil2  13901  negmod  13981  modnegd  13991  addmodlteq  14011  binom2sub1  14286  binom3  14289  zesq  14291  sqoddm1div8  14308  bcm1k  14380  bcp1n  14381  bcp1m1  14385  bcpasc  14386  bcn2m1  14389  hashfz  14493  hashfzo  14495  hashfzp1  14497  hashf1lem2  14522  hashf1  14523  hashdifsnp1  14572  lswccatn0lsw  14659  ccatws1lenp1b  14690  revccat  14836  revpfxsfxrev  14838  repswrevw  14859  cshwidxm1  14879  cshwidxn  14881  cshweqrep  14893  cshimadifsn0  14902  swrds2m  15013  swrd2lsw  15026  relexpaddnn  15125  sgn0bi  15177  absexpz  15393  reccn2  15685  rlimno1  15742  isercolllem1  15753  isercoll2  15757  iseraltlem2  15771  iseraltlem3  15772  fsump1  15843  fsumconst1  15878  hashiun  15910  hash2iun1dif1  15912  indsumhash  15917  binomlem  15919  bcxmas  15925  incexc  15927  incexc2  15928  climcndslem1  15939  arisum  15950  arisum2  15951  trireciplem  15952  pwdif  15958  pwm1geoser  15959  geolim2  15961  georeclim  15962  mertenslem1  15974  prodfrec  15985  ntrivcvg  15987  ntrivcvgtail  15990  prodrblem  16017  prodmolem2a  16022  fprodntriv  16030  prod1  16032  fprodser  16037  fprodcl  16040  fprodm1  16055  fprodp1  16057  fprodclf  16080  risefacval2  16098  fallfacval2  16099  risefacp1  16116  fallfacp1  16117  risefacfac  16122  fallfacfwd  16123  binomfallfaclem2  16127  fallfacval4  16130  bpolydiflem  16141  ef0lem  16165  tanaddlem  16255  tanadd  16256  cos01bnd  16275  oddm1even  16434  oddp1even  16435  oexpneg  16436  ltoddhalfle  16452  halfleoddlt  16453  nn0ob  16475  pwp1fsum  16482  flodddiv4  16506  bitsp1o  16524  bitsf1  16537  sadcp1  16546  qredeu  16749  prmdiv  16877  prmdiveq  16878  vfermltlALT  16895  pc2dvds  16972  4sqlem11  17048  4sqlem12  17049  vdwapun  17067  vdwlem3  17076  vdwlem6  17079  vdwlem9  17082  ramub1lem2  17120  prmop1  17131  prmdvdsprmo  17135  prmgaplem8  17151  cshwshashnsame  17196  chnub  18711  chnlt  18712  chnccat  18715  chnrev  18716  gsumsgrpccat  18950  psgnunilem5  19622  psgnunilem2  19623  sylow1lem1  19726  efgredlemc  19873  odadd2  19977  ablsimpgfindlem1  20237  omndmul2  20261  srgbinomlem3  20368  srgbinomlem4  20369  cncrng  21607  gzrngunit  21647  zringunit  21680  prmirredlem  21686  pzriprnglem12  21706  freshmansdream  21788  mhppwdeg  22379  psdmul  22395  cayhamlem1  23092  expcn  25101  iirevcn  25159  iihalf2cn  25163  icchmeo  25170  icopnfcnv  25171  icopnfhmeo  25172  evth  25188  pcoass  25253  pjthlem1  25666  ovolunlem1a  25725  ovolunlem1  25726  opnmbllem  25830  mbfi1fseqlem6  25949  bddibl  26068  dvnadd  26157  dvmptid  26185  dvmptdiv  26202  dvcnvlem  26204  dveflem  26207  dvef  26208  dvsincos  26209  dvlipcn  26222  dvivthlem1  26236  lhop2  26243  dvcvx  26248  dvfsumle  26249  dvfsumabs  26251  dvfsumlem1  26254  dvfsumlem2  26255  itgpowd  26278  ply1divex  26363  fta1glem1  26394  dgrcolem1  26500  dgrcolem2  26501  vieta1lem1  26543  aaliou3lem2  26580  aaliou3lem8  26582  dvtaylp  26607  dvntaylp  26608  taylthlem1  26610  taylthlem2  26611  abelthlem1  26668  abelthlem2  26669  abelthlem6  26673  abelthlem7  26675  logdivlti  26858  advlog  26892  advlogexp  26893  logtayl  26898  cxpmul2  26927  dvcxp1  26978  dvcxp2  26979  dvcncxp1  26981  dvcnsqrt  26982  loglesqrt  26999  relogbdiv  27017  ang180lem4  27050  ang180lem5  27051  isosctrlem2  27057  isosctrlem3  27058  affineequiv  27061  affineequiv2  27062  affineequiv3  27063  angpieqvdlem  27066  chordthmlem2  27071  chordthmlem3  27072  chordthmlem5  27074  dcubic2  27082  dcubic  27084  quart1lem  27093  quart1  27094  quart  27099  asinlem  27106  asinlem3  27109  atansopn  27170  dvatan  27173  leibpi  27180  birthdaylem2  27190  efrlim  27207  cxplim  27209  divsqrtsumlem  27217  logdifbnd  27231  emcllem2  27234  emcllem3  27235  emcllem5  27237  zetacvg  27252  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamgulmlem4  27269  lgamgulmlem5  27270  lgamgulmlem6  27271  lgamgulm2  27273  lgamcvg2  27292  gamcvg  27293  gamcvg2lem  27296  lgam1  27301  gamfac  27304  wilthlem2  27306  wilthimp  27309  ftalem5  27314  basellem3  27320  basellem5  27322  basellem8  27325  basellem9  27326  sqff1o  27419  muinv  27430  logfaclbnd  27459  logfacrlim  27461  logexprlim  27462  perfectlem2  27467  dchr1cl  27488  dchrinvcl  27490  dchrfi  27492  dchr1  27494  dchrsum2  27505  bcmono  27514  bcp1ctr  27516  bclbnd  27517  bposlem9  27529  gausslemma2dlem1a  27602  gausslemma2dlem5  27608  lgseisenlem4  27615  lgsquadlem1  27617  m1lgs  27625  2lgslem3a  27633  2lgslem3b  27634  2lgslem3c  27635  2lgslem3d  27636  2lgslem3d1  27640  2lgsoddprmlem1  27645  2sqlem8  27663  2sq2  27670  addsqn2reu  27678  addsqrexnreu  27679  addsqnreup  27680  addsq2nreurex  27681  chtppilim  27712  rpvmasumlem  27724  dchrisumlem1  27726  dchrisum0re  27750  dchrisum0lem2a  27754  mudivsum  27767  mulogsumlem  27768  mulogsum  27769  2vmadivsumlem  27777  selberg4lem1  27797  pntrsumo1  27802  selberg34r  27808  pntrlog2bndlem2  27815  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntrlog2bndlem6  27820  pntibndlem2  27828  pntlemg  27835  pntlemr  27839  pntlemf  27842  pntlemk  27843  pntlemo  27844  pntlem3  27846  ostth2lem2  27871  ttgcontlem1  29342  cusgrsize2inds  29914  wlklenvclwlk  30114  revwlk  30147  swrdwlk  30148  pthdadjvtx  30193  crctcshwlkn0lem1  30279  crctcshwlkn0lem4  30282  crctcshwlkn0lem5  30283  wlklnwwlkln2lem  30351  wlknwwlksnbij  30357  wwlksnred  30361  wwlksnext  30362  wwlksnextbi  30363  wwlksnredwwlkn  30364  wwlksnextwrd  30366  wwlksnextinj  30368  wwlksnextproplem2  30379  wwlksnextproplem3  30380  clwwlkccatlem  30460  clwlkclwwlklem2a1  30463  clwlkclwwlklem2a4  30468  clwlkclwwlklem2a  30469  clwlkclwwlklem2  30471  clwlkclwwlklem3  30472  clwlkclwwlk  30473  clwwisshclwwslemlem  30484  clwwisshclwws  30486  clwwlkel  30517  clwwlkf  30518  clwwlkwwlksb  30525  clwwlkext2edg  30527  wwlksext2clwwlk  30528  clwwlknonex2lem1  30578  clwwlknonex2lem2  30579  eucrct2eupth  30726  numclwwlk1lem2foalem  30832  numclwwlk1lem2fo  30839  numclwlk2lem2f  30858  numclwlk2lem2f1o  30860  numclwwlk6  30871  smcnlem  31179  receqid  33216  fzm1ne1  33260  bcm1n  33267  ltesubnnd  33294  oexpled  33307  wrdt2ind  33396  gsummptp1  33498  gsummulsubdishift1  33509  psgnfzto1stlem  33541  cycpmco2lem3  33569  cycpmco2lem4  33570  cycpmco2lem5  33571  cycpmco2lem6  33572  cycpmco2lem7  33573  cycpmco2  33574  archirngz  33630  archiabllem1a  33632  archiabllem2c  33636  gsumind  33786  esplyind  34086  esplyindfv  34087  esplyfvn  34088  vietadeg1  34089  vietalem  34090  ccfldextdgrr  34183  constrfin  34257  nn0constr  34272  iconstr  34277  constrrecl  34280  constrimcl  34281  constrreinvcl  34283  constrinvcl  34284  constrresqrtcl  34288  2sqr3minply  34291  cos9thpiminplylem1  34293  cos9thpiminplylem2  34294  cos9thpiminplylem3  34295  cos9thpiminply  34299  cos9thpinconstrlem1  34300  1smat1  34315  madjusmdetlem2  34339  madjusmdetlem4  34341  dya2icoseg  34789  iwrdsplit  34899  fibp1  34913  ballotlemfp1  35004  ballotlemfc0  35005  ballotlemfcc  35006  ballotlemic  35019  ballotlem1c  35020  ballotlemsgt1  35023  ballotlemsdom  35024  ballotlemsel1i  35025  ballotlemsi  35027  ballotlemsima  35028  ballotlem1ri  35047  signstfvn  35078  signsvtn0  35079  signstfveq0  35086  signsvfn  35091  signsvtn  35093  signshf  35097  hashreprin  35129  circlemeth  35149  logdivsqrle  35159  subfacp1lem1  35759  subfacp1lem5  35764  cvxpconn  35822  sinccvglem  36252  divcnvlin  36313  bcm1nt  36317  bcprod  36318  bccolsum  36319  iprodgam  36322  faclimlem1  36323  faclimlem2  36324  faclimlem3  36325  faclim  36326  iprodfac  36327  faclim2  36328  fwddifnp1  36746  dnizphlfeqhlf  37174  dnibndlem3  37178  dnibndlem13  37188  unblimceq0  37205  knoppndvlem6  37215  knoppndvlem9  37218  knoppndvlem14  37223  knoppndvlem15  37224  knoppndvlem16  37225  knoppndvlem17  37226  bj-bary1lem1  38064  irrdiff  38079  qdiff  38080  poimirlem25  38395  poimirlem26  38396  poimirlem32  38402  opnmbllem0  38406  itg2addnclem2  38422  dvasin  38454  dvacos  38455  areacirclem1  38458  areacirclem4  38461  areacirc  38463  bfp  38575  fzsplitnd  42849  lcmfunnnd  42879  lcmineqlem1  42896  lcmineqlem3  42898  lcmineqlem4  42899  lcmineqlem7  42902  lcmineqlem8  42903  lcmineqlem10  42905  lcmineqlem11  42906  lcmineqlem12  42907  lcmineqlem18  42913  lcmineqlem19  42914  lcmineqlem22  42917  lcmineqlem23  42918  dvrelogpow2b  42935  aks4d1p1p4  42938  aks4d1p1p6  42940  aks4d1p1p7  42941  aks4d1p1p5  42942  aks4d1p1  42943  aks4d1p3  42945  aks4d1p7d1  42949  primrootsunit1  42964  posbezout  42967  primrootscoprbij  42969  primrootspoweq0  42973  aks6d1c1  42983  hashscontpow1  42988  2np3bcnp1  43011  sticksstones10  43022  sticksstones12a  43024  sticksstones12  43025  sticksstones16  43029  sticksstones22  43035  aks6d1c6lem3  43039  aks6d1c7lem1  43047  unitscyglem5  43066  3rdpwhole  43168  fz1sump1  43186  oddnumth  43187  nicomachus  43188  sumcubes  43189  tan3rdpi  43228  redvmptabs  43236  readvrec  43238  reixi  43299  sn-mullid  43312  sn-0tie0  43340  renegmulnnass  43354  fiabv  43419  fltnltalem  43509  fltnlta  43510  3cubeslem1  43530  3cubeslem2  43531  3cubeslem4  43535  pell1qrge1  43712  rmspecfund  43751  acongeq  43825  jm2.18  43830  jm2.19lem3  43833  jm2.25  43841  jm2.16nn0  43846  jm3.1lem1  43859  jm3.1lem2  43860  areaquad  44058  relexpmulnn  44550  relexpaddss  44559  cvgdvgrat  45138  radcnvrat  45139  hashnzfzclim  45147  ofdivrec  45151  expgrowthi  45158  bccm1k  45167  dvradcnv2  45172  binomcxplemwb  45173  binomcxplemnn0  45174  binomcxplemrat  45175  binomcxplemfrat  45176  binomcxplemdvbinom  45178  binomcxplemnotnn0  45181  refsum2cnlem1  45872  fzisoeu  46134  fperiodmullem  46137  fzdifsuc2  46144  xralrple2  46185  nnsplit  46189  infleinflem2  46201  fmul01lt1lem2  46416  fprodcn  46431  clim1fr1  46432  isumneg  46433  climneg  46441  sumnnodd  46461  reclimc  46482  coseq0  46693  coskpi2  46695  cosknegpi  46698  fprodcncf  46729  fprodsubrecnncnvlem  46736  fprodaddrecnncnvlem  46738  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnxpaek  46771  dvnmul  46772  dvmptfprod  46774  dvnprodlem3  46777  itgsinexp  46784  itgiccshift  46809  itgperiod  46810  itgsbtaddcnst  46811  stoweidlem1  46830  stoweidlem7  46836  stoweidlem10  46839  stoweidlem11  46840  stoweidlem14  46843  stoweidlem17  46846  stoweidlem34  46863  stoweidlem42  46871  wallispilem3  46896  wallispilem5  46898  wallispi  46899  wallispi2lem1  46900  wallispi2lem2  46901  wallispi2  46902  stirlinglem1  46903  stirlinglem3  46905  stirlinglem4  46906  stirlinglem5  46907  stirlinglem6  46908  stirlinglem7  46909  stirlinglem8  46910  stirlinglem10  46912  stirlinglem11  46913  stirlinglem12  46914  stirlinglem13  46915  stirlinglem15  46917  dirkertrigeqlem2  46928  dirkertrigeqlem3  46929  dirkertrigeq  46930  dirkercncflem1  46932  dirkercncflem2  46933  dirkercncflem4  46935  fourierdlem11  46947  fourierdlem15  46951  fourierdlem26  46962  fourierdlem36  46972  fourierdlem40  46976  fourierdlem41  46977  fourierdlem42  46978  fourierdlem48  46983  fourierdlem49  46984  fourierdlem56  46991  fourierdlem58  46993  fourierdlem59  46994  fourierdlem62  46997  fourierdlem64  46999  fourierdlem65  47000  fourierdlem78  47013  fourierdlem79  47014  sqwvfoura  47057  fourierswlem  47059  fouriersw  47060  etransclem23  47086  etransclem24  47087  etransclem28  47091  etransclem35  47098  etransclem38  47101  nnfoctbdjlem  47284  smfmullem1  47620  sigaradd  47695  chnerlem2  47712  sin3t  47736  cos3t  47737  sin5tlem1  47738  sin5tlem2  47739  sin5tlem4  47741  cos5t  47744  goldratval  47755  cjnpoly  47758  deccarry  48200  ceilbi  48226  flmrecm1  48232  m1modne  48243  m1modmmod  48253  modm1nep2  48263  modm1nem2  48264  fargshiftf1  48342  fargshiftfo  48343  fmtnof1  48439  sqrtpwpw2p  48442  fmtnorec2lem  48446  fmtnorec4  48453  fmtnoprmfac1lem  48468  fmtnoprmfac1  48469  fmtnoprmfac2  48471  2pwp1prm  48493  mod42tp1mod8  48506  sfprmdvdsmersenne  48507  lighneallem3  48511  lighneallem4  48514  ppivalnnprm  48529  ppivalnnnprmge6  48530  onego  48563  zofldiv2ALTV  48579  oexpnegALTV  48594  opoeALTV  48600  opeoALTV  48601  epee  48622  perfectALTVlem1  48638  fppr2odd  48648  fpprwppr  48656  gpg3nbgrvtx0  48993  pgnbgreunbgrlem2lem1  49031  pgnbgreunbgrlem2lem2  49032  0nodd  49086  2nodd  49088  nnsgrpnmnd  49094  1neven  49154  altgsumbc  49283  pw2m1lepw2m1  49451  zofldiv2  49462  nnpw2pmod  49514  blen1b  49519  blennn0em1  49522  dignn0flhalflem1  49546  dignn0flhalflem2  49547  nn0sumshdiglemB  49551  nn0sumshdiglem1  49552  nn0sumshdiglem2  49553  itcovalpclem2  49602  ackval1  49612  ackval2  49613  ackval3  49614  affineid  49635  1subrec1sub  49636  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  rrx2vlinest  49672  dvsec  50690  dvcsc  50691