Theorem 1cnd 11110

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  1c1 11010

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

This theorem is referenced by:  adddirp1d  11141  1p1times  11287  addcom  11302  addcomd  11318  muladd11r  11329  pncan1  11544  npcan1  11545  muls1d  11580  mulsubfacd  11581  recrec  11821  rec11  11822  rec11r  11823  rereccl  11842  subrecd  11953  nn1m1nn  12149  add1p1  12375  sub1m1  12376  cnm2m1cnm3  12377  xp1d2m1eqxm1d2  12378  div4p1lem1div2  12379  nn0n0n1ge2  12452  zneo  12559  rpnnen1lem5  12882  lincmb01cmp  13398  iccf1o  13399  xov1plusxeqvd  13401  zpnn0elfzo1  13642  ubmelm1fzo  13666  fzosplitpr  13679  fzosplitprm1  13680  fzoshftral  13687  fladdz  13729  2tnp1ge0ge0  13733  ltdifltdiv  13738  dfceil2  13743  negmod  13823  modnegd  13833  addmodlteq  13853  binom2sub1  14128  binom3  14131  zesq  14133  sqoddm1div8  14150  bcm1k  14222  bcp1n  14223  bcp1m1  14227  bcpasc  14228  bcn2m1  14231  hashfz  14334  hashfzo  14336  hashfzp1  14338  hashf1lem2  14363  hashf1  14364  hashdifsnp1  14413  lswccatn0lsw  14498  ccatws1lenp1b  14528  revccat  14672  repswrevw  14693  cshwidxm1  14713  cshwidxn  14715  cshweqrep  14727  cshimadifsn0  14737  swrds2m  14848  swrd2lsw  14859  relexpaddnn  14958  absexpz  15212  reccn2  15504  rlimno1  15561  isercolllem1  15572  isercoll2  15576  iseraltlem2  15590  iseraltlem3  15591  fsump1  15663  hashiun  15729  hash2iun1dif1  15731  binomlem  15736  bcxmas  15742  incexc  15744  incexc2  15745  climcndslem1  15756  arisum  15767  arisum2  15768  trireciplem  15769  pwdif  15775  pwm1geoser  15776  geolim2  15778  georeclim  15779  mertenslem1  15791  prodfrec  15802  ntrivcvg  15804  ntrivcvgtail  15807  prodrblem  15836  prodmolem2a  15841  fprodntriv  15849  prod1  15851  fprodser  15856  fprodcl  15859  fprodm1  15874  fprodp1  15876  fprodclf  15899  risefacval2  15917  fallfacval2  15918  risefacp1  15936  fallfacp1  15937  risefacfac  15942  fallfacfwd  15943  binomfallfaclem2  15947  fallfacval4  15950  bpolydiflem  15961  ef0lem  15985  tanaddlem  16075  tanadd  16076  cos01bnd  16095  oddm1even  16254  oddp1even  16255  oexpneg  16256  ltoddhalfle  16272  halfleoddlt  16273  nn0ob  16295  pwp1fsum  16302  flodddiv4  16326  bitsp1o  16344  bitsf1  16357  sadcp1  16366  qredeu  16569  prmdiv  16696  prmdiveq  16697  vfermltlALT  16714  pc2dvds  16791  4sqlem11  16867  4sqlem12  16868  vdwapun  16886  vdwlem3  16895  vdwlem6  16898  vdwlem9  16901  ramub1lem2  16939  prmop1  16950  prmdvdsprmo  16954  prmgaplem8  16970  cshwshashnsame  17015  gsumsgrpccat  18714  psgnunilem5  19373  psgnunilem2  19374  sylow1lem1  19477  efgredlemc  19624  odadd2  19728  ablsimpgfindlem1  19988  omndmul2  20012  srgbinomlem3  20113  srgbinomlem4  20114  cncrng  21295  cncrngOLD  21296  gzrngunit  21340  zringunit  21373  prmirredlem  21379  pzriprnglem12  21399  freshmansdream  21481  mhppwdeg  22035  psdmul  22051  cayhamlem1  22751  expcn  24761  expcnOLD  24763  iirevcn  24822  iihalf2cn  24827  iihalf2cnOLD  24828  icchmeo  24836  icchmeoOLD  24837  icopnfcnv  24838  icopnfhmeo  24839  evth  24856  pcoass  24922  pjthlem1  25335  ovolunlem1a  25395  ovolunlem1  25396  opnmbllem  25500  mbfi1fseqlem6  25619  bddibl  25739  dvnadd  25829  dvmptid  25859  dvmptdiv  25876  dvcnvlem  25878  dveflem  25881  dvef  25882  dvsincos  25883  dvlipcn  25897  dvivthlem1  25911  lhop2  25918  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  itgpowd  25955  ply1divex  26040  fta1glem1  26071  dgrcolem1  26177  dgrcolem2  26178  vieta1lem1  26216  aaliou3lem2  26249  aaliou3lem8  26251  dvtaylp  26276  dvntaylp  26277  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  abelthlem1  26339  abelthlem2  26340  abelthlem6  26344  abelthlem7  26346  logdivlti  26527  advlog  26561  advlogexp  26562  logtayl  26567  cxpmul2  26596  dvcxp1  26647  dvcxp2  26648  dvcncxp1  26650  dvcnsqrt  26651  loglesqrt  26669  relogbdiv  26687  ang180lem4  26720  ang180lem5  26721  isosctrlem2  26727  isosctrlem3  26728  affineequiv  26731  affineequiv2  26732  affineequiv3  26733  angpieqvdlem  26736  chordthmlem2  26741  chordthmlem3  26742  chordthmlem5  26744  dcubic2  26752  dcubic  26754  quart1lem  26763  quart1  26764  quart  26769  asinlem  26776  asinlem3  26779  atansopn  26840  dvatan  26843  leibpi  26850  birthdaylem2  26860  efrlim  26877  efrlimOLD  26878  cxplim  26880  divsqrtsumlem  26888  logdifbnd  26902  emcllem2  26905  emcllem3  26906  emcllem5  26908  zetacvg  26923  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem4  26940  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  lgam1  26972  gamfac  26975  wilthlem2  26977  wilthimp  26980  ftalem5  26985  basellem3  26991  basellem5  26993  basellem8  26996  basellem9  26997  sqff1o  27090  muinv  27101  logfaclbnd  27131  logfacrlim  27133  logexprlim  27134  perfectlem2  27139  dchr1cl  27160  dchrinvcl  27162  dchrfi  27164  dchr1  27166  dchrsum2  27177  bcmono  27186  bcp1ctr  27188  bclbnd  27189  bposlem9  27201  gausslemma2dlem1a  27274  gausslemma2dlem5  27280  lgseisenlem4  27287  lgsquadlem1  27289  m1lgs  27297  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2lgslem3d1  27312  2lgsoddprmlem1  27317  2sqlem8  27335  2sq2  27342  addsqn2reu  27350  addsqrexnreu  27351  addsqnreup  27352  addsq2nreurex  27353  chtppilim  27384  rpvmasumlem  27396  dchrisumlem1  27398  dchrisum0re  27422  dchrisum0lem2a  27426  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  2vmadivsumlem  27449  selberg4lem1  27469  pntrsumo1  27474  selberg34r  27480  pntrlog2bndlem2  27487  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntibndlem2  27500  pntlemg  27507  pntlemr  27511  pntlemf  27514  pntlemk  27515  pntlemo  27516  pntlem3  27518  ostth2lem2  27543  ttgcontlem1  28830  cusgrsize2inds  29399  wlklenvclwlk  29599  pthdadjvtx  29673  crctcshwlkn0lem1  29755  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  wlklnwwlkln2lem  29827  wlknwwlksnbij  29833  wwlksnred  29837  wwlksnext  29838  wwlksnextbi  29839  wwlksnredwwlkn  29840  wwlksnextwrd  29842  wwlksnextinj  29844  wwlksnextproplem2  29855  wwlksnextproplem3  29856  clwwlkccatlem  29933  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwlkclwwlklem3  29945  clwlkclwwlk  29946  clwwisshclwwslemlem  29957  clwwisshclwws  29959  clwwlkel  29990  clwwlkf  29991  clwwlkwwlksb  29998  clwwlkext2edg  30000  wwlksext2clwwlk  30001  clwwlknonex2lem1  30051  clwwlknonex2lem2  30052  eucrct2eupth  30189  numclwwlk1lem2foalem  30295  numclwwlk1lem2fo  30302  numclwlk2lem2f  30321  numclwlk2lem2f1o  30323  numclwwlk6  30334  smcnlem  30641  receqid  32688  fzm1ne1  32731  bcm1n  32738  fzom1ne1  32744  ltesubnnd  32767  sgn0bi  32785  oexpled  32792  wrdt2ind  32895  chnub  32954  chnlt  32955  psgnfzto1stlem  33042  cycpmco2lem3  33070  cycpmco2lem4  33071  cycpmco2lem5  33072  cycpmco2lem6  33073  cycpmco2lem7  33074  cycpmco2  33075  archirngz  33131  archiabllem1a  33133  archiabllem2c  33137  ccfldextdgrr  33639  constrfin  33713  nn0constr  33728  iconstr  33733  constrrecl  33736  constrimcl  33737  constrreinvcl  33739  constrinvcl  33740  constrresqrtcl  33744  2sqr3minply  33747  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpiminply  33755  cos9thpinconstrlem1  33756  1smat1  33771  madjusmdetlem2  33795  madjusmdetlem4  33797  dya2icoseg  34245  iwrdsplit  34355  fibp1  34369  ballotlemfp1  34460  ballotlemfc0  34461  ballotlemfcc  34462  ballotlemic  34475  ballotlem1c  34476  ballotlemsgt1  34479  ballotlemsdom  34480  ballotlemsel1i  34481  ballotlemsi  34483  ballotlemsima  34484  ballotlem1ri  34503  signstfvn  34537  signsvtn0  34538  signstfveq0  34545  signsvfn  34550  signsvtn  34552  signshf  34556  hashreprin  34588  circlemeth  34608  logdivsqrle  34618  revpfxsfxrev  35093  revwlk  35102  swrdwlk  35104  subfacp1lem1  35156  subfacp1lem5  35161  cvxpconn  35219  sinccvglem  35649  divcnvlin  35710  bcm1nt  35714  bcprod  35715  bccolsum  35716  iprodgam  35719  faclimlem1  35720  faclimlem2  35721  faclimlem3  35722  faclim  35723  iprodfac  35724  faclim2  35725  fwddifnp1  36143  dnizphlfeqhlf  36454  dnibndlem3  36458  dnibndlem13  36468  unblimceq0  36485  knoppndvlem6  36495  knoppndvlem9  36498  knoppndvlem14  36503  knoppndvlem15  36504  knoppndvlem16  36505  knoppndvlem17  36506  bj-bary1lem1  37289  irrdiff  37304  poimirlem25  37629  poimirlem26  37630  poimirlem32  37636  opnmbllem0  37640  itg2addnclem2  37656  dvasin  37688  dvacos  37689  areacirclem1  37692  areacirclem4  37695  areacirc  37697  bfp  37808  fzsplitnd  41959  lcmfunnnd  41989  lcmineqlem1  42006  lcmineqlem3  42008  lcmineqlem4  42009  lcmineqlem7  42012  lcmineqlem8  42013  lcmineqlem10  42015  lcmineqlem11  42016  lcmineqlem12  42017  lcmineqlem18  42023  lcmineqlem19  42024  lcmineqlem22  42027  lcmineqlem23  42028  dvrelogpow2b  42045  aks4d1p1p4  42048  aks4d1p1p6  42050  aks4d1p1p7  42051  aks4d1p1p5  42052  aks4d1p1  42053  aks4d1p3  42055  aks4d1p7d1  42059  primrootsunit1  42074  posbezout  42077  primrootscoprbij  42079  primrootspoweq0  42083  aks6d1c1  42093  hashscontpow1  42098  2np3bcnp1  42121  sticksstones10  42132  sticksstones12a  42134  sticksstones12  42135  sticksstones16  42139  sticksstones22  42145  aks6d1c6lem3  42149  aks6d1c7lem1  42157  unitscyglem5  42176  nnadd1com  42244  nnaddcom  42245  nnadddir  42247  nnmul1com  42248  nnmulcom  42249  3rdpwhole  42269  fz1sump1  42287  oddnumth  42288  nicomachus  42289  sumcubes  42290  tan3rdpi  42329  redvmptabs  42337  readvrec  42339  reixi  42400  sn-mullid  42413  sn-0tie0  42428  renegmulnnass  42442  fiabv  42513  fltnltalem  42639  fltnlta  42640  3cubeslem1  42661  3cubeslem2  42662  3cubeslem4  42666  pell1qrge1  42847  rmspecfund  42886  acongeq  42960  jm2.18  42965  jm2.19lem3  42968  jm2.25  42976  jm2.16nn0  42981  jm3.1lem1  42994  jm3.1lem2  42995  areaquad  43193  relexpmulnn  43686  relexpaddss  43695  cvgdvgrat  44290  radcnvrat  44291  hashnzfzclim  44299  ofdivrec  44303  expgrowthi  44310  bccm1k  44319  dvradcnv2  44324  binomcxplemwb  44325  binomcxplemnn0  44326  binomcxplemrat  44327  binomcxplemfrat  44328  binomcxplemdvbinom  44330  binomcxplemnotnn0  44333  refsum2cnlem1  45019  fzisoeu  45286  fperiodmullem  45289  fzdifsuc2  45296  xralrple2  45338  nnsplit  45342  infleinflem2  45354  fmul01lt1lem2  45570  fprodcn  45585  clim1fr1  45586  isumneg  45587  climneg  45595  sumnnodd  45615  reclimc  45638  coseq0  45849  coskpi2  45851  cosknegpi  45854  fprodcncf  45885  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnxpaek  45927  dvnmul  45928  dvmptfprod  45930  dvnprodlem3  45933  itgsinexp  45940  itgiccshift  45965  itgperiod  45966  itgsbtaddcnst  45967  stoweidlem1  45986  stoweidlem7  45992  stoweidlem10  45995  stoweidlem11  45996  stoweidlem14  45999  stoweidlem17  46002  stoweidlem34  46019  stoweidlem42  46027  wallispilem3  46052  wallispilem5  46054  wallispi  46055  wallispi2lem1  46056  wallispi2lem2  46057  wallispi2  46058  stirlinglem1  46059  stirlinglem3  46061  stirlinglem4  46062  stirlinglem5  46063  stirlinglem6  46064  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  stirlinglem11  46069  stirlinglem12  46070  stirlinglem13  46071  stirlinglem15  46073  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  dirkertrigeq  46086  dirkercncflem1  46088  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem11  46103  fourierdlem15  46107  fourierdlem26  46118  fourierdlem36  46128  fourierdlem40  46132  fourierdlem41  46133  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem56  46147  fourierdlem58  46149  fourierdlem59  46150  fourierdlem62  46153  fourierdlem64  46155  fourierdlem65  46156  fourierdlem78  46169  fourierdlem79  46170  sqwvfoura  46213  fourierswlem  46215  fouriersw  46216  etransclem23  46242  etransclem24  46243  etransclem28  46247  etransclem35  46254  etransclem38  46257  nnfoctbdjlem  46440  smfmullem1  46776  sigaradd  46851  cjnpoly  46877  deccarry  47299  ceilbi  47321  m1modne  47336  m1modmmod  47346  modm1nep2  47356  modm1nem2  47357  fargshiftf1  47429  fargshiftfo  47430  fmtnof1  47523  sqrtpwpw2p  47526  fmtnorec2lem  47530  fmtnorec4  47537  fmtnoprmfac1lem  47552  fmtnoprmfac1  47553  fmtnoprmfac2  47555  2pwp1prm  47577  mod42tp1mod8  47590  sfprmdvdsmersenne  47591  lighneallem3  47595  lighneallem4  47598  onego  47634  zofldiv2ALTV  47650  oexpnegALTV  47665  opoeALTV  47671  opeoALTV  47672  epee  47693  perfectALTVlem1  47709  fppr2odd  47719  fpprwppr  47727  gpg3nbgrvtx0  48064  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  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