Theorem 1cnd 11175

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℂcc 11071  1c1 11074

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

This theorem is referenced by:  adddirp1d  11208  1p1times  11354  addcom  11369  addcomd  11385  muladd11r  11396  pncan1  11611  npcan1  11612  muls1d  11647  mulsubfacd  11648  recrec  11888  rec11  11889  rec11r  11890  rereccl  11909  subrecd  12020  nn1m1nn  12231  nnadd1com  12236  nnaddcom  12237  nnadddir  12269  nnmul1com  12270  nnmulcom  12271  add1p1  12472  sub1m1  12473  cnm2m1cnm3  12474  xp1d2m1eqxm1d2  12475  div4p1lem1div2  12476  nn0n0n1ge2  12549  zneo  12656  rpnnen1lem5  12982  lincmb01cmp  13499  iccf1o  13500  xov1plusxeqvd  13502  zpnn0elfzo1  13745  ubmelm1fzo  13769  fzosplitpr  13783  fzosplitprm1  13784  fzom1ne1  13791  fzoshftral  13793  fladdz  13835  2tnp1ge0ge0  13839  ltdifltdiv  13844  dfceil2  13849  negmod  13929  modnegd  13939  addmodlteq  13959  binom2sub1  14234  binom3  14237  zesq  14239  sqoddm1div8  14256  bcm1k  14328  bcp1n  14329  bcp1m1  14333  bcpasc  14334  bcn2m1  14337  hashfz  14440  hashfzo  14442  hashfzp1  14444  hashf1lem2  14469  hashf1  14470  hashdifsnp1  14519  lswccatn0lsw  14605  ccatws1lenp1b  14635  revccat  14779  repswrevw  14800  cshwidxm1  14820  cshwidxn  14822  cshweqrep  14834  cshimadifsn0  14843  swrds2m  14954  swrd2lsw  14965  relexpaddnn  15064  sgn0bi  15116  absexpz  15332  reccn2  15624  rlimno1  15681  isercolllem1  15692  isercoll2  15696  iseraltlem2  15710  iseraltlem3  15711  fsump1  15783  fsumconst1  15818  hashiun  15850  hash2iun1dif1  15852  indsumhash  15857  binomlem  15859  bcxmas  15865  incexc  15867  incexc2  15868  climcndslem1  15879  arisum  15890  arisum2  15891  trireciplem  15892  pwdif  15898  pwm1geoser  15899  geolim2  15901  georeclim  15902  mertenslem1  15914  prodfrec  15925  ntrivcvg  15927  ntrivcvgtail  15930  prodrblem  15959  prodmolem2a  15964  fprodntriv  15972  prod1  15974  fprodser  15979  fprodcl  15982  fprodm1  15997  fprodp1  15999  fprodclf  16022  risefacval2  16040  fallfacval2  16041  risefacp1  16059  fallfacp1  16060  risefacfac  16065  fallfacfwd  16066  binomfallfaclem2  16070  fallfacval4  16073  bpolydiflem  16084  ef0lem  16108  tanaddlem  16198  tanadd  16199  cos01bnd  16218  oddm1even  16377  oddp1even  16378  oexpneg  16379  ltoddhalfle  16395  halfleoddlt  16396  nn0ob  16418  pwp1fsum  16425  flodddiv4  16449  bitsp1o  16467  bitsf1  16480  sadcp1  16489  qredeu  16692  prmdiv  16820  prmdiveq  16821  vfermltlALT  16838  pc2dvds  16915  4sqlem11  16991  4sqlem12  16992  vdwapun  17010  vdwlem3  17019  vdwlem6  17022  vdwlem9  17025  ramub1lem2  17063  prmop1  17074  prmdvdsprmo  17078  prmgaplem8  17094  cshwshashnsame  17139  chnub  18654  chnlt  18655  chnccat  18658  chnrev  18659  gsumsgrpccat  18874  psgnunilem5  19534  psgnunilem2  19535  sylow1lem1  19638  efgredlemc  19785  odadd2  19889  ablsimpgfindlem1  20149  omndmul2  20173  srgbinomlem3  20278  srgbinomlem4  20279  cncrng  21445  gzrngunit  21485  zringunit  21518  prmirredlem  21524  pzriprnglem12  21544  freshmansdream  21626  mhppwdeg  22215  psdmul  22231  cayhamlem1  22926  expcn  24934  iirevcn  24992  iihalf2cn  24996  icchmeo  25003  icopnfcnv  25004  icopnfhmeo  25005  evth  25021  pcoass  25086  pjthlem1  25499  ovolunlem1a  25558  ovolunlem1  25559  opnmbllem  25663  mbfi1fseqlem6  25782  bddibl  25902  dvnadd  25991  dvmptid  26019  dvmptdiv  26036  dvcnvlem  26038  dveflem  26041  dvef  26042  dvsincos  26043  dvlipcn  26056  dvivthlem1  26070  lhop2  26077  dvcvx  26082  dvfsumle  26083  dvfsumabs  26085  dvfsumlem1  26088  dvfsumlem2  26089  itgpowd  26112  ply1divex  26197  fta1glem1  26228  dgrcolem1  26333  dgrcolem2  26334  vieta1lem1  26374  aaliou3lem2  26407  aaliou3lem8  26409  dvtaylp  26433  dvntaylp  26434  taylthlem1  26436  taylthlem2  26437  abelthlem1  26494  abelthlem2  26495  abelthlem6  26499  abelthlem7  26501  logdivlti  26685  advlog  26719  advlogexp  26720  logtayl  26725  cxpmul2  26754  dvcxp1  26805  dvcxp2  26806  dvcncxp1  26808  dvcnsqrt  26809  loglesqrt  26826  relogbdiv  26844  ang180lem4  26877  ang180lem5  26878  isosctrlem2  26884  isosctrlem3  26885  affineequiv  26888  affineequiv2  26889  affineequiv3  26890  angpieqvdlem  26893  chordthmlem2  26898  chordthmlem3  26899  chordthmlem5  26901  dcubic2  26909  dcubic  26911  quart1lem  26920  quart1  26921  quart  26926  asinlem  26933  asinlem3  26936  atansopn  26997  dvatan  27000  leibpi  27007  birthdaylem2  27017  efrlim  27034  cxplim  27036  divsqrtsumlem  27044  logdifbnd  27058  emcllem2  27061  emcllem3  27062  emcllem5  27064  zetacvg  27079  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem4  27096  lgamgulmlem5  27097  lgamgulmlem6  27098  lgamgulm2  27100  lgamcvg2  27119  gamcvg  27120  gamcvg2lem  27123  lgam1  27128  gamfac  27131  wilthlem2  27133  wilthimp  27136  ftalem5  27141  basellem3  27147  basellem5  27149  basellem8  27152  basellem9  27153  sqff1o  27246  muinv  27257  logfaclbnd  27286  logfacrlim  27288  logexprlim  27289  perfectlem2  27294  dchr1cl  27315  dchrinvcl  27317  dchrfi  27319  dchr1  27321  dchrsum2  27332  bcmono  27341  bcp1ctr  27343  bclbnd  27344  bposlem9  27356  gausslemma2dlem1a  27429  gausslemma2dlem5  27435  lgseisenlem4  27442  lgsquadlem1  27444  m1lgs  27452  2lgslem3a  27460  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  2lgslem3d1  27467  2lgsoddprmlem1  27472  2sqlem8  27490  2sq2  27497  addsqn2reu  27505  addsqrexnreu  27506  addsqnreup  27507  addsq2nreurex  27508  chtppilim  27539  rpvmasumlem  27551  dchrisumlem1  27553  dchrisum0re  27577  dchrisum0lem2a  27581  mudivsum  27594  mulogsumlem  27595  mulogsum  27596  2vmadivsumlem  27604  selberg4lem1  27624  pntrsumo1  27629  selberg34r  27635  pntrlog2bndlem2  27642  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntrlog2bndlem6  27647  pntibndlem2  27655  pntlemg  27662  pntlemr  27666  pntlemf  27669  pntlemk  27670  pntlemo  27671  pntlem3  27673  ostth2lem2  27698  ttgcontlem1  29085  cusgrsize2inds  29654  wlklenvclwlk  29854  pthdadjvtx  29928  crctcshwlkn0lem1  30010  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  wlklnwwlkln2lem  30082  wlknwwlksnbij  30088  wwlksnred  30092  wwlksnext  30093  wwlksnextbi  30094  wwlksnredwwlkn  30095  wwlksnextwrd  30097  wwlksnextinj  30099  wwlksnextproplem2  30110  wwlksnextproplem3  30111  clwwlkccatlem  30191  clwlkclwwlklem2a1  30194  clwlkclwwlklem2a4  30199  clwlkclwwlklem2a  30200  clwlkclwwlklem2  30202  clwlkclwwlklem3  30203  clwlkclwwlk  30204  clwwisshclwwslemlem  30215  clwwisshclwws  30217  clwwlkel  30248  clwwlkf  30249  clwwlkwwlksb  30256  clwwlkext2edg  30258  wwlksext2clwwlk  30259  clwwlknonex2lem1  30309  clwwlknonex2lem2  30310  eucrct2eupth  30447  numclwwlk1lem2foalem  30553  numclwwlk1lem2fo  30560  numclwlk2lem2f  30579  numclwlk2lem2f1o  30581  numclwwlk6  30592  smcnlem  30900  receqid  32946  fzm1ne1  32990  bcm1n  32997  ltesubnnd  33025  oexpled  33038  wrdt2ind  33131  gsummptp1  33237  gsummulsubdishift1  33248  psgnfzto1stlem  33280  cycpmco2lem3  33308  cycpmco2lem4  33309  cycpmco2lem5  33310  cycpmco2lem6  33311  cycpmco2lem7  33312  cycpmco2  33313  archirngz  33369  archiabllem1a  33371  archiabllem2c  33375  gsumind  33531  esplyind  33872  esplyindfv  33873  esplyfvn  33874  vietadeg1  33875  vietalem  33876  ccfldextdgrr  33969  constrfin  34043  nn0constr  34058  iconstr  34063  constrrecl  34066  constrimcl  34067  constrreinvcl  34069  constrinvcl  34070  constrresqrtcl  34074  2sqr3minply  34077  cos9thpiminplylem1  34079  cos9thpiminplylem2  34080  cos9thpiminplylem3  34081  cos9thpiminply  34085  cos9thpinconstrlem1  34086  1smat1  34101  madjusmdetlem2  34125  madjusmdetlem4  34127  dya2icoseg  34574  iwrdsplit  34684  fibp1  34698  ballotlemfp1  34789  ballotlemfc0  34790  ballotlemfcc  34791  ballotlemic  34804  ballotlem1c  34805  ballotlemsgt1  34808  ballotlemsdom  34809  ballotlemsel1i  34810  ballotlemsi  34812  ballotlemsima  34813  ballotlem1ri  34832  signstfvn  34863  signsvtn0  34864  signstfveq0  34871  signsvfn  34876  signsvtn  34878  signshf  34882  hashreprin  34914  circlemeth  34934  logdivsqrle  34944  revpfxsfxrev  35466  revwlk  35475  swrdwlk  35477  subfacp1lem1  35529  subfacp1lem5  35534  cvxpconn  35592  sinccvglem  36022  divcnvlin  36083  bcm1nt  36087  bcprod  36088  bccolsum  36089  iprodgam  36092  faclimlem1  36093  faclimlem2  36094  faclimlem3  36095  faclim  36096  iprodfac  36097  faclim2  36098  fwddifnp1  36515  dnizphlfeqhlf  36914  dnibndlem3  36918  dnibndlem13  36928  unblimceq0  36945  knoppndvlem6  36955  knoppndvlem9  36958  knoppndvlem14  36963  knoppndvlem15  36964  knoppndvlem16  36965  knoppndvlem17  36966  bj-bary1lem1  37803  irrdiff  37818  qdiff  37819  poimirlem25  38144  poimirlem26  38145  poimirlem32  38151  opnmbllem0  38155  itg2addnclem2  38171  dvasin  38203  dvacos  38204  areacirclem1  38207  areacirclem4  38210  areacirc  38212  bfp  38323  fzsplitnd  42599  lcmfunnnd  42629  lcmineqlem1  42646  lcmineqlem3  42648  lcmineqlem4  42649  lcmineqlem7  42652  lcmineqlem8  42653  lcmineqlem10  42655  lcmineqlem11  42656  lcmineqlem12  42657  lcmineqlem18  42663  lcmineqlem19  42664  lcmineqlem22  42667  lcmineqlem23  42668  dvrelogpow2b  42685  aks4d1p1p4  42688  aks4d1p1p6  42690  aks4d1p1p7  42691  aks4d1p1p5  42692  aks4d1p1  42693  aks4d1p3  42695  aks4d1p7d1  42699  primrootsunit1  42714  posbezout  42717  primrootscoprbij  42719  primrootspoweq0  42723  aks6d1c1  42733  hashscontpow1  42738  2np3bcnp1  42761  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  sticksstones16  42779  sticksstones22  42785  aks6d1c6lem3  42789  aks6d1c7lem1  42797  unitscyglem5  42816  3rdpwhole  42901  fz1sump1  42919  oddnumth  42920  nicomachus  42921  sumcubes  42922  tan3rdpi  42961  redvmptabs  42969  readvrec  42971  reixi  43032  sn-mullid  43045  sn-0tie0  43073  renegmulnnass  43087  fiabv  43154  fltnltalem  43244  fltnlta  43245  3cubeslem1  43265  3cubeslem2  43266  3cubeslem4  43270  pell1qrge1  43447  rmspecfund  43486  acongeq  43560  jm2.18  43565  jm2.19lem3  43568  jm2.25  43576  jm2.16nn0  43581  jm3.1lem1  43594  jm3.1lem2  43595  areaquad  43793  relexpmulnn  44285  relexpaddss  44294  cvgdvgrat  44889  radcnvrat  44890  hashnzfzclim  44898  ofdivrec  44902  expgrowthi  44909  bccm1k  44918  dvradcnv2  44923  binomcxplemwb  44924  binomcxplemnn0  44925  binomcxplemrat  44926  binomcxplemfrat  44927  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  refsum2cnlem1  45617  fzisoeu  45879  fperiodmullem  45882  fzdifsuc2  45889  xralrple2  45930  nnsplit  45934  infleinflem2  45946  fmul01lt1lem2  46161  fprodcn  46176  clim1fr1  46177  isumneg  46178  climneg  46186  sumnnodd  46206  reclimc  46227  coseq0  46438  coskpi2  46440  cosknegpi  46443  fprodcncf  46474  fprodsubrecnncnvlem  46481  fprodaddrecnncnvlem  46483  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnxpaek  46516  dvnmul  46517  dvmptfprod  46519  dvnprodlem3  46522  itgsinexp  46529  itgiccshift  46554  itgperiod  46555  itgsbtaddcnst  46556  stoweidlem1  46575  stoweidlem7  46581  stoweidlem10  46584  stoweidlem11  46585  stoweidlem14  46588  stoweidlem17  46591  stoweidlem34  46608  stoweidlem42  46616  wallispilem3  46641  wallispilem5  46643  wallispi  46644  wallispi2lem1  46645  wallispi2lem2  46646  wallispi2  46647  stirlinglem1  46648  stirlinglem3  46650  stirlinglem4  46651  stirlinglem5  46652  stirlinglem6  46653  stirlinglem7  46654  stirlinglem8  46655  stirlinglem10  46657  stirlinglem11  46658  stirlinglem12  46659  stirlinglem13  46660  stirlinglem15  46662  dirkertrigeqlem2  46673  dirkertrigeqlem3  46674  dirkertrigeq  46675  dirkercncflem1  46677  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem11  46692  fourierdlem15  46696  fourierdlem26  46707  fourierdlem36  46717  fourierdlem40  46721  fourierdlem41  46722  fourierdlem42  46723  fourierdlem48  46728  fourierdlem49  46729  fourierdlem56  46736  fourierdlem58  46738  fourierdlem59  46739  fourierdlem62  46742  fourierdlem64  46744  fourierdlem65  46745  fourierdlem78  46758  fourierdlem79  46759  sqwvfoura  46802  fourierswlem  46804  fouriersw  46805  etransclem23  46831  etransclem24  46832  etransclem28  46836  etransclem35  46843  etransclem38  46846  nnfoctbdjlem  47029  smfmullem1  47365  sigaradd  47440  chnerlem2  47459  sin3t  47465  cos3t  47466  sin5tlem1  47467  sin5tlem2  47468  sin5tlem4  47470  cos5t  47473  cjnpoly  47483  deccarry  47905  ceilbi  47931  flmrecm1  47937  m1modne  47948  m1modmmod  47958  modm1nep2  47968  modm1nem2  47969  fargshiftf1  48047  fargshiftfo  48048  fmtnof1  48144  sqrtpwpw2p  48147  fmtnorec2lem  48151  fmtnorec4  48158  fmtnoprmfac1lem  48173  fmtnoprmfac1  48174  fmtnoprmfac2  48176  2pwp1prm  48198  mod42tp1mod8  48211  sfprmdvdsmersenne  48212  lighneallem3  48216  lighneallem4  48219  ppivalnnprm  48234  ppivalnnnprmge6  48235  onego  48268  zofldiv2ALTV  48284  oexpnegALTV  48299  opoeALTV  48305  opeoALTV  48306  epee  48327  perfectALTVlem1  48343  fppr2odd  48353  fpprwppr  48361  gpg3nbgrvtx0  48698  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  0nodd  48792  2nodd  48794  nnsgrpnmnd  48800  1neven  48860  altgsumbc  48974  pw2m1lepw2m1  49142  zofldiv2  49153  nnpw2pmod  49205  blen1b  49210  blennn0em1  49213  dignn0flhalflem1  49237  dignn0flhalflem2  49238  nn0sumshdiglemB  49242  nn0sumshdiglem1  49243  nn0sumshdiglem2  49244  itcovalpclem2  49293  ackval1  49303  ackval2  49304  ackval3  49305  affineid  49326  1subrec1sub  49327  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2vlinest  49363