Theorem 1cnd 10901

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  1c1 10803

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

This theorem is referenced by:  adddirp1d  10932  1p1times  11076  addcom  11091  addcomd  11107  muladd11r  11118  pncan1  11329  npcan1  11330  muls1d  11365  mulsubfacd  11366  recrec  11602  rec11  11603  rec11r  11604  rereccl  11623  subrec  11734  nn1m1nn  11924  add1p1  12154  sub1m1  12155  cnm2m1cnm3  12156  xp1d2m1eqxm1d2  12157  div4p1lem1div2  12158  nn0n0n1ge2  12230  zneo  12333  rpnnen1lem5  12650  lincmb01cmp  13156  iccf1o  13157  xov1plusxeqvd  13159  zpnn0elfzo1  13389  ubmelm1fzo  13411  fzosplitpr  13424  fzosplitprm1  13425  fzoshftral  13432  fladdz  13473  2tnp1ge0ge0  13477  ltdifltdiv  13482  dfceil2  13487  negmod  13564  modnegd  13574  addmodlteq  13594  binom2sub1  13864  binom3  13867  zesq  13869  sqoddm1div8  13886  bcm1k  13957  bcp1n  13958  bcp1m1  13962  bcpasc  13963  bcn2m1  13966  hashfz  14070  hashfzo  14072  hashfzp1  14074  hashf1lem2  14098  hashf1  14099  hashdifsnp1  14138  lswccatn0lsw  14224  ccatws1lenp1b  14254  revccat  14407  repswrevw  14428  cshwidxm1  14448  cshwidxn  14450  cshweqrep  14462  cshimadifsn0  14471  swrds2m  14582  swrd2lsw  14593  relexpaddnn  14690  absexpz  14945  reccn2  15234  rlimno1  15293  isercolllem1  15304  isercoll2  15308  iseraltlem2  15322  iseraltlem3  15323  hashiun  15462  hash2iun1dif1  15464  binomlem  15469  bcxmas  15475  incexc  15477  incexc2  15478  climcndslem1  15489  arisum  15500  arisum2  15501  trireciplem  15502  pwdif  15508  pwm1geoser  15509  geolim2  15511  georeclim  15512  mertenslem1  15524  prodfrec  15535  ntrivcvg  15537  ntrivcvgtail  15540  prodrblem  15567  prodmolem2a  15572  fprodntriv  15580  prod1  15582  fprodser  15587  fprodcl  15590  fprodm1  15605  fprodp1  15607  fprodclf  15630  risefacval2  15648  fallfacval2  15649  risefacp1  15667  fallfacp1  15668  risefacfac  15673  fallfacfwd  15674  binomfallfaclem2  15678  fallfacval4  15681  bpolydiflem  15692  ef0lem  15716  tanaddlem  15803  tanadd  15804  cos01bnd  15823  oddm1even  15980  oddp1even  15981  oexpneg  15982  ltoddhalfle  15998  halfleoddlt  15999  nn0ob  16021  pwp1fsum  16028  flodddiv4  16050  bitsp1o  16068  bitsf1  16081  sadcp1  16090  qredeu  16291  prmdiv  16414  prmdiveq  16415  vfermltlALT  16431  pc2dvds  16508  4sqlem11  16584  4sqlem12  16585  vdwapun  16603  vdwlem3  16612  vdwlem6  16615  vdwlem9  16618  ramub1lem2  16656  prmop1  16667  prmdvdsprmo  16671  prmgaplem8  16687  cshwshashnsame  16733  gsumsgrpccat  18393  gsumccatOLD  18394  psgnunilem5  19017  psgnunilem2  19018  sylow1lem1  19118  efgredlemc  19266  odadd2  19365  ablsimpgfindlem1  19625  srgbinomlem3  19693  srgbinomlem4  19694  cncrng  20531  gzrngunit  20576  zringunit  20600  prmirredlem  20606  mhppwdeg  21250  cayhamlem1  21923  expcn  23941  iirevcn  23999  iihalf2cn  24003  icchmeo  24010  icopnfcnv  24011  icopnfhmeo  24012  evth  24028  pcoass  24093  pjthlem1  24506  ovolunlem1a  24565  ovolunlem1  24566  opnmbllem  24670  mbfi1fseqlem6  24790  bddibl  24909  dvnadd  24998  dvmptid  25026  dvmptdiv  25043  dvcnvlem  25045  dveflem  25048  dvef  25049  dvsincos  25050  dvlipcn  25063  dvivthlem1  25077  lhop2  25084  dvcvx  25089  dvfsumle  25090  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem2  25096  itgpowd  25119  ply1divex  25206  fta1glem1  25235  dgrcolem1  25339  dgrcolem2  25340  vieta1lem1  25375  aaliou3lem2  25408  aaliou3lem8  25410  dvtaylp  25434  dvntaylp  25435  taylthlem1  25437  taylthlem2  25438  abelthlem1  25495  abelthlem2  25496  abelthlem6  25500  abelthlem7  25502  logdivlti  25680  advlog  25714  advlogexp  25715  logtayl  25720  cxpmul2  25749  dvcxp1  25798  dvcxp2  25799  dvcncxp1  25801  dvcnsqrt  25802  loglesqrt  25816  relogbdiv  25834  ang180lem4  25867  ang180lem5  25868  isosctrlem2  25874  isosctrlem3  25875  affineequiv  25878  affineequiv2  25879  affineequiv3  25880  angpieqvdlem  25883  chordthmlem2  25888  chordthmlem3  25889  chordthmlem5  25891  dcubic2  25899  dcubic  25901  quart1lem  25910  quart1  25911  quart  25916  asinlem  25923  asinlem3  25926  atansopn  25987  dvatan  25990  leibpi  25997  birthdaylem2  26007  efrlim  26024  cxplim  26026  divsqrtsumlem  26034  logdifbnd  26048  emcllem2  26051  emcllem3  26052  emcllem5  26054  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  lgam1  26118  gamfac  26121  wilthlem2  26123  wilthimp  26126  ftalem5  26131  basellem3  26137  basellem5  26139  basellem8  26142  basellem9  26143  sqff1o  26236  muinv  26247  logfaclbnd  26275  logfacrlim  26277  logexprlim  26278  perfectlem2  26283  dchr1cl  26304  dchrinvcl  26306  dchrfi  26308  dchr1  26310  dchrsum2  26321  bcmono  26330  bcp1ctr  26332  bclbnd  26333  bposlem9  26345  gausslemma2dlem1a  26418  gausslemma2dlem5  26424  lgseisenlem4  26431  lgsquadlem1  26433  m1lgs  26441  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgslem3d1  26456  2lgsoddprmlem1  26461  2sqlem8  26479  2sq2  26486  addsqn2reu  26494  addsqrexnreu  26495  addsqnreup  26496  addsq2nreurex  26497  chtppilim  26528  rpvmasumlem  26540  dchrisumlem1  26542  dchrisum0re  26566  dchrisum0lem2a  26570  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  2vmadivsumlem  26593  selberg4lem1  26613  pntrsumo1  26618  selberg34r  26624  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntibndlem2  26644  pntlemg  26651  pntlemr  26655  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntlem3  26662  ostth2lem2  26687  ttgcontlem1  27155  cusgrsize2inds  27723  wlklenvclwlk  27924  wlklenvclwlkOLD  27925  pthdadjvtx  27999  crctcshwlkn0lem1  28076  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  wlklnwwlkln2lem  28148  wlknwwlksnbij  28154  wwlksnred  28158  wwlksnext  28159  wwlksnextbi  28160  wwlksnredwwlkn  28161  wwlksnextwrd  28163  wwlksnextinj  28165  wwlksnextproplem2  28176  wwlksnextproplem3  28177  clwwlkccatlem  28254  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlklem3  28266  clwlkclwwlk  28267  clwwisshclwwslemlem  28278  clwwisshclwws  28280  clwwlkel  28311  clwwlkf  28312  clwwlkwwlksb  28319  clwwlkext2edg  28321  wwlksext2clwwlk  28322  clwwlknonex2lem1  28372  clwwlknonex2lem2  28373  eucrct2eupth  28510  numclwwlk1lem2foalem  28616  numclwwlk1lem2fo  28623  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  numclwwlk6  28655  smcnlem  28960  fzm1ne1  31012  bcm1n  31018  fzom1ne1  31024  ltesubnnd  31038  wrdt2ind  31127  omndmul2  31240  psgnfzto1stlem  31269  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  archirngz  31345  archiabllem1a  31347  archiabllem2c  31351  freshmansdream  31386  ccfldextdgrr  31644  1smat1  31656  madjusmdetlem2  31680  madjusmdetlem4  31682  dya2icoseg  32144  iwrdsplit  32254  fibp1  32268  ballotlemfp1  32358  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemic  32373  ballotlem1c  32374  ballotlemsgt1  32377  ballotlemsdom  32378  ballotlemsel1i  32379  ballotlemsi  32381  ballotlemsima  32382  ballotlem1ri  32401  sgn0bi  32414  signstfvn  32448  signsvtn0  32449  signstfveq0  32456  signsvfn  32461  signsvtn  32463  signshf  32467  hashreprin  32500  circlemeth  32520  logdivsqrle  32530  revpfxsfxrev  32977  revwlk  32986  swrdwlk  32988  subfacp1lem1  33041  subfacp1lem5  33046  cvxpconn  33104  sinccvglem  33530  divcnvlin  33604  bcm1nt  33609  bcprod  33610  bccolsum  33611  iprodgam  33614  faclimlem1  33615  faclimlem2  33616  faclimlem3  33617  faclim  33618  iprodfac  33619  faclim2  33620  fwddifnp1  34394  dnizphlfeqhlf  34583  dnibndlem3  34587  dnibndlem13  34597  unblimceq0  34614  knoppndvlem6  34624  knoppndvlem9  34627  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem16  34634  knoppndvlem17  34635  bj-bary1lem1  35409  irrdiff  35424  poimirlem25  35729  poimirlem26  35730  poimirlem32  35736  opnmbllem0  35740  itg2addnclem2  35756  dvasin  35788  dvacos  35789  areacirclem1  35792  areacirclem4  35795  areacirc  35797  bfp  35909  fzsplitnd  39919  lcmfunnnd  39948  lcmineqlem1  39965  lcmineqlem3  39967  lcmineqlem4  39968  lcmineqlem7  39971  lcmineqlem8  39972  lcmineqlem10  39974  lcmineqlem11  39975  lcmineqlem12  39976  lcmineqlem18  39982  lcmineqlem19  39983  lcmineqlem22  39986  lcmineqlem23  39987  dvrelogpow2b  40004  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p3  40014  aks4d1p7d1  40018  2np3bcnp1  40028  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones16  40046  sticksstones22  40052  metakunt8  40060  metakunt12  40064  metakunt15  40067  metakunt16  40068  metakunt28  40080  nnadd1com  40218  nnaddcom  40219  nnadddir  40221  nnmul1com  40222  nnmulcom  40223  reixi  40325  sn-mulid2  40338  sn-0tie0  40342  fltnltalem  40415  fltnlta  40416  3cubeslem1  40422  3cubeslem2  40423  3cubeslem4  40427  pell1qrge1  40608  rmspecfund  40647  acongeq  40721  jm2.18  40726  jm2.19lem3  40729  jm2.25  40737  jm2.16nn0  40742  jm3.1lem1  40755  jm3.1lem2  40756  areaquad  40963  relexpmulnn  41206  relexpaddss  41215  cvgdvgrat  41820  radcnvrat  41821  hashnzfzclim  41829  ofdivrec  41833  expgrowthi  41840  bccm1k  41849  dvradcnv2  41854  binomcxplemwb  41855  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  refsum2cnlem1  42469  fzisoeu  42729  fperiodmullem  42732  fzdifsuc2  42739  xralrple2  42783  nnsplit  42787  infleinflem2  42800  fmul01lt1lem2  43016  fprodcn  43031  clim1fr1  43032  isumneg  43033  climneg  43041  sumnnodd  43061  reclimc  43084  coseq0  43295  coskpi2  43297  cosknegpi  43300  fprodcncf  43331  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnxpaek  43373  dvnmul  43374  dvmptfprod  43376  dvnprodlem3  43379  itgsinexp  43386  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem1  43432  stoweidlem7  43438  stoweidlem10  43441  stoweidlem11  43442  stoweidlem14  43445  stoweidlem17  43448  stoweidlem34  43465  stoweidlem42  43473  wallispilem3  43498  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem15  43519  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem11  43549  fourierdlem15  43553  fourierdlem26  43564  fourierdlem36  43574  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem56  43593  fourierdlem58  43595  fourierdlem59  43596  fourierdlem62  43599  fourierdlem64  43601  fourierdlem65  43602  fourierdlem78  43615  fourierdlem79  43616  sqwvfoura  43659  fourierswlem  43661  fouriersw  43662  etransclem23  43688  etransclem24  43689  etransclem28  43693  etransclem35  43700  etransclem38  43703  nnfoctbdjlem  43883  smfmullem1  44212  sigaradd  44269  deccarry  44691  fargshiftf1  44781  fargshiftfo  44782  fmtnof1  44875  sqrtpwpw2p  44878  fmtnorec2lem  44882  fmtnorec4  44889  fmtnoprmfac1lem  44904  fmtnoprmfac1  44905  fmtnoprmfac2  44907  2pwp1prm  44929  mod42tp1mod8  44942  sfprmdvdsmersenne  44943  lighneallem3  44947  lighneallem4  44950  onego  44986  zofldiv2ALTV  45002  oexpnegALTV  45017  opoeALTV  45023  opeoALTV  45024  epee  45045  perfectALTVlem1  45061  fppr2odd  45071  fpprwppr  45079  0nodd  45252  2nodd  45254  nnsgrpnmnd  45260  1neven  45378  altgsumbc  45576  pw2m1lepw2m1  45749  m1modmmod  45755  zofldiv2  45765  nnpw2pmod  45817  blen1b  45822  blennn0em1  45825  dignn0flhalflem1  45849  dignn0flhalflem2  45850  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  nn0sumshdiglem2  45856  itcovalpclem2  45905  ackval1  45915  ackval2  45916  ackval3  45917  affineid  45938  1subrec1sub  45939  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2vlinest  45975