Theorem 1cnd 11125

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  1c1 11025

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

This theorem is referenced by:  adddirp1d  11156  1p1times  11302  addcom  11317  addcomd  11333  muladd11r  11344  pncan1  11559  npcan1  11560  muls1d  11595  mulsubfacd  11596  recrec  11836  rec11  11837  rec11r  11838  rereccl  11857  subrecd  11968  nn1m1nn  12164  add1p1  12390  sub1m1  12391  cnm2m1cnm3  12392  xp1d2m1eqxm1d2  12393  div4p1lem1div2  12394  nn0n0n1ge2  12467  zneo  12573  rpnnen1lem5  12892  lincmb01cmp  13409  iccf1o  13410  xov1plusxeqvd  13412  zpnn0elfzo1  13653  ubmelm1fzo  13677  fzosplitpr  13691  fzosplitprm1  13692  fzom1ne1  13699  fzoshftral  13701  fladdz  13743  2tnp1ge0ge0  13747  ltdifltdiv  13752  dfceil2  13757  negmod  13837  modnegd  13847  addmodlteq  13867  binom2sub1  14142  binom3  14145  zesq  14147  sqoddm1div8  14164  bcm1k  14236  bcp1n  14237  bcp1m1  14241  bcpasc  14242  bcn2m1  14245  hashfz  14348  hashfzo  14350  hashfzp1  14352  hashf1lem2  14377  hashf1  14378  hashdifsnp1  14427  lswccatn0lsw  14513  ccatws1lenp1b  14543  revccat  14687  repswrevw  14708  cshwidxm1  14728  cshwidxn  14730  cshweqrep  14742  cshimadifsn0  14751  swrds2m  14862  swrd2lsw  14873  relexpaddnn  14972  absexpz  15226  reccn2  15518  rlimno1  15575  isercolllem1  15586  isercoll2  15590  iseraltlem2  15604  iseraltlem3  15605  fsump1  15677  hashiun  15743  hash2iun1dif1  15745  binomlem  15750  bcxmas  15756  incexc  15758  incexc2  15759  climcndslem1  15770  arisum  15781  arisum2  15782  trireciplem  15783  pwdif  15789  pwm1geoser  15790  geolim2  15792  georeclim  15793  mertenslem1  15805  prodfrec  15816  ntrivcvg  15818  ntrivcvgtail  15821  prodrblem  15850  prodmolem2a  15855  fprodntriv  15863  prod1  15865  fprodser  15870  fprodcl  15873  fprodm1  15888  fprodp1  15890  fprodclf  15913  risefacval2  15931  fallfacval2  15932  risefacp1  15950  fallfacp1  15951  risefacfac  15956  fallfacfwd  15957  binomfallfaclem2  15961  fallfacval4  15964  bpolydiflem  15975  ef0lem  15999  tanaddlem  16089  tanadd  16090  cos01bnd  16109  oddm1even  16268  oddp1even  16269  oexpneg  16270  ltoddhalfle  16286  halfleoddlt  16287  nn0ob  16309  pwp1fsum  16316  flodddiv4  16340  bitsp1o  16358  bitsf1  16371  sadcp1  16380  qredeu  16583  prmdiv  16710  prmdiveq  16711  vfermltlALT  16728  pc2dvds  16805  4sqlem11  16881  4sqlem12  16882  vdwapun  16900  vdwlem3  16909  vdwlem6  16912  vdwlem9  16915  ramub1lem2  16953  prmop1  16964  prmdvdsprmo  16968  prmgaplem8  16984  cshwshashnsame  17029  chnub  18543  chnlt  18544  chnccat  18547  chnrev  18548  gsumsgrpccat  18763  psgnunilem5  19421  psgnunilem2  19422  sylow1lem1  19525  efgredlemc  19672  odadd2  19776  ablsimpgfindlem1  20036  omndmul2  20060  srgbinomlem3  20161  srgbinomlem4  20162  cncrng  21341  cncrngOLD  21342  gzrngunit  21386  zringunit  21419  prmirredlem  21425  pzriprnglem12  21445  freshmansdream  21527  mhppwdeg  22091  psdmul  22107  cayhamlem1  22808  expcn  24817  expcnOLD  24819  iirevcn  24878  iihalf2cn  24883  iihalf2cnOLD  24884  icchmeo  24892  icchmeoOLD  24893  icopnfcnv  24894  icopnfhmeo  24895  evth  24912  pcoass  24978  pjthlem1  25391  ovolunlem1a  25451  ovolunlem1  25452  opnmbllem  25556  mbfi1fseqlem6  25675  bddibl  25795  dvnadd  25885  dvmptid  25915  dvmptdiv  25932  dvcnvlem  25934  dveflem  25937  dvef  25938  dvsincos  25939  dvlipcn  25953  dvivthlem1  25967  lhop2  25974  dvcvx  25979  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dvfsumlem1  25986  dvfsumlem2  25987  dvfsumlem2OLD  25988  itgpowd  26011  ply1divex  26096  fta1glem1  26127  dgrcolem1  26233  dgrcolem2  26234  vieta1lem1  26272  aaliou3lem2  26305  aaliou3lem8  26307  dvtaylp  26332  dvntaylp  26333  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  abelthlem1  26395  abelthlem2  26396  abelthlem6  26400  abelthlem7  26402  logdivlti  26583  advlog  26617  advlogexp  26618  logtayl  26623  cxpmul2  26652  dvcxp1  26703  dvcxp2  26704  dvcncxp1  26706  dvcnsqrt  26707  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  efrlimOLD  26934  cxplim  26936  divsqrtsumlem  26944  logdifbnd  26958  emcllem2  26961  emcllem3  26962  emcllem5  26964  zetacvg  26979  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem4  26996  lgamgulmlem5  26997  lgamgulmlem6  26998  lgamgulm2  27000  lgamcvg2  27019  gamcvg  27020  gamcvg2lem  27023  lgam1  27028  gamfac  27031  wilthlem2  27033  wilthimp  27036  ftalem5  27041  basellem3  27047  basellem5  27049  basellem8  27052  basellem9  27053  sqff1o  27146  muinv  27157  logfaclbnd  27187  logfacrlim  27189  logexprlim  27190  perfectlem2  27195  dchr1cl  27216  dchrinvcl  27218  dchrfi  27220  dchr1  27222  dchrsum2  27233  bcmono  27242  bcp1ctr  27244  bclbnd  27245  bposlem9  27257  gausslemma2dlem1a  27330  gausslemma2dlem5  27336  lgseisenlem4  27343  lgsquadlem1  27345  m1lgs  27353  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2lgslem3d1  27368  2lgsoddprmlem1  27373  2sqlem8  27391  2sq2  27398  addsqn2reu  27406  addsqrexnreu  27407  addsqnreup  27408  addsq2nreurex  27409  chtppilim  27440  rpvmasumlem  27452  dchrisumlem1  27454  dchrisum0re  27478  dchrisum0lem2a  27482  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  2vmadivsumlem  27505  selberg4lem1  27525  pntrsumo1  27530  selberg34r  27536  pntrlog2bndlem2  27543  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntibndlem2  27556  pntlemg  27563  pntlemr  27567  pntlemf  27570  pntlemk  27571  pntlemo  27572  pntlem3  27574  ostth2lem2  27599  ttgcontlem1  28906  cusgrsize2inds  29476  wlklenvclwlk  29676  pthdadjvtx  29750  crctcshwlkn0lem1  29832  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  wlklnwwlkln2lem  29904  wlknwwlksnbij  29910  wwlksnred  29914  wwlksnext  29915  wwlksnextbi  29916  wwlksnredwwlkn  29917  wwlksnextwrd  29919  wwlksnextinj  29921  wwlksnextproplem2  29932  wwlksnextproplem3  29933  clwwlkccatlem  30013  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwlkclwwlklem3  30025  clwlkclwwlk  30026  clwwisshclwwslemlem  30037  clwwisshclwws  30039  clwwlkel  30070  clwwlkf  30071  clwwlkwwlksb  30078  clwwlkext2edg  30080  wwlksext2clwwlk  30081  clwwlknonex2lem1  30131  clwwlknonex2lem2  30132  eucrct2eupth  30269  numclwwlk1lem2foalem  30375  numclwwlk1lem2fo  30382  numclwlk2lem2f  30401  numclwlk2lem2f1o  30403  numclwwlk6  30414  smcnlem  30721  receqid  32773  fzm1ne1  32817  bcm1n  32824  ltesubnnd  32852  sgn0bi  32870  oexpled  32877  wrdt2ind  32984  gsummptp1  33089  gsummulsubdishift1  33100  psgnfzto1stlem  33131  cycpmco2lem3  33159  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  archirngz  33220  archiabllem1a  33222  archiabllem2c  33226  gsumind  33375  esplyind  33680  esplyindfv  33681  esplyfvn  33682  vietadeg1  33683  vietalem  33684  ccfldextdgrr  33778  constrfin  33852  nn0constr  33867  iconstr  33872  constrrecl  33875  constrimcl  33876  constrreinvcl  33878  constrinvcl  33879  constrresqrtcl  33883  2sqr3minply  33886  cos9thpiminplylem1  33888  cos9thpiminplylem2  33889  cos9thpiminplylem3  33890  cos9thpiminply  33894  cos9thpinconstrlem1  33895  1smat1  33910  madjusmdetlem2  33934  madjusmdetlem4  33936  dya2icoseg  34383  iwrdsplit  34493  fibp1  34507  ballotlemfp1  34598  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemic  34613  ballotlem1c  34614  ballotlemsgt1  34617  ballotlemsdom  34618  ballotlemsel1i  34619  ballotlemsi  34621  ballotlemsima  34622  ballotlem1ri  34641  signstfvn  34675  signsvtn0  34676  signstfveq0  34683  signsvfn  34688  signsvtn  34690  signshf  34694  hashreprin  34726  circlemeth  34746  logdivsqrle  34756  revpfxsfxrev  35259  revwlk  35268  swrdwlk  35270  subfacp1lem1  35322  subfacp1lem5  35327  cvxpconn  35385  sinccvglem  35815  divcnvlin  35876  bcm1nt  35880  bcprod  35881  bccolsum  35882  iprodgam  35885  faclimlem1  35886  faclimlem2  35887  faclimlem3  35888  faclim  35889  iprodfac  35890  faclim2  35891  fwddifnp1  36308  dnizphlfeqhlf  36619  dnibndlem3  36623  dnibndlem13  36633  unblimceq0  36650  knoppndvlem6  36660  knoppndvlem9  36663  knoppndvlem14  36668  knoppndvlem15  36669  knoppndvlem16  36670  knoppndvlem17  36671  bj-bary1lem1  37455  irrdiff  37470  poimirlem25  37785  poimirlem26  37786  poimirlem32  37792  opnmbllem0  37796  itg2addnclem2  37812  dvasin  37844  dvacos  37845  areacirclem1  37848  areacirclem4  37851  areacirc  37853  bfp  37964  fzsplitnd  42175  lcmfunnnd  42205  lcmineqlem1  42222  lcmineqlem3  42224  lcmineqlem4  42225  lcmineqlem7  42228  lcmineqlem8  42229  lcmineqlem10  42231  lcmineqlem11  42232  lcmineqlem12  42233  lcmineqlem18  42239  lcmineqlem19  42240  lcmineqlem22  42243  lcmineqlem23  42244  dvrelogpow2b  42261  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p3  42271  aks4d1p7d1  42275  primrootsunit1  42290  posbezout  42293  primrootscoprbij  42295  primrootspoweq0  42299  aks6d1c1  42309  hashscontpow1  42314  2np3bcnp1  42337  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  sticksstones16  42355  sticksstones22  42361  aks6d1c6lem3  42365  aks6d1c7lem1  42373  unitscyglem5  42392  nnadd1com  42464  nnaddcom  42465  nnadddir  42467  nnmul1com  42468  nnmulcom  42469  3rdpwhole  42489  fz1sump1  42507  oddnumth  42508  nicomachus  42509  sumcubes  42510  tan3rdpi  42549  redvmptabs  42557  readvrec  42559  reixi  42620  sn-mullid  42633  sn-0tie0  42648  renegmulnnass  42662  fiabv  42733  fltnltalem  42847  fltnlta  42848  3cubeslem1  42868  3cubeslem2  42869  3cubeslem4  42873  pell1qrge1  43054  rmspecfund  43093  acongeq  43167  jm2.18  43172  jm2.19lem3  43175  jm2.25  43183  jm2.16nn0  43188  jm3.1lem1  43201  jm3.1lem2  43202  areaquad  43400  relexpmulnn  43892  relexpaddss  43901  cvgdvgrat  44496  radcnvrat  44497  hashnzfzclim  44505  ofdivrec  44509  expgrowthi  44516  bccm1k  44525  dvradcnv2  44530  binomcxplemwb  44531  binomcxplemnn0  44532  binomcxplemrat  44533  binomcxplemfrat  44534  binomcxplemdvbinom  44536  binomcxplemnotnn0  44539  refsum2cnlem1  45224  fzisoeu  45490  fperiodmullem  45493  fzdifsuc2  45500  xralrple2  45541  nnsplit  45545  infleinflem2  45557  fmul01lt1lem2  45773  fprodcn  45788  clim1fr1  45789  isumneg  45790  climneg  45798  sumnnodd  45818  reclimc  45839  coseq0  46050  coskpi2  46052  cosknegpi  46055  fprodcncf  46086  fprodsubrecnncnvlem  46093  fprodaddrecnncnvlem  46095  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnxpaek  46128  dvnmul  46129  dvmptfprod  46131  dvnprodlem3  46134  itgsinexp  46141  itgiccshift  46166  itgperiod  46167  itgsbtaddcnst  46168  stoweidlem1  46187  stoweidlem7  46193  stoweidlem10  46196  stoweidlem11  46197  stoweidlem14  46200  stoweidlem17  46203  stoweidlem34  46220  stoweidlem42  46228  wallispilem3  46253  wallispilem5  46255  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  wallispi2  46259  stirlinglem1  46260  stirlinglem3  46262  stirlinglem4  46263  stirlinglem5  46264  stirlinglem6  46265  stirlinglem7  46266  stirlinglem8  46267  stirlinglem10  46269  stirlinglem11  46270  stirlinglem12  46271  stirlinglem13  46272  stirlinglem15  46274  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  dirkertrigeq  46287  dirkercncflem1  46289  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem11  46304  fourierdlem15  46308  fourierdlem26  46319  fourierdlem36  46329  fourierdlem40  46333  fourierdlem41  46334  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem56  46348  fourierdlem58  46350  fourierdlem59  46351  fourierdlem62  46354  fourierdlem64  46356  fourierdlem65  46357  fourierdlem78  46370  fourierdlem79  46371  sqwvfoura  46414  fourierswlem  46416  fouriersw  46417  etransclem23  46443  etransclem24  46444  etransclem28  46448  etransclem35  46455  etransclem38  46458  nnfoctbdjlem  46641  smfmullem1  46977  sigaradd  47052  chnerlem2  47069  cjnpoly  47077  deccarry  47499  ceilbi  47521  m1modne  47536  m1modmmod  47546  modm1nep2  47556  modm1nem2  47557  fargshiftf1  47629  fargshiftfo  47630  fmtnof1  47723  sqrtpwpw2p  47726  fmtnorec2lem  47730  fmtnorec4  47737  fmtnoprmfac1lem  47752  fmtnoprmfac1  47753  fmtnoprmfac2  47755  2pwp1prm  47777  mod42tp1mod8  47790  sfprmdvdsmersenne  47791  lighneallem3  47795  lighneallem4  47798  onego  47834  zofldiv2ALTV  47850  oexpnegALTV  47865  opoeALTV  47871  opeoALTV  47872  epee  47893  perfectALTVlem1  47909  fppr2odd  47919  fpprwppr  47927  gpg3nbgrvtx0  48264  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  0nodd  48358  2nodd  48360  nnsgrpnmnd  48366  1neven  48426  altgsumbc  48540  pw2m1lepw2m1  48708  zofldiv2  48719  nnpw2pmod  48771  blen1b  48776  blennn0em1  48779  dignn0flhalflem1  48803  dignn0flhalflem2  48804  nn0sumshdiglemB  48808  nn0sumshdiglem1  48809  nn0sumshdiglem2  48810  itcovalpclem2  48859  ackval1  48869  ackval2  48870  ackval3  48871  affineid  48892  1subrec1sub  48893  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  rrx2vlinest  48929