Theorem 1cnd 11169

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  1c1 11069

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

This theorem is referenced by:  adddirp1d  11200  1p1times  11345  addcom  11360  addcomd  11376  muladd11r  11387  pncan1  11602  npcan1  11603  muls1d  11638  mulsubfacd  11639  recrec  11879  rec11  11880  rec11r  11881  rereccl  11900  subrecd  12011  nn1m1nn  12207  add1p1  12433  sub1m1  12434  cnm2m1cnm3  12435  xp1d2m1eqxm1d2  12436  div4p1lem1div2  12437  nn0n0n1ge2  12510  zneo  12617  rpnnen1lem5  12940  lincmb01cmp  13456  iccf1o  13457  xov1plusxeqvd  13459  zpnn0elfzo1  13700  ubmelm1fzo  13724  fzosplitpr  13737  fzosplitprm1  13738  fzoshftral  13745  fladdz  13787  2tnp1ge0ge0  13791  ltdifltdiv  13796  dfceil2  13801  negmod  13881  modnegd  13891  addmodlteq  13911  binom2sub1  14186  binom3  14189  zesq  14191  sqoddm1div8  14208  bcm1k  14280  bcp1n  14281  bcp1m1  14285  bcpasc  14286  bcn2m1  14289  hashfz  14392  hashfzo  14394  hashfzp1  14396  hashf1lem2  14421  hashf1  14422  hashdifsnp1  14471  lswccatn0lsw  14556  ccatws1lenp1b  14586  revccat  14731  repswrevw  14752  cshwidxm1  14772  cshwidxn  14774  cshweqrep  14786  cshimadifsn0  14796  swrds2m  14907  swrd2lsw  14918  relexpaddnn  15017  absexpz  15271  reccn2  15563  rlimno1  15620  isercolllem1  15631  isercoll2  15635  iseraltlem2  15649  iseraltlem3  15650  fsump1  15722  hashiun  15788  hash2iun1dif1  15790  binomlem  15795  bcxmas  15801  incexc  15803  incexc2  15804  climcndslem1  15815  arisum  15826  arisum2  15827  trireciplem  15828  pwdif  15834  pwm1geoser  15835  geolim2  15837  georeclim  15838  mertenslem1  15850  prodfrec  15861  ntrivcvg  15863  ntrivcvgtail  15866  prodrblem  15895  prodmolem2a  15900  fprodntriv  15908  prod1  15910  fprodser  15915  fprodcl  15918  fprodm1  15933  fprodp1  15935  fprodclf  15958  risefacval2  15976  fallfacval2  15977  risefacp1  15995  fallfacp1  15996  risefacfac  16001  fallfacfwd  16002  binomfallfaclem2  16006  fallfacval4  16009  bpolydiflem  16020  ef0lem  16044  tanaddlem  16134  tanadd  16135  cos01bnd  16154  oddm1even  16313  oddp1even  16314  oexpneg  16315  ltoddhalfle  16331  halfleoddlt  16332  nn0ob  16354  pwp1fsum  16361  flodddiv4  16385  bitsp1o  16403  bitsf1  16416  sadcp1  16425  qredeu  16628  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  gsumsgrpccat  18767  psgnunilem5  19424  psgnunilem2  19425  sylow1lem1  19528  efgredlemc  19675  odadd2  19779  ablsimpgfindlem1  20039  srgbinomlem3  20137  srgbinomlem4  20138  cncrng  21300  cncrngOLD  21301  gzrngunit  21350  zringunit  21376  prmirredlem  21382  pzriprnglem12  21402  freshmansdream  21484  mhppwdeg  22037  psdmul  22053  cayhamlem1  22753  expcn  24763  expcnOLD  24765  iirevcn  24824  iihalf2cn  24829  iihalf2cnOLD  24830  icchmeo  24838  icchmeoOLD  24839  icopnfcnv  24840  icopnfhmeo  24841  evth  24858  pcoass  24924  pjthlem1  25337  ovolunlem1a  25397  ovolunlem1  25398  opnmbllem  25502  mbfi1fseqlem6  25621  bddibl  25741  dvnadd  25831  dvmptid  25861  dvmptdiv  25878  dvcnvlem  25880  dveflem  25883  dvef  25884  dvsincos  25885  dvlipcn  25899  dvivthlem1  25913  lhop2  25920  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgpowd  25957  ply1divex  26042  fta1glem1  26073  dgrcolem1  26179  dgrcolem2  26180  vieta1lem1  26218  aaliou3lem2  26251  aaliou3lem8  26253  dvtaylp  26278  dvntaylp  26279  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  abelthlem1  26341  abelthlem2  26342  abelthlem6  26346  abelthlem7  26348  logdivlti  26529  advlog  26563  advlogexp  26564  logtayl  26569  cxpmul2  26598  dvcxp1  26649  dvcxp2  26650  dvcncxp1  26652  dvcnsqrt  26653  loglesqrt  26671  relogbdiv  26689  ang180lem4  26722  ang180lem5  26723  isosctrlem2  26729  isosctrlem3  26730  affineequiv  26733  affineequiv2  26734  affineequiv3  26735  angpieqvdlem  26738  chordthmlem2  26743  chordthmlem3  26744  chordthmlem5  26746  dcubic2  26754  dcubic  26756  quart1lem  26765  quart1  26766  quart  26771  asinlem  26778  asinlem3  26781  atansopn  26842  dvatan  26845  leibpi  26852  birthdaylem2  26862  efrlim  26879  efrlimOLD  26880  cxplim  26882  divsqrtsumlem  26890  logdifbnd  26904  emcllem2  26907  emcllem3  26908  emcllem5  26910  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  lgam1  26974  gamfac  26977  wilthlem2  26979  wilthimp  26982  ftalem5  26987  basellem3  26993  basellem5  26995  basellem8  26998  basellem9  26999  sqff1o  27092  muinv  27103  logfaclbnd  27133  logfacrlim  27135  logexprlim  27136  perfectlem2  27141  dchr1cl  27162  dchrinvcl  27164  dchrfi  27166  dchr1  27168  dchrsum2  27179  bcmono  27188  bcp1ctr  27190  bclbnd  27191  bposlem9  27203  gausslemma2dlem1a  27276  gausslemma2dlem5  27282  lgseisenlem4  27289  lgsquadlem1  27291  m1lgs  27299  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3d1  27314  2lgsoddprmlem1  27319  2sqlem8  27337  2sq2  27344  addsqn2reu  27352  addsqrexnreu  27353  addsqnreup  27354  addsq2nreurex  27355  chtppilim  27386  rpvmasumlem  27398  dchrisumlem1  27400  dchrisum0re  27424  dchrisum0lem2a  27428  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  2vmadivsumlem  27451  selberg4lem1  27471  pntrsumo1  27476  selberg34r  27482  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntibndlem2  27502  pntlemg  27509  pntlemr  27513  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntlem3  27520  ostth2lem2  27545  ttgcontlem1  28812  cusgrsize2inds  29381  wlklenvclwlk  29583  pthdadjvtx  29658  crctcshwlkn0lem1  29740  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  wlklnwwlkln2lem  29812  wlknwwlksnbij  29818  wwlksnred  29822  wwlksnext  29823  wwlksnextbi  29824  wwlksnredwwlkn  29825  wwlksnextwrd  29827  wwlksnextinj  29829  wwlksnextproplem2  29840  wwlksnextproplem3  29841  clwwlkccatlem  29918  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlklem3  29930  clwlkclwwlk  29931  clwwisshclwwslemlem  29942  clwwisshclwws  29944  clwwlkel  29975  clwwlkf  29976  clwwlkwwlksb  29983  clwwlkext2edg  29985  wwlksext2clwwlk  29986  clwwlknonex2lem1  30036  clwwlknonex2lem2  30037  eucrct2eupth  30174  numclwwlk1lem2foalem  30280  numclwwlk1lem2fo  30287  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  numclwwlk6  30319  smcnlem  30626  receqid  32668  fzm1ne1  32711  bcm1n  32718  fzom1ne1  32724  ltesubnnd  32747  sgn0bi  32765  oexpled  32772  wrdt2ind  32875  chnub  32938  chnlt  32939  omndmul2  33026  psgnfzto1stlem  33057  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  archirngz  33143  archiabllem1a  33145  archiabllem2c  33149  ccfldextdgrr  33667  constrfin  33736  nn0constr  33751  iconstr  33756  constrrecl  33759  constrimcl  33760  constrreinvcl  33762  constrinvcl  33763  constrresqrtcl  33767  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminply  33778  cos9thpinconstrlem1  33779  1smat1  33794  madjusmdetlem2  33818  madjusmdetlem4  33820  dya2icoseg  34268  iwrdsplit  34378  fibp1  34392  ballotlemfp1  34483  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemic  34498  ballotlem1c  34499  ballotlemsgt1  34502  ballotlemsdom  34503  ballotlemsel1i  34504  ballotlemsi  34506  ballotlemsima  34507  ballotlem1ri  34526  signstfvn  34560  signsvtn0  34561  signstfveq0  34568  signsvfn  34573  signsvtn  34575  signshf  34579  hashreprin  34611  circlemeth  34631  logdivsqrle  34641  revpfxsfxrev  35103  revwlk  35112  swrdwlk  35114  subfacp1lem1  35166  subfacp1lem5  35171  cvxpconn  35229  sinccvglem  35659  divcnvlin  35720  bcm1nt  35724  bcprod  35725  bccolsum  35726  iprodgam  35729  faclimlem1  35730  faclimlem2  35731  faclimlem3  35732  faclim  35733  iprodfac  35734  faclim2  35735  fwddifnp1  36153  dnizphlfeqhlf  36464  dnibndlem3  36468  dnibndlem13  36478  unblimceq0  36495  knoppndvlem6  36505  knoppndvlem9  36508  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem16  36515  knoppndvlem17  36516  bj-bary1lem1  37299  irrdiff  37314  poimirlem25  37639  poimirlem26  37640  poimirlem32  37646  opnmbllem0  37650  itg2addnclem2  37666  dvasin  37698  dvacos  37699  areacirclem1  37702  areacirclem4  37705  areacirc  37707  bfp  37818  fzsplitnd  41970  lcmfunnnd  42000  lcmineqlem1  42017  lcmineqlem3  42019  lcmineqlem4  42020  lcmineqlem7  42023  lcmineqlem8  42024  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem12  42028  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem22  42038  lcmineqlem23  42039  dvrelogpow2b  42056  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks4d1p7d1  42070  primrootsunit1  42085  posbezout  42088  primrootscoprbij  42090  primrootspoweq0  42094  aks6d1c1  42104  hashscontpow1  42109  2np3bcnp1  42132  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones16  42150  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c7lem1  42168  unitscyglem5  42187  nnadd1com  42255  nnaddcom  42256  nnadddir  42258  nnmul1com  42259  nnmulcom  42260  3rdpwhole  42280  fz1sump1  42298  oddnumth  42299  nicomachus  42300  sumcubes  42301  tan3rdpi  42340  redvmptabs  42348  readvrec  42350  reixi  42411  sn-mullid  42424  sn-0tie0  42439  renegmulnnass  42453  fiabv  42524  fltnltalem  42650  fltnlta  42651  3cubeslem1  42672  3cubeslem2  42673  3cubeslem4  42677  pell1qrge1  42858  rmspecfund  42897  acongeq  42972  jm2.18  42977  jm2.19lem3  42980  jm2.25  42988  jm2.16nn0  42993  jm3.1lem1  43006  jm3.1lem2  43007  areaquad  43205  relexpmulnn  43698  relexpaddss  43707  cvgdvgrat  44302  radcnvrat  44303  hashnzfzclim  44311  ofdivrec  44315  expgrowthi  44322  bccm1k  44331  dvradcnv2  44336  binomcxplemwb  44337  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  refsum2cnlem1  45031  fzisoeu  45298  fperiodmullem  45301  fzdifsuc2  45308  xralrple2  45350  nnsplit  45354  infleinflem2  45367  fmul01lt1lem2  45583  fprodcn  45598  clim1fr1  45599  isumneg  45600  climneg  45608  sumnnodd  45628  reclimc  45651  coseq0  45862  coskpi2  45864  cosknegpi  45867  fprodcncf  45898  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnmul  45941  dvmptfprod  45943  dvnprodlem3  45946  itgsinexp  45953  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem1  45999  stoweidlem7  46005  stoweidlem10  46008  stoweidlem11  46009  stoweidlem14  46012  stoweidlem17  46015  stoweidlem34  46032  stoweidlem42  46040  wallispilem3  46065  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem15  46086  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem11  46116  fourierdlem15  46120  fourierdlem26  46131  fourierdlem36  46141  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem56  46160  fourierdlem58  46162  fourierdlem59  46163  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem78  46182  fourierdlem79  46183  sqwvfoura  46226  fourierswlem  46228  fouriersw  46229  etransclem23  46255  etransclem24  46256  etransclem28  46260  etransclem35  46267  etransclem38  46270  nnfoctbdjlem  46453  smfmullem1  46789  sigaradd  46864  cjnpoly  46890  deccarry  47312  ceilbi  47334  m1modne  47349  m1modmmod  47359  modm1nep2  47369  modm1nem2  47370  fargshiftf1  47442  fargshiftfo  47443  fmtnof1  47536  sqrtpwpw2p  47539  fmtnorec2lem  47543  fmtnorec4  47550  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  fmtnoprmfac2  47568  2pwp1prm  47590  mod42tp1mod8  47603  sfprmdvdsmersenne  47604  lighneallem3  47608  lighneallem4  47611  onego  47647  zofldiv2ALTV  47663  oexpnegALTV  47678  opoeALTV  47684  opeoALTV  47685  epee  47706  perfectALTVlem1  47722  fppr2odd  47732  fpprwppr  47740  gpg3nbgrvtx0  48067  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  0nodd  48158  2nodd  48160  nnsgrpnmnd  48166  1neven  48226  altgsumbc  48340  pw2m1lepw2m1  48509  zofldiv2  48520  nnpw2pmod  48572  blen1b  48577  blennn0em1  48580  dignn0flhalflem1  48604  dignn0flhalflem2  48605  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdiglem2  48611  itcovalpclem2  48660  ackval1  48670  ackval2  48671  ackval3  48672  affineid  48693  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2vlinest  48730