Theorem 1cnd 11139

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  1c1 11039

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

This theorem is referenced by:  adddirp1d  11170  1p1times  11316  addcom  11331  addcomd  11347  muladd11r  11358  pncan1  11573  npcan1  11574  muls1d  11609  mulsubfacd  11610  recrec  11850  rec11  11851  rec11r  11852  rereccl  11871  subrecd  11982  nn1m1nn  12178  add1p1  12404  sub1m1  12405  cnm2m1cnm3  12406  xp1d2m1eqxm1d2  12407  div4p1lem1div2  12408  nn0n0n1ge2  12481  zneo  12587  rpnnen1lem5  12906  lincmb01cmp  13423  iccf1o  13424  xov1plusxeqvd  13426  zpnn0elfzo1  13667  ubmelm1fzo  13691  fzosplitpr  13705  fzosplitprm1  13706  fzom1ne1  13713  fzoshftral  13715  fladdz  13757  2tnp1ge0ge0  13761  ltdifltdiv  13766  dfceil2  13771  negmod  13851  modnegd  13861  addmodlteq  13881  binom2sub1  14156  binom3  14159  zesq  14161  sqoddm1div8  14178  bcm1k  14250  bcp1n  14251  bcp1m1  14255  bcpasc  14256  bcn2m1  14259  hashfz  14362  hashfzo  14364  hashfzp1  14366  hashf1lem2  14391  hashf1  14392  hashdifsnp1  14441  lswccatn0lsw  14527  ccatws1lenp1b  14557  revccat  14701  repswrevw  14722  cshwidxm1  14742  cshwidxn  14744  cshweqrep  14756  cshimadifsn0  14765  swrds2m  14876  swrd2lsw  14887  relexpaddnn  14986  absexpz  15240  reccn2  15532  rlimno1  15589  isercolllem1  15600  isercoll2  15604  iseraltlem2  15618  iseraltlem3  15619  fsump1  15691  hashiun  15757  hash2iun1dif1  15759  binomlem  15764  bcxmas  15770  incexc  15772  incexc2  15773  climcndslem1  15784  arisum  15795  arisum2  15796  trireciplem  15797  pwdif  15803  pwm1geoser  15804  geolim2  15806  georeclim  15807  mertenslem1  15819  prodfrec  15830  ntrivcvg  15832  ntrivcvgtail  15835  prodrblem  15864  prodmolem2a  15869  fprodntriv  15877  prod1  15879  fprodser  15884  fprodcl  15887  fprodm1  15902  fprodp1  15904  fprodclf  15927  risefacval2  15945  fallfacval2  15946  risefacp1  15964  fallfacp1  15965  risefacfac  15970  fallfacfwd  15971  binomfallfaclem2  15975  fallfacval4  15978  bpolydiflem  15989  ef0lem  16013  tanaddlem  16103  tanadd  16104  cos01bnd  16123  oddm1even  16282  oddp1even  16283  oexpneg  16284  ltoddhalfle  16300  halfleoddlt  16301  nn0ob  16323  pwp1fsum  16330  flodddiv4  16354  bitsp1o  16372  bitsf1  16385  sadcp1  16394  qredeu  16597  prmdiv  16724  prmdiveq  16725  vfermltlALT  16742  pc2dvds  16819  4sqlem11  16895  4sqlem12  16896  vdwapun  16914  vdwlem3  16923  vdwlem6  16926  vdwlem9  16929  ramub1lem2  16967  prmop1  16978  prmdvdsprmo  16982  prmgaplem8  16998  cshwshashnsame  17043  chnub  18557  chnlt  18558  chnccat  18561  chnrev  18562  gsumsgrpccat  18777  psgnunilem5  19435  psgnunilem2  19436  sylow1lem1  19539  efgredlemc  19686  odadd2  19790  ablsimpgfindlem1  20050  omndmul2  20074  srgbinomlem3  20175  srgbinomlem4  20176  cncrng  21355  cncrngOLD  21356  gzrngunit  21400  zringunit  21433  prmirredlem  21439  pzriprnglem12  21459  freshmansdream  21541  mhppwdeg  22105  psdmul  22121  cayhamlem1  22822  expcn  24831  expcnOLD  24833  iirevcn  24892  iihalf2cn  24897  iihalf2cnOLD  24898  icchmeo  24906  icchmeoOLD  24907  icopnfcnv  24908  icopnfhmeo  24909  evth  24926  pcoass  24992  pjthlem1  25405  ovolunlem1a  25465  ovolunlem1  25466  opnmbllem  25570  mbfi1fseqlem6  25689  bddibl  25809  dvnadd  25899  dvmptid  25929  dvmptdiv  25946  dvcnvlem  25948  dveflem  25951  dvef  25952  dvsincos  25953  dvlipcn  25967  dvivthlem1  25981  lhop2  25988  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgpowd  26025  ply1divex  26110  fta1glem1  26141  dgrcolem1  26247  dgrcolem2  26248  vieta1lem1  26286  aaliou3lem2  26319  aaliou3lem8  26321  dvtaylp  26346  dvntaylp  26347  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  abelthlem1  26409  abelthlem2  26410  abelthlem6  26414  abelthlem7  26416  logdivlti  26597  advlog  26631  advlogexp  26632  logtayl  26637  cxpmul2  26666  dvcxp1  26717  dvcxp2  26718  dvcncxp1  26720  dvcnsqrt  26721  loglesqrt  26739  relogbdiv  26757  ang180lem4  26790  ang180lem5  26791  isosctrlem2  26797  isosctrlem3  26798  affineequiv  26801  affineequiv2  26802  affineequiv3  26803  angpieqvdlem  26806  chordthmlem2  26811  chordthmlem3  26812  chordthmlem5  26814  dcubic2  26822  dcubic  26824  quart1lem  26833  quart1  26834  quart  26839  asinlem  26846  asinlem3  26849  atansopn  26910  dvatan  26913  leibpi  26920  birthdaylem2  26930  efrlim  26947  efrlimOLD  26948  cxplim  26950  divsqrtsumlem  26958  logdifbnd  26972  emcllem2  26975  emcllem3  26976  emcllem5  26978  zetacvg  26993  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  lgam1  27042  gamfac  27045  wilthlem2  27047  wilthimp  27050  ftalem5  27055  basellem3  27061  basellem5  27063  basellem8  27066  basellem9  27067  sqff1o  27160  muinv  27171  logfaclbnd  27201  logfacrlim  27203  logexprlim  27204  perfectlem2  27209  dchr1cl  27230  dchrinvcl  27232  dchrfi  27234  dchr1  27236  dchrsum2  27247  bcmono  27256  bcp1ctr  27258  bclbnd  27259  bposlem9  27271  gausslemma2dlem1a  27344  gausslemma2dlem5  27350  lgseisenlem4  27357  lgsquadlem1  27359  m1lgs  27367  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgslem3d1  27382  2lgsoddprmlem1  27387  2sqlem8  27405  2sq2  27412  addsqn2reu  27420  addsqrexnreu  27421  addsqnreup  27422  addsq2nreurex  27423  chtppilim  27454  rpvmasumlem  27466  dchrisumlem1  27468  dchrisum0re  27492  dchrisum0lem2a  27496  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  2vmadivsumlem  27519  selberg4lem1  27539  pntrsumo1  27544  selberg34r  27550  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntibndlem2  27570  pntlemg  27577  pntlemr  27581  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntlem3  27588  ostth2lem2  27613  ttgcontlem1  28969  cusgrsize2inds  29539  wlklenvclwlk  29739  pthdadjvtx  29813  crctcshwlkn0lem1  29895  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wlklnwwlkln2lem  29967  wlknwwlksnbij  29973  wwlksnred  29977  wwlksnext  29978  wwlksnextbi  29979  wwlksnredwwlkn  29980  wwlksnextwrd  29982  wwlksnextinj  29984  wwlksnextproplem2  29995  wwlksnextproplem3  29996  clwwlkccatlem  30076  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlklem3  30088  clwlkclwwlk  30089  clwwisshclwwslemlem  30100  clwwisshclwws  30102  clwwlkel  30133  clwwlkf  30134  clwwlkwwlksb  30141  clwwlkext2edg  30143  wwlksext2clwwlk  30144  clwwlknonex2lem1  30194  clwwlknonex2lem2  30195  eucrct2eupth  30332  numclwwlk1lem2foalem  30438  numclwwlk1lem2fo  30445  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  numclwwlk6  30477  smcnlem  30785  receqid  32835  fzm1ne1  32879  bcm1n  32886  ltesubnnd  32914  sgn0bi  32932  oexpled  32939  wrdt2ind  33046  gsummptp1  33151  gsummulsubdishift1  33162  psgnfzto1stlem  33194  cycpmco2lem3  33222  cycpmco2lem4  33223  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2lem7  33226  cycpmco2  33227  archirngz  33283  archiabllem1a  33285  archiabllem2c  33289  gsumind  33438  esplyind  33752  esplyindfv  33753  esplyfvn  33754  vietadeg1  33755  vietalem  33756  ccfldextdgrr  33850  constrfin  33924  nn0constr  33939  iconstr  33944  constrrecl  33947  constrimcl  33948  constrreinvcl  33950  constrinvcl  33951  constrresqrtcl  33955  2sqr3minply  33958  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  cos9thpiminply  33966  cos9thpinconstrlem1  33967  1smat1  33982  madjusmdetlem2  34006  madjusmdetlem4  34008  dya2icoseg  34455  iwrdsplit  34565  fibp1  34579  ballotlemfp1  34670  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemic  34685  ballotlem1c  34686  ballotlemsgt1  34689  ballotlemsdom  34690  ballotlemsel1i  34691  ballotlemsi  34693  ballotlemsima  34694  ballotlem1ri  34713  signstfvn  34747  signsvtn0  34748  signstfveq0  34755  signsvfn  34760  signsvtn  34762  signshf  34766  hashreprin  34798  circlemeth  34818  logdivsqrle  34828  revpfxsfxrev  35332  revwlk  35341  swrdwlk  35343  subfacp1lem1  35395  subfacp1lem5  35400  cvxpconn  35458  sinccvglem  35888  divcnvlin  35949  bcm1nt  35953  bcprod  35954  bccolsum  35955  iprodgam  35958  faclimlem1  35959  faclimlem2  35960  faclimlem3  35961  faclim  35962  iprodfac  35963  faclim2  35964  fwddifnp1  36381  dnizphlfeqhlf  36698  dnibndlem3  36702  dnibndlem13  36712  unblimceq0  36729  knoppndvlem6  36739  knoppndvlem9  36742  knoppndvlem14  36747  knoppndvlem15  36748  knoppndvlem16  36749  knoppndvlem17  36750  bj-bary1lem1  37566  irrdiff  37581  poimirlem25  37896  poimirlem26  37897  poimirlem32  37903  opnmbllem0  37907  itg2addnclem2  37923  dvasin  37955  dvacos  37956  areacirclem1  37959  areacirclem4  37962  areacirc  37964  bfp  38075  fzsplitnd  42352  lcmfunnnd  42382  lcmineqlem1  42399  lcmineqlem3  42401  lcmineqlem4  42402  lcmineqlem7  42405  lcmineqlem8  42406  lcmineqlem10  42408  lcmineqlem11  42409  lcmineqlem12  42410  lcmineqlem18  42416  lcmineqlem19  42417  lcmineqlem22  42420  lcmineqlem23  42421  dvrelogpow2b  42438  aks4d1p1p4  42441  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  aks4d1p3  42448  aks4d1p7d1  42452  primrootsunit1  42467  posbezout  42470  primrootscoprbij  42472  primrootspoweq0  42476  aks6d1c1  42486  hashscontpow1  42491  2np3bcnp1  42514  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  sticksstones16  42532  sticksstones22  42538  aks6d1c6lem3  42542  aks6d1c7lem1  42550  unitscyglem5  42569  nnadd1com  42637  nnaddcom  42638  nnadddir  42640  nnmul1com  42641  nnmulcom  42642  3rdpwhole  42662  fz1sump1  42680  oddnumth  42681  nicomachus  42682  sumcubes  42683  tan3rdpi  42722  redvmptabs  42730  readvrec  42732  reixi  42793  sn-mullid  42806  sn-0tie0  42821  renegmulnnass  42835  fiabv  42906  fltnltalem  43020  fltnlta  43021  3cubeslem1  43041  3cubeslem2  43042  3cubeslem4  43046  pell1qrge1  43227  rmspecfund  43266  acongeq  43340  jm2.18  43345  jm2.19lem3  43348  jm2.25  43356  jm2.16nn0  43361  jm3.1lem1  43374  jm3.1lem2  43375  areaquad  43573  relexpmulnn  44065  relexpaddss  44074  cvgdvgrat  44669  radcnvrat  44670  hashnzfzclim  44678  ofdivrec  44682  expgrowthi  44689  bccm1k  44698  dvradcnv2  44703  binomcxplemwb  44704  binomcxplemnn0  44705  binomcxplemrat  44706  binomcxplemfrat  44707  binomcxplemdvbinom  44709  binomcxplemnotnn0  44712  refsum2cnlem1  45397  fzisoeu  45662  fperiodmullem  45665  fzdifsuc2  45672  xralrple2  45713  nnsplit  45717  infleinflem2  45729  fmul01lt1lem2  45945  fprodcn  45960  clim1fr1  45961  isumneg  45962  climneg  45970  sumnnodd  45990  reclimc  46011  coseq0  46222  coskpi2  46224  cosknegpi  46227  fprodcncf  46258  fprodsubrecnncnvlem  46265  fprodaddrecnncnvlem  46267  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnxpaek  46300  dvnmul  46301  dvmptfprod  46303  dvnprodlem3  46306  itgsinexp  46313  itgiccshift  46338  itgperiod  46339  itgsbtaddcnst  46340  stoweidlem1  46359  stoweidlem7  46365  stoweidlem10  46368  stoweidlem11  46369  stoweidlem14  46372  stoweidlem17  46375  stoweidlem34  46392  stoweidlem42  46400  wallispilem3  46425  wallispilem5  46427  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  wallispi2  46431  stirlinglem1  46432  stirlinglem3  46434  stirlinglem4  46435  stirlinglem5  46436  stirlinglem6  46437  stirlinglem7  46438  stirlinglem8  46439  stirlinglem10  46441  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  stirlinglem15  46446  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkertrigeq  46459  dirkercncflem1  46461  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem11  46476  fourierdlem15  46480  fourierdlem26  46491  fourierdlem36  46501  fourierdlem40  46505  fourierdlem41  46506  fourierdlem42  46507  fourierdlem48  46512  fourierdlem49  46513  fourierdlem56  46520  fourierdlem58  46522  fourierdlem59  46523  fourierdlem62  46526  fourierdlem64  46528  fourierdlem65  46529  fourierdlem78  46542  fourierdlem79  46543  sqwvfoura  46586  fourierswlem  46588  fouriersw  46589  etransclem23  46615  etransclem24  46616  etransclem28  46620  etransclem35  46627  etransclem38  46630  nnfoctbdjlem  46813  smfmullem1  47149  sigaradd  47224  chnerlem2  47241  cjnpoly  47249  deccarry  47671  ceilbi  47693  m1modne  47708  m1modmmod  47718  modm1nep2  47728  modm1nem2  47729  fargshiftf1  47801  fargshiftfo  47802  fmtnof1  47895  sqrtpwpw2p  47898  fmtnorec2lem  47902  fmtnorec4  47909  fmtnoprmfac1lem  47924  fmtnoprmfac1  47925  fmtnoprmfac2  47927  2pwp1prm  47949  mod42tp1mod8  47962  sfprmdvdsmersenne  47963  lighneallem3  47967  lighneallem4  47970  onego  48006  zofldiv2ALTV  48022  oexpnegALTV  48037  opoeALTV  48043  opeoALTV  48044  epee  48065  perfectALTVlem1  48081  fppr2odd  48091  fpprwppr  48099  gpg3nbgrvtx0  48436  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  0nodd  48530  2nodd  48532  nnsgrpnmnd  48538  1neven  48598  altgsumbc  48712  pw2m1lepw2m1  48880  zofldiv2  48891  nnpw2pmod  48943  blen1b  48948  blennn0em1  48951  dignn0flhalflem1  48975  dignn0flhalflem2  48976  nn0sumshdiglemB  48980  nn0sumshdiglem1  48981  nn0sumshdiglem2  48982  itcovalpclem2  49031  ackval1  49041  ackval2  49042  ackval3  49043  affineid  49064  1subrec1sub  49065  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2vlinest  49101