Theorem 1cnd 11256

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  1c1 11156

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

This theorem is referenced by:  adddirp1d  11287  1p1times  11432  addcom  11447  addcomd  11463  muladd11r  11474  pncan1  11687  npcan1  11688  muls1d  11723  mulsubfacd  11724  recrec  11964  rec11  11965  rec11r  11966  rereccl  11985  subrec  12096  nn1m1nn  12287  add1p1  12517  sub1m1  12518  cnm2m1cnm3  12519  xp1d2m1eqxm1d2  12520  div4p1lem1div2  12521  nn0n0n1ge2  12594  zneo  12701  rpnnen1lem5  13023  lincmb01cmp  13535  iccf1o  13536  xov1plusxeqvd  13538  zpnn0elfzo1  13778  ubmelm1fzo  13802  fzosplitpr  13815  fzosplitprm1  13816  fzoshftral  13823  fladdz  13865  2tnp1ge0ge0  13869  ltdifltdiv  13874  dfceil2  13879  negmod  13957  modnegd  13967  addmodlteq  13987  binom2sub1  14260  binom3  14263  zesq  14265  sqoddm1div8  14282  bcm1k  14354  bcp1n  14355  bcp1m1  14359  bcpasc  14360  bcn2m1  14363  hashfz  14466  hashfzo  14468  hashfzp1  14470  hashf1lem2  14495  hashf1  14496  hashdifsnp1  14545  lswccatn0lsw  14629  ccatws1lenp1b  14659  revccat  14804  repswrevw  14825  cshwidxm1  14845  cshwidxn  14847  cshweqrep  14859  cshimadifsn0  14869  swrds2m  14980  swrd2lsw  14991  relexpaddnn  15090  absexpz  15344  reccn2  15633  rlimno1  15690  isercolllem1  15701  isercoll2  15705  iseraltlem2  15719  iseraltlem3  15720  fsump1  15792  hashiun  15858  hash2iun1dif1  15860  binomlem  15865  bcxmas  15871  incexc  15873  incexc2  15874  climcndslem1  15885  arisum  15896  arisum2  15897  trireciplem  15898  pwdif  15904  pwm1geoser  15905  geolim2  15907  georeclim  15908  mertenslem1  15920  prodfrec  15931  ntrivcvg  15933  ntrivcvgtail  15936  prodrblem  15965  prodmolem2a  15970  fprodntriv  15978  prod1  15980  fprodser  15985  fprodcl  15988  fprodm1  16003  fprodp1  16005  fprodclf  16028  risefacval2  16046  fallfacval2  16047  risefacp1  16065  fallfacp1  16066  risefacfac  16071  fallfacfwd  16072  binomfallfaclem2  16076  fallfacval4  16079  bpolydiflem  16090  ef0lem  16114  tanaddlem  16202  tanadd  16203  cos01bnd  16222  oddm1even  16380  oddp1even  16381  oexpneg  16382  ltoddhalfle  16398  halfleoddlt  16399  nn0ob  16421  pwp1fsum  16428  flodddiv4  16452  bitsp1o  16470  bitsf1  16483  sadcp1  16492  qredeu  16695  prmdiv  16822  prmdiveq  16823  vfermltlALT  16840  pc2dvds  16917  4sqlem11  16993  4sqlem12  16994  vdwapun  17012  vdwlem3  17021  vdwlem6  17024  vdwlem9  17027  ramub1lem2  17065  prmop1  17076  prmdvdsprmo  17080  prmgaplem8  17096  cshwshashnsame  17141  gsumsgrpccat  18853  psgnunilem5  19512  psgnunilem2  19513  sylow1lem1  19616  efgredlemc  19763  odadd2  19867  ablsimpgfindlem1  20127  srgbinomlem3  20225  srgbinomlem4  20226  cncrng  21401  cncrngOLD  21402  gzrngunit  21451  zringunit  21477  prmirredlem  21483  pzriprnglem12  21503  freshmansdream  21593  mhppwdeg  22154  psdmul  22170  cayhamlem1  22872  expcn  24896  expcnOLD  24898  iirevcn  24957  iihalf2cn  24962  iihalf2cnOLD  24963  icchmeo  24971  icchmeoOLD  24972  icopnfcnv  24973  icopnfhmeo  24974  evth  24991  pcoass  25057  pjthlem1  25471  ovolunlem1a  25531  ovolunlem1  25532  opnmbllem  25636  mbfi1fseqlem6  25755  bddibl  25875  dvnadd  25965  dvmptid  25995  dvmptdiv  26012  dvcnvlem  26014  dveflem  26017  dvef  26018  dvsincos  26019  dvlipcn  26033  dvivthlem1  26047  lhop2  26054  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgpowd  26091  ply1divex  26176  fta1glem1  26207  dgrcolem1  26313  dgrcolem2  26314  vieta1lem1  26352  aaliou3lem2  26385  aaliou3lem8  26387  dvtaylp  26412  dvntaylp  26413  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  abelthlem1  26475  abelthlem2  26476  abelthlem6  26480  abelthlem7  26482  logdivlti  26662  advlog  26696  advlogexp  26697  logtayl  26702  cxpmul2  26731  dvcxp1  26782  dvcxp2  26783  dvcncxp1  26785  dvcnsqrt  26786  loglesqrt  26804  relogbdiv  26822  ang180lem4  26855  ang180lem5  26856  isosctrlem2  26862  isosctrlem3  26863  affineequiv  26866  affineequiv2  26867  affineequiv3  26868  angpieqvdlem  26871  chordthmlem2  26876  chordthmlem3  26877  chordthmlem5  26879  dcubic2  26887  dcubic  26889  quart1lem  26898  quart1  26899  quart  26904  asinlem  26911  asinlem3  26914  atansopn  26975  dvatan  26978  leibpi  26985  birthdaylem2  26995  efrlim  27012  efrlimOLD  27013  cxplim  27015  divsqrtsumlem  27023  logdifbnd  27037  emcllem2  27040  emcllem3  27041  emcllem5  27043  zetacvg  27058  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  lgam1  27107  gamfac  27110  wilthlem2  27112  wilthimp  27115  ftalem5  27120  basellem3  27126  basellem5  27128  basellem8  27131  basellem9  27132  sqff1o  27225  muinv  27236  logfaclbnd  27266  logfacrlim  27268  logexprlim  27269  perfectlem2  27274  dchr1cl  27295  dchrinvcl  27297  dchrfi  27299  dchr1  27301  dchrsum2  27312  bcmono  27321  bcp1ctr  27323  bclbnd  27324  bposlem9  27336  gausslemma2dlem1a  27409  gausslemma2dlem5  27415  lgseisenlem4  27422  lgsquadlem1  27424  m1lgs  27432  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgslem3d1  27447  2lgsoddprmlem1  27452  2sqlem8  27470  2sq2  27477  addsqn2reu  27485  addsqrexnreu  27486  addsqnreup  27487  addsq2nreurex  27488  chtppilim  27519  rpvmasumlem  27531  dchrisumlem1  27533  dchrisum0re  27557  dchrisum0lem2a  27561  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  2vmadivsumlem  27584  selberg4lem1  27604  pntrsumo1  27609  selberg34r  27615  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntibndlem2  27635  pntlemg  27642  pntlemr  27646  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntlem3  27653  ostth2lem2  27678  ttgcontlem1  28899  cusgrsize2inds  29471  wlklenvclwlk  29673  pthdadjvtx  29748  crctcshwlkn0lem1  29830  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  wlklnwwlkln2lem  29902  wlknwwlksnbij  29908  wwlksnred  29912  wwlksnext  29913  wwlksnextbi  29914  wwlksnredwwlkn  29915  wwlksnextwrd  29917  wwlksnextinj  29919  wwlksnextproplem2  29930  wwlksnextproplem3  29931  clwwlkccatlem  30008  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlklem3  30020  clwlkclwwlk  30021  clwwisshclwwslemlem  30032  clwwisshclwws  30034  clwwlkel  30065  clwwlkf  30066  clwwlkwwlksb  30073  clwwlkext2edg  30075  wwlksext2clwwlk  30076  clwwlknonex2lem1  30126  clwwlknonex2lem2  30127  eucrct2eupth  30264  numclwwlk1lem2foalem  30370  numclwwlk1lem2fo  30377  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  numclwwlk6  30409  smcnlem  30716  fzm1ne1  32790  bcm1n  32797  fzom1ne1  32803  ltesubnnd  32824  wrdt2ind  32938  chnub  33002  chnlt  33003  omndmul2  33089  psgnfzto1stlem  33120  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  archirngz  33196  archiabllem1a  33198  archiabllem2c  33202  ccfldextdgrr  33722  constrfin  33787  2sqr3minply  33791  1smat1  33803  madjusmdetlem2  33827  madjusmdetlem4  33829  dya2icoseg  34279  iwrdsplit  34389  fibp1  34403  ballotlemfp1  34494  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemic  34509  ballotlem1c  34510  ballotlemsgt1  34513  ballotlemsdom  34514  ballotlemsel1i  34515  ballotlemsi  34517  ballotlemsima  34518  ballotlem1ri  34537  sgn0bi  34550  signstfvn  34584  signsvtn0  34585  signstfveq0  34592  signsvfn  34597  signsvtn  34599  signshf  34603  hashreprin  34635  circlemeth  34655  logdivsqrle  34665  revpfxsfxrev  35121  revwlk  35130  swrdwlk  35132  subfacp1lem1  35184  subfacp1lem5  35189  cvxpconn  35247  sinccvglem  35677  divcnvlin  35733  bcm1nt  35737  bcprod  35738  bccolsum  35739  iprodgam  35742  faclimlem1  35743  faclimlem2  35744  faclimlem3  35745  faclim  35746  iprodfac  35747  faclim2  35748  fwddifnp1  36166  dnizphlfeqhlf  36477  dnibndlem3  36481  dnibndlem13  36491  unblimceq0  36508  knoppndvlem6  36518  knoppndvlem9  36521  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem16  36528  knoppndvlem17  36529  bj-bary1lem1  37312  irrdiff  37327  poimirlem25  37652  poimirlem26  37653  poimirlem32  37659  opnmbllem0  37663  itg2addnclem2  37679  dvasin  37711  dvacos  37712  areacirclem1  37715  areacirclem4  37718  areacirc  37720  bfp  37831  fzsplitnd  41983  lcmfunnnd  42013  lcmineqlem1  42030  lcmineqlem3  42032  lcmineqlem4  42033  lcmineqlem7  42036  lcmineqlem8  42037  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem12  42041  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem22  42051  lcmineqlem23  42052  dvrelogpow2b  42069  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p3  42079  aks4d1p7d1  42083  primrootsunit1  42098  posbezout  42101  primrootscoprbij  42103  primrootspoweq0  42107  aks6d1c1  42117  hashscontpow1  42122  2np3bcnp1  42145  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones16  42163  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c7lem1  42181  unitscyglem5  42200  metakunt8  42213  metakunt12  42217  metakunt15  42220  metakunt16  42221  metakunt28  42233  nnadd1com  42302  nnaddcom  42303  nnadddir  42305  nnmul1com  42306  nnmulcom  42307  fz1sump1  42344  oddnumth  42345  nicomachus  42346  sumcubes  42347  tan3rdpi  42386  redvmptabs  42390  readvrec  42392  reixi  42452  sn-mullid  42465  sn-0tie0  42469  renegmulnnass  42483  fiabv  42546  fltnltalem  42672  fltnlta  42673  3cubeslem1  42695  3cubeslem2  42696  3cubeslem4  42700  pell1qrge1  42881  rmspecfund  42920  acongeq  42995  jm2.18  43000  jm2.19lem3  43003  jm2.25  43011  jm2.16nn0  43016  jm3.1lem1  43029  jm3.1lem2  43030  areaquad  43228  relexpmulnn  43722  relexpaddss  43731  cvgdvgrat  44332  radcnvrat  44333  hashnzfzclim  44341  ofdivrec  44345  expgrowthi  44352  bccm1k  44361  dvradcnv2  44366  binomcxplemwb  44367  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  refsum2cnlem1  45042  fzisoeu  45312  fperiodmullem  45315  fzdifsuc2  45322  xralrple2  45365  nnsplit  45369  infleinflem2  45382  fmul01lt1lem2  45600  fprodcn  45615  clim1fr1  45616  isumneg  45617  climneg  45625  sumnnodd  45645  reclimc  45668  coseq0  45879  coskpi2  45881  cosknegpi  45884  fprodcncf  45915  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnmul  45958  dvmptfprod  45960  dvnprodlem3  45963  itgsinexp  45970  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem1  46016  stoweidlem7  46022  stoweidlem10  46025  stoweidlem11  46026  stoweidlem14  46029  stoweidlem17  46032  stoweidlem34  46049  stoweidlem42  46057  wallispilem3  46082  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem15  46103  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem11  46133  fourierdlem15  46137  fourierdlem26  46148  fourierdlem36  46158  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem56  46177  fourierdlem58  46179  fourierdlem59  46180  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem78  46199  fourierdlem79  46200  sqwvfoura  46243  fourierswlem  46245  fouriersw  46246  etransclem23  46272  etransclem24  46273  etransclem28  46277  etransclem35  46284  etransclem38  46287  nnfoctbdjlem  46470  smfmullem1  46806  sigaradd  46881  deccarry  47323  m1modne  47350  fargshiftf1  47428  fargshiftfo  47429  fmtnof1  47522  sqrtpwpw2p  47525  fmtnorec2lem  47529  fmtnorec4  47536  fmtnoprmfac1lem  47551  fmtnoprmfac1  47552  fmtnoprmfac2  47554  2pwp1prm  47576  mod42tp1mod8  47589  sfprmdvdsmersenne  47590  lighneallem3  47594  lighneallem4  47597  onego  47633  zofldiv2ALTV  47649  oexpnegALTV  47664  opoeALTV  47670  opeoALTV  47671  epee  47692  perfectALTVlem1  47708  fppr2odd  47718  fpprwppr  47726  gpg3nbgrvtx0  48032  0nodd  48086  2nodd  48088  nnsgrpnmnd  48094  1neven  48154  altgsumbc  48268  pw2m1lepw2m1  48437  m1modmmod  48442  zofldiv2  48452  nnpw2pmod  48504  blen1b  48509  blennn0em1  48512  dignn0flhalflem1  48536  dignn0flhalflem2  48537  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdiglem2  48543  itcovalpclem2  48592  ackval1  48602  ackval2  48603  ackval3  48604  affineid  48625  1subrec1sub  48626  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2vlinest  48662