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  11171  1p1times  11317  addcom  11332  addcomd  11348  muladd11r  11359  pncan1  11574  npcan1  11575  muls1d  11610  mulsubfacd  11611  recrec  11852  rec11  11853  rec11r  11854  rereccl  11873  subrecd  11984  nn1m1nn  12195  nnadd1com  12200  nnaddcom  12201  nnadddir  12233  nnmul1com  12234  nnmulcom  12235  add1p1  12428  sub1m1  12429  cnm2m1cnm3  12430  xp1d2m1eqxm1d2  12431  div4p1lem1div2  12432  nn0n0n1ge2  12505  zneo  12612  rpnnen1lem5  12931  lincmb01cmp  13448  iccf1o  13449  xov1plusxeqvd  13451  zpnn0elfzo1  13694  ubmelm1fzo  13718  fzosplitpr  13732  fzosplitprm1  13733  fzom1ne1  13740  fzoshftral  13742  fladdz  13784  2tnp1ge0ge0  13788  ltdifltdiv  13793  dfceil2  13798  negmod  13878  modnegd  13888  addmodlteq  13908  binom2sub1  14183  binom3  14186  zesq  14188  sqoddm1div8  14205  bcm1k  14277  bcp1n  14278  bcp1m1  14282  bcpasc  14283  bcn2m1  14286  hashfz  14389  hashfzo  14391  hashfzp1  14393  hashf1lem2  14418  hashf1  14419  hashdifsnp1  14468  lswccatn0lsw  14554  ccatws1lenp1b  14584  revccat  14728  repswrevw  14749  cshwidxm1  14769  cshwidxn  14771  cshweqrep  14783  cshimadifsn0  14792  swrds2m  14903  swrd2lsw  14914  relexpaddnn  15013  absexpz  15267  reccn2  15559  rlimno1  15616  isercolllem1  15627  isercoll2  15631  iseraltlem2  15645  iseraltlem3  15646  fsump1  15718  fsumconst1  15753  hashiun  15785  hash2iun1dif1  15787  indsumhash  15792  binomlem  15794  bcxmas  15800  incexc  15802  incexc2  15803  climcndslem1  15814  arisum  15825  arisum2  15826  trireciplem  15827  pwdif  15833  pwm1geoser  15834  geolim2  15836  georeclim  15837  mertenslem1  15849  prodfrec  15860  ntrivcvg  15862  ntrivcvgtail  15865  prodrblem  15894  prodmolem2a  15899  fprodntriv  15907  prod1  15909  fprodser  15914  fprodcl  15917  fprodm1  15932  fprodp1  15934  fprodclf  15957  risefacval2  15975  fallfacval2  15976  risefacp1  15994  fallfacp1  15995  risefacfac  16000  fallfacfwd  16001  binomfallfaclem2  16005  fallfacval4  16008  bpolydiflem  16019  ef0lem  16043  tanaddlem  16133  tanadd  16134  cos01bnd  16153  oddm1even  16312  oddp1even  16313  oexpneg  16314  ltoddhalfle  16330  halfleoddlt  16331  nn0ob  16353  pwp1fsum  16360  flodddiv4  16384  bitsp1o  16402  bitsf1  16415  sadcp1  16424  qredeu  16627  prmdiv  16755  prmdiveq  16756  vfermltlALT  16773  pc2dvds  16850  4sqlem11  16926  4sqlem12  16927  vdwapun  16945  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  ramub1lem2  16998  prmop1  17009  prmdvdsprmo  17013  prmgaplem8  17029  cshwshashnsame  17074  chnub  18588  chnlt  18589  chnccat  18592  chnrev  18593  gsumsgrpccat  18808  psgnunilem5  19469  psgnunilem2  19470  sylow1lem1  19573  efgredlemc  19720  odadd2  19824  ablsimpgfindlem1  20084  omndmul2  20108  srgbinomlem3  20209  srgbinomlem4  20210  cncrng  21373  gzrngunit  21413  zringunit  21446  prmirredlem  21452  pzriprnglem12  21472  freshmansdream  21554  mhppwdeg  22116  psdmul  22132  cayhamlem1  22831  expcn  24839  iirevcn  24897  iihalf2cn  24901  icchmeo  24908  icopnfcnv  24909  icopnfhmeo  24910  evth  24926  pcoass  24991  pjthlem1  25404  ovolunlem1a  25463  ovolunlem1  25464  opnmbllem  25568  mbfi1fseqlem6  25687  bddibl  25807  dvnadd  25896  dvmptid  25924  dvmptdiv  25941  dvcnvlem  25943  dveflem  25946  dvef  25947  dvsincos  25948  dvlipcn  25961  dvivthlem1  25975  lhop2  25982  dvcvx  25987  dvfsumle  25988  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem2  25994  itgpowd  26017  ply1divex  26102  fta1glem1  26133  dgrcolem1  26238  dgrcolem2  26239  vieta1lem1  26276  aaliou3lem2  26309  aaliou3lem8  26311  dvtaylp  26335  dvntaylp  26336  taylthlem1  26338  taylthlem2  26339  abelthlem1  26396  abelthlem2  26397  abelthlem6  26401  abelthlem7  26403  logdivlti  26584  advlog  26618  advlogexp  26619  logtayl  26624  cxpmul2  26653  dvcxp1  26704  dvcxp2  26705  dvcncxp1  26707  dvcnsqrt  26708  loglesqrt  26725  relogbdiv  26743  ang180lem4  26776  ang180lem5  26777  isosctrlem2  26783  isosctrlem3  26784  affineequiv  26787  affineequiv2  26788  affineequiv3  26789  angpieqvdlem  26792  chordthmlem2  26797  chordthmlem3  26798  chordthmlem5  26800  dcubic2  26808  dcubic  26810  quart1lem  26819  quart1  26820  quart  26825  asinlem  26832  asinlem3  26835  atansopn  26896  dvatan  26899  leibpi  26906  birthdaylem2  26916  efrlim  26933  cxplim  26935  divsqrtsumlem  26943  logdifbnd  26957  emcllem2  26960  emcllem3  26961  emcllem5  26963  zetacvg  26978  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  lgam1  27027  gamfac  27030  wilthlem2  27032  wilthimp  27035  ftalem5  27040  basellem3  27046  basellem5  27048  basellem8  27051  basellem9  27052  sqff1o  27145  muinv  27156  logfaclbnd  27185  logfacrlim  27187  logexprlim  27188  perfectlem2  27193  dchr1cl  27214  dchrinvcl  27216  dchrfi  27218  dchr1  27220  dchrsum2  27231  bcmono  27240  bcp1ctr  27242  bclbnd  27243  bposlem9  27255  gausslemma2dlem1a  27328  gausslemma2dlem5  27334  lgseisenlem4  27341  lgsquadlem1  27343  m1lgs  27351  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgslem3d1  27366  2lgsoddprmlem1  27371  2sqlem8  27389  2sq2  27396  addsqn2reu  27404  addsqrexnreu  27405  addsqnreup  27406  addsq2nreurex  27407  chtppilim  27438  rpvmasumlem  27450  dchrisumlem1  27452  dchrisum0re  27476  dchrisum0lem2a  27480  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  2vmadivsumlem  27503  selberg4lem1  27523  pntrsumo1  27528  selberg34r  27534  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntibndlem2  27554  pntlemg  27561  pntlemr  27565  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntlem3  27572  ostth2lem2  27597  ttgcontlem1  28953  cusgrsize2inds  29522  wlklenvclwlk  29722  pthdadjvtx  29796  crctcshwlkn0lem1  29878  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wlklnwwlkln2lem  29950  wlknwwlksnbij  29956  wwlksnred  29960  wwlksnext  29961  wwlksnextbi  29962  wwlksnredwwlkn  29963  wwlksnextwrd  29965  wwlksnextinj  29967  wwlksnextproplem2  29978  wwlksnextproplem3  29979  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlklem3  30071  clwlkclwwlk  30072  clwwisshclwwslemlem  30083  clwwisshclwws  30085  clwwlkel  30116  clwwlkf  30117  clwwlkwwlksb  30124  clwwlkext2edg  30126  wwlksext2clwwlk  30127  clwwlknonex2lem1  30177  clwwlknonex2lem2  30178  eucrct2eupth  30315  numclwwlk1lem2foalem  30421  numclwwlk1lem2fo  30428  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  numclwwlk6  30460  smcnlem  30768  receqid  32817  fzm1ne1  32861  bcm1n  32868  ltesubnnd  32896  sgn0bi  32913  oexpled  32920  wrdt2ind  33013  gsummptp1  33118  gsummulsubdishift1  33129  psgnfzto1stlem  33161  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  archirngz  33250  archiabllem1a  33252  archiabllem2c  33256  gsumind  33405  esplyind  33719  esplyindfv  33720  esplyfvn  33721  vietadeg1  33722  vietalem  33723  ccfldextdgrr  33816  constrfin  33890  nn0constr  33905  iconstr  33910  constrrecl  33913  constrimcl  33914  constrreinvcl  33916  constrinvcl  33917  constrresqrtcl  33921  2sqr3minply  33924  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminply  33932  cos9thpinconstrlem1  33933  1smat1  33948  madjusmdetlem2  33972  madjusmdetlem4  33974  dya2icoseg  34421  iwrdsplit  34531  fibp1  34545  ballotlemfp1  34636  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemic  34651  ballotlem1c  34652  ballotlemsgt1  34655  ballotlemsdom  34656  ballotlemsel1i  34657  ballotlemsi  34659  ballotlemsima  34660  ballotlem1ri  34679  signstfvn  34713  signsvtn0  34714  signstfveq0  34721  signsvfn  34726  signsvtn  34728  signshf  34732  hashreprin  34764  circlemeth  34784  logdivsqrle  34794  revpfxsfxrev  35298  revwlk  35307  swrdwlk  35309  subfacp1lem1  35361  subfacp1lem5  35366  cvxpconn  35424  sinccvglem  35854  divcnvlin  35915  bcm1nt  35919  bcprod  35920  bccolsum  35921  iprodgam  35924  faclimlem1  35925  faclimlem2  35926  faclimlem3  35927  faclim  35928  iprodfac  35929  faclim2  35930  fwddifnp1  36347  dnizphlfeqhlf  36736  dnibndlem3  36740  dnibndlem13  36750  unblimceq0  36767  knoppndvlem6  36777  knoppndvlem9  36780  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem16  36787  knoppndvlem17  36788  bj-bary1lem1  37625  irrdiff  37640  qdiff  37641  poimirlem25  37966  poimirlem26  37967  poimirlem32  37973  opnmbllem0  37977  itg2addnclem2  37993  dvasin  38025  dvacos  38026  areacirclem1  38029  areacirclem4  38032  areacirc  38034  bfp  38145  fzsplitnd  42421  lcmfunnnd  42451  lcmineqlem1  42468  lcmineqlem3  42470  lcmineqlem4  42471  lcmineqlem7  42474  lcmineqlem8  42475  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem12  42479  lcmineqlem18  42485  lcmineqlem19  42486  lcmineqlem22  42489  lcmineqlem23  42490  dvrelogpow2b  42507  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p3  42517  aks4d1p7d1  42521  primrootsunit1  42536  posbezout  42539  primrootscoprbij  42541  primrootspoweq0  42545  aks6d1c1  42555  hashscontpow1  42560  2np3bcnp1  42583  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones16  42601  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c7lem1  42619  unitscyglem5  42638  3rdpwhole  42724  fz1sump1  42742  oddnumth  42743  nicomachus  42744  sumcubes  42745  tan3rdpi  42784  redvmptabs  42792  readvrec  42794  reixi  42855  sn-mullid  42868  sn-0tie0  42896  renegmulnnass  42910  fiabv  42981  fltnltalem  43095  fltnlta  43096  3cubeslem1  43116  3cubeslem2  43117  3cubeslem4  43121  pell1qrge1  43298  rmspecfund  43337  acongeq  43411  jm2.18  43416  jm2.19lem3  43419  jm2.25  43427  jm2.16nn0  43432  jm3.1lem1  43445  jm3.1lem2  43446  areaquad  43644  relexpmulnn  44136  relexpaddss  44145  cvgdvgrat  44740  radcnvrat  44741  hashnzfzclim  44749  ofdivrec  44753  expgrowthi  44760  bccm1k  44769  dvradcnv2  44774  binomcxplemwb  44775  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  refsum2cnlem1  45468  fzisoeu  45733  fperiodmullem  45736  fzdifsuc2  45743  xralrple2  45784  nnsplit  45788  infleinflem2  45800  fmul01lt1lem2  46015  fprodcn  46030  clim1fr1  46031  isumneg  46032  climneg  46040  sumnnodd  46060  reclimc  46081  coseq0  46292  coskpi2  46294  cosknegpi  46297  fprodcncf  46328  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnmul  46371  dvmptfprod  46373  dvnprodlem3  46376  itgsinexp  46383  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem1  46429  stoweidlem7  46435  stoweidlem10  46438  stoweidlem11  46439  stoweidlem14  46442  stoweidlem17  46445  stoweidlem34  46462  stoweidlem42  46470  wallispilem3  46495  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem15  46516  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem11  46546  fourierdlem15  46550  fourierdlem26  46561  fourierdlem36  46571  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem56  46590  fourierdlem58  46592  fourierdlem59  46593  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem78  46612  fourierdlem79  46613  sqwvfoura  46656  fourierswlem  46658  fouriersw  46659  etransclem23  46685  etransclem24  46686  etransclem28  46690  etransclem35  46697  etransclem38  46700  nnfoctbdjlem  46883  smfmullem1  47219  sigaradd  47294  chnerlem2  47313  sin3t  47319  cos3t  47320  sin5tlem1  47321  sin5tlem2  47322  sin5tlem4  47324  cos5t  47327  cjnpoly  47337  deccarry  47759  ceilbi  47785  flmrecm1  47791  m1modne  47802  m1modmmod  47812  modm1nep2  47822  modm1nem2  47823  fargshiftf1  47901  fargshiftfo  47902  fmtnof1  47998  sqrtpwpw2p  48001  fmtnorec2lem  48005  fmtnorec4  48012  fmtnoprmfac1lem  48027  fmtnoprmfac1  48028  fmtnoprmfac2  48030  2pwp1prm  48052  mod42tp1mod8  48065  sfprmdvdsmersenne  48066  lighneallem3  48070  lighneallem4  48073  ppivalnnprm  48088  ppivalnnnprmge6  48089  onego  48122  zofldiv2ALTV  48138  oexpnegALTV  48153  opoeALTV  48159  opeoALTV  48160  epee  48181  perfectALTVlem1  48197  fppr2odd  48207  fpprwppr  48215  gpg3nbgrvtx0  48552  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  0nodd  48646  2nodd  48648  nnsgrpnmnd  48654  1neven  48714  altgsumbc  48828  pw2m1lepw2m1  48996  zofldiv2  49007  nnpw2pmod  49059  blen1b  49064  blennn0em1  49067  dignn0flhalflem1  49091  dignn0flhalflem2  49092  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  nn0sumshdiglem2  49098  itcovalpclem2  49147  ackval1  49157  ackval2  49158  ackval3  49159  affineid  49180  1subrec1sub  49181  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2vlinest  49217