Theorem 1cnd 10636

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  1c1 10538

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

This theorem is referenced by:  adddirp1d  10667  1p1times  10811  addcom  10826  addcomd  10842  muladd11r  10853  pncan1  11064  npcan1  11065  muls1d  11100  mulsubfacd  11101  recrec  11337  rec11  11338  rec11r  11339  rereccl  11358  subrec  11469  nn1m1nn  11659  add1p1  11889  sub1m1  11890  cnm2m1cnm3  11891  xp1d2m1eqxm1d2  11892  div4p1lem1div2  11893  nn0n0n1ge2  11963  zneo  12066  rpnnen1lem5  12381  lincmb01cmp  12882  iccf1o  12883  xov1plusxeqvd  12885  zpnn0elfzo1  13112  ubmelm1fzo  13134  fzosplitpr  13147  fzosplitprm1  13148  fzoshftral  13155  fladdz  13196  2tnp1ge0ge0  13200  ltdifltdiv  13205  dfceil2  13210  negmod  13285  modnegd  13295  addmodlteq  13315  binom2sub1  13583  binom3  13586  zesq  13588  sqoddm1div8  13605  bcm1k  13676  bcp1n  13677  bcp1m1  13681  bcpasc  13682  bcn2m1  13685  hashfz  13789  hashfzo  13791  hashfzp1  13793  hashf1lem2  13815  hashf1  13816  hashdifsnp1  13855  lswccatn0lsw  13945  ccatws1lenp1b  13975  revccat  14128  repswrevw  14149  cshwidxm1  14169  cshwidxn  14171  cshweqrep  14183  cshimadifsn0  14192  swrds2m  14303  swrd2lsw  14314  relexpaddnn  14410  absexpz  14665  reccn2  14953  rlimno1  15010  isercolllem1  15021  isercoll2  15025  iseraltlem2  15039  iseraltlem3  15040  hashiun  15177  hash2iun1dif1  15179  binomlem  15184  bcxmas  15190  incexc  15192  incexc2  15193  climcndslem1  15204  arisum  15215  arisum2  15216  trireciplem  15217  pwdif  15223  pwm1geoser  15224  pwm1geoserOLD  15225  geolim2  15227  georeclim  15228  mertenslem1  15240  prodfrec  15251  ntrivcvg  15253  ntrivcvgtail  15256  prodrblem  15283  prodmolem2a  15288  fprodntriv  15296  prod1  15298  fprodser  15303  fprodcl  15306  fprodm1  15321  fprodp1  15323  fprodclf  15346  risefacval2  15364  fallfacval2  15365  risefacp1  15383  fallfacp1  15384  risefacfac  15389  fallfacfwd  15390  binomfallfaclem2  15394  fallfacval4  15397  bpolydiflem  15408  ef0lem  15432  tanaddlem  15519  tanadd  15520  cos01bnd  15539  oddm1even  15692  oddp1even  15693  oexpneg  15694  ltoddhalfle  15710  halfleoddlt  15711  nn0ob  15735  pwp1fsum  15742  flodddiv4  15764  bitsp1o  15782  bitsf1  15795  sadcp1  15804  qredeu  16002  prmdiv  16122  prmdiveq  16123  vfermltlALT  16139  pc2dvds  16215  4sqlem11  16291  4sqlem12  16292  vdwapun  16310  vdwlem3  16319  vdwlem6  16322  vdwlem9  16325  ramub1lem2  16363  prmop1  16374  prmdvdsprmo  16378  prmgaplem8  16394  cshwshashnsame  16437  gsumsgrpccat  18004  gsumccatOLD  18005  psgnunilem5  18622  psgnunilem2  18623  sylow1lem1  18723  efgredlemc  18871  odadd2  18969  ablsimpgfindlem1  19229  srgbinomlem3  19292  srgbinomlem4  19293  cncrng  20566  gzrngunit  20611  zringunit  20635  prmirredlem  20640  cayhamlem1  21474  expcn  23480  iirevcn  23534  iihalf2cn  23538  icchmeo  23545  icopnfcnv  23546  icopnfhmeo  23547  evth  23563  pcoass  23628  pjthlem1  24040  ovolunlem1a  24097  ovolunlem1  24098  opnmbllem  24202  mbfi1fseqlem6  24321  bddibl  24440  dvnadd  24526  dvmptid  24554  dvmptdiv  24571  dvcnvlem  24573  dveflem  24576  dvef  24577  dvsincos  24578  dvlipcn  24591  dvivthlem1  24605  lhop2  24612  dvcvx  24617  dvfsumle  24618  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem2  24624  ply1divex  24730  fta1glem1  24759  dgrcolem1  24863  dgrcolem2  24864  vieta1lem1  24899  aaliou3lem2  24932  aaliou3lem8  24934  dvtaylp  24958  dvntaylp  24959  taylthlem1  24961  taylthlem2  24962  abelthlem1  25019  abelthlem2  25020  abelthlem6  25024  abelthlem7  25026  logdivlti  25203  advlog  25237  advlogexp  25238  logtayl  25243  cxpmul2  25272  dvcxp1  25321  dvcxp2  25322  dvcncxp1  25324  dvcnsqrt  25325  loglesqrt  25339  relogbdiv  25357  ang180lem4  25390  ang180lem5  25391  isosctrlem2  25397  isosctrlem3  25398  affineequiv  25401  affineequiv2  25402  affineequiv3  25403  angpieqvdlem  25406  chordthmlem2  25411  chordthmlem3  25412  chordthmlem5  25414  dcubic2  25422  dcubic  25424  quart1lem  25433  quart1  25434  quart  25439  asinlem  25446  asinlem3  25449  atansopn  25510  dvatan  25513  leibpi  25520  birthdaylem2  25530  efrlim  25547  cxplim  25549  divsqrtsumlem  25557  logdifbnd  25571  emcllem2  25574  emcllem3  25575  emcllem5  25577  zetacvg  25592  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamgulm2  25613  lgamcvg2  25632  gamcvg  25633  gamcvg2lem  25636  lgam1  25641  gamfac  25644  wilthlem2  25646  wilthimp  25649  ftalem5  25654  basellem3  25660  basellem5  25662  basellem8  25665  basellem9  25666  sqff1o  25759  muinv  25770  logfaclbnd  25798  logfacrlim  25800  logexprlim  25801  perfectlem2  25806  dchr1cl  25827  dchrinvcl  25829  dchrfi  25831  dchr1  25833  dchrsum2  25844  bcmono  25853  bcp1ctr  25855  bclbnd  25856  bposlem9  25868  gausslemma2dlem1a  25941  gausslemma2dlem5  25947  lgseisenlem4  25954  lgsquadlem1  25956  m1lgs  25964  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3d1  25979  2lgsoddprmlem1  25984  2sqlem8  26002  2sq2  26009  addsqn2reu  26017  addsqrexnreu  26018  addsqnreup  26019  addsq2nreurex  26020  chtppilim  26051  rpvmasumlem  26063  dchrisumlem1  26065  dchrisum0re  26089  dchrisum0lem2a  26093  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  2vmadivsumlem  26116  selberg4lem1  26136  pntrsumo1  26141  selberg34r  26147  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntibndlem2  26167  pntlemg  26174  pntlemr  26178  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntlem3  26185  ostth2lem2  26210  ttgcontlem1  26671  cusgrsize2inds  27235  wlklenvclwlk  27436  wlklenvclwlkOLD  27437  pthdadjvtx  27511  crctcshwlkn0lem1  27588  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  wlklnwwlkln2lem  27660  wlknwwlksnbij  27666  wwlksnred  27670  wwlksnext  27671  wwlksnextbi  27672  wwlksnredwwlkn  27673  wwlksnextwrd  27675  wwlksnextinj  27677  wwlksnextproplem2  27689  wwlksnextproplem3  27690  clwwlkccatlem  27767  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlklem3  27779  clwlkclwwlk  27780  clwwisshclwwslemlem  27791  clwwisshclwws  27793  clwwlkel  27825  clwwlkf  27826  clwwlkwwlksb  27833  clwwlkext2edg  27835  wwlksext2clwwlk  27836  clwwlknonex2lem1  27886  clwwlknonex2lem2  27887  eucrct2eupth  28024  numclwwlk1lem2foalem  28130  numclwwlk1lem2fo  28137  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  numclwwlk6  28169  smcnlem  28474  fzm1ne1  30512  bcm1n  30518  fzom1ne1  30524  ltesubnnd  30538  wrdt2ind  30627  omndmul2  30713  psgnfzto1stlem  30742  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  archirngz  30818  archiabllem1a  30820  archiabllem2c  30824  freshmansdream  30859  ccfldextdgrr  31057  1smat1  31069  madjusmdetlem2  31093  madjusmdetlem4  31095  dya2icoseg  31535  iwrdsplit  31645  fibp1  31659  ballotlemfp1  31749  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemic  31764  ballotlem1c  31765  ballotlemsgt1  31768  ballotlemsdom  31769  ballotlemsel1i  31770  ballotlemsi  31772  ballotlemsima  31773  ballotlem1ri  31792  sgn0bi  31805  signstfvn  31839  signsvtn0  31840  signstfveq0  31847  signsvfn  31852  signsvtn  31854  signshf  31858  hashreprin  31891  circlemeth  31911  logdivsqrle  31921  revpfxsfxrev  32362  revwlk  32371  swrdwlk  32373  subfacp1lem1  32426  subfacp1lem5  32431  cvxpconn  32489  sinccvglem  32915  divcnvlin  32964  bcm1nt  32969  bcprod  32970  bccolsum  32971  iprodgam  32974  faclimlem1  32975  faclimlem2  32976  faclimlem3  32977  faclim  32978  iprodfac  32979  faclim2  32980  fwddifnp1  33626  dnizphlfeqhlf  33815  dnibndlem3  33819  dnibndlem13  33829  unblimceq0  33846  knoppndvlem6  33856  knoppndvlem9  33859  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem16  33866  knoppndvlem17  33867  bj-bary1lem1  34595  poimirlem25  34932  poimirlem26  34933  poimirlem32  34939  opnmbllem0  34943  itg2addnclem2  34959  dvasin  34993  dvacos  34994  areacirclem1  34997  areacirclem4  35000  areacirc  35002  bfp  35117  lcmfunnnd  39133  nnadd1com  39209  nnaddcom  39210  nnadddir  39212  nnmul1com  39213  nnmulcom  39214  fltnltalem  39323  fltnlta  39324  3cubeslem1  39330  3cubeslem2  39331  3cubeslem4  39335  pell1qrge1  39516  rmspecfund  39555  acongeq  39629  jm2.18  39634  jm2.19lem3  39637  jm2.25  39645  jm2.16nn0  39650  jm3.1lem1  39663  jm3.1lem2  39664  itgpowd  39870  areaquad  39872  relexpmulnn  40103  relexpaddss  40112  cvgdvgrat  40694  radcnvrat  40695  hashnzfzclim  40703  ofdivrec  40707  expgrowthi  40714  bccm1k  40723  dvradcnv2  40728  binomcxplemwb  40729  binomcxplemnn0  40730  binomcxplemrat  40731  binomcxplemfrat  40732  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  refsum2cnlem1  41343  fzisoeu  41616  fperiodmullem  41619  fzdifsuc2  41626  xralrple2  41671  nnsplit  41675  infleinflem2  41688  fmul01lt1lem2  41915  fprodcn  41930  clim1fr1  41931  isumneg  41932  climneg  41940  sumnnodd  41960  reclimc  41983  coseq0  42194  coskpi2  42196  cosknegpi  42199  fprodcncf  42233  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnxpaek  42276  dvnmul  42277  dvmptfprod  42279  dvnprodlem3  42282  itgsinexp  42289  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  stoweidlem1  42335  stoweidlem7  42341  stoweidlem10  42344  stoweidlem11  42345  stoweidlem14  42348  stoweidlem17  42351  stoweidlem34  42368  stoweidlem42  42376  wallispilem3  42401  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  wallispi2  42407  stirlinglem1  42408  stirlinglem3  42410  stirlinglem4  42411  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem8  42415  stirlinglem10  42417  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  stirlinglem15  42422  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem11  42452  fourierdlem15  42456  fourierdlem26  42467  fourierdlem36  42477  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem56  42496  fourierdlem58  42498  fourierdlem59  42499  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem78  42518  fourierdlem79  42519  sqwvfoura  42562  fourierswlem  42564  fouriersw  42565  etransclem23  42591  etransclem24  42592  etransclem28  42596  etransclem35  42603  etransclem38  42606  nnfoctbdjlem  42786  smfmullem1  43115  sigaradd  43172  deccarry  43560  fargshiftf1  43650  fargshiftfo  43651  fmtnof1  43746  sqrtpwpw2p  43749  fmtnorec2lem  43753  fmtnorec4  43760  fmtnoprmfac1lem  43775  fmtnoprmfac1  43776  fmtnoprmfac2  43778  2pwp1prm  43800  mod42tp1mod8  43816  sfprmdvdsmersenne  43817  lighneallem3  43821  lighneallem4  43824  onego  43860  zofldiv2ALTV  43876  oexpnegALTV  43891  opoeALTV  43897  opeoALTV  43898  epee  43919  perfectALTVlem1  43935  fppr2odd  43945  fpprwppr  43953  0nodd  44126  2nodd  44128  nnsgrpnmnd  44134  1neven  44252  altgsumbc  44449  pw2m1lepw2m1  44624  m1modmmod  44630  zofldiv2  44640  nnpw2pmod  44692  blen1b  44697  blennn0em1  44700  dignn0flhalflem1  44724  dignn0flhalflem2  44725  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  nn0sumshdiglem2  44731  affineid  44740  1subrec1sub  44741  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrx2vlinest  44777