Theorem 1cnd 11206

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11105  1c1 11108

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

This theorem is referenced by:  adddirp1d  11237  1p1times  11382  addcom  11397  addcomd  11413  muladd11r  11424  pncan1  11635  npcan1  11636  muls1d  11671  mulsubfacd  11672  recrec  11908  rec11  11909  rec11r  11910  rereccl  11929  subrec  12040  nn1m1nn  12230  add1p1  12460  sub1m1  12461  cnm2m1cnm3  12462  xp1d2m1eqxm1d2  12463  div4p1lem1div2  12464  nn0n0n1ge2  12536  zneo  12642  rpnnen1lem5  12962  lincmb01cmp  13469  iccf1o  13470  xov1plusxeqvd  13472  zpnn0elfzo1  13703  ubmelm1fzo  13725  fzosplitpr  13738  fzosplitprm1  13739  fzoshftral  13746  fladdz  13787  2tnp1ge0ge0  13791  ltdifltdiv  13796  dfceil2  13801  negmod  13878  modnegd  13888  addmodlteq  13908  binom2sub1  14181  binom3  14184  zesq  14186  sqoddm1div8  14203  bcm1k  14272  bcp1n  14273  bcp1m1  14277  bcpasc  14278  bcn2m1  14281  hashfz  14384  hashfzo  14386  hashfzp1  14388  hashf1lem2  14414  hashf1  14415  hashdifsnp1  14454  lswccatn0lsw  14538  ccatws1lenp1b  14568  revccat  14713  repswrevw  14734  cshwidxm1  14754  cshwidxn  14756  cshweqrep  14768  cshimadifsn0  14778  swrds2m  14889  swrd2lsw  14900  relexpaddnn  14995  absexpz  15249  reccn2  15538  rlimno1  15597  isercolllem1  15608  isercoll2  15612  iseraltlem2  15626  iseraltlem3  15627  fsump1  15699  hashiun  15765  hash2iun1dif1  15767  binomlem  15772  bcxmas  15778  incexc  15780  incexc2  15781  climcndslem1  15792  arisum  15803  arisum2  15804  trireciplem  15805  pwdif  15811  pwm1geoser  15812  geolim2  15814  georeclim  15815  mertenslem1  15827  prodfrec  15838  ntrivcvg  15840  ntrivcvgtail  15843  prodrblem  15870  prodmolem2a  15875  fprodntriv  15883  prod1  15885  fprodser  15890  fprodcl  15893  fprodm1  15908  fprodp1  15910  fprodclf  15933  risefacval2  15951  fallfacval2  15952  risefacp1  15970  fallfacp1  15971  risefacfac  15976  fallfacfwd  15977  binomfallfaclem2  15981  fallfacval4  15984  bpolydiflem  15995  ef0lem  16019  tanaddlem  16106  tanadd  16107  cos01bnd  16126  oddm1even  16283  oddp1even  16284  oexpneg  16285  ltoddhalfle  16301  halfleoddlt  16302  nn0ob  16324  pwp1fsum  16331  flodddiv4  16353  bitsp1o  16371  bitsf1  16384  sadcp1  16393  qredeu  16592  prmdiv  16715  prmdiveq  16716  vfermltlALT  16732  pc2dvds  16809  4sqlem11  16885  4sqlem12  16886  vdwapun  16904  vdwlem3  16913  vdwlem6  16916  vdwlem9  16919  ramub1lem2  16957  prmop1  16968  prmdvdsprmo  16972  prmgaplem8  16988  cshwshashnsame  17034  gsumsgrpccat  18718  psgnunilem5  19357  psgnunilem2  19358  sylow1lem1  19461  efgredlemc  19608  odadd2  19712  ablsimpgfindlem1  19972  srgbinomlem3  20045  srgbinomlem4  20046  cncrng  20959  gzrngunit  21004  zringunit  21028  prmirredlem  21034  mhppwdeg  21685  cayhamlem1  22360  expcn  24380  iirevcn  24438  iihalf2cn  24442  icchmeo  24449  icopnfcnv  24450  icopnfhmeo  24451  evth  24467  pcoass  24532  pjthlem1  24946  ovolunlem1a  25005  ovolunlem1  25006  opnmbllem  25110  mbfi1fseqlem6  25230  bddibl  25349  dvnadd  25438  dvmptid  25466  dvmptdiv  25483  dvcnvlem  25485  dveflem  25488  dvef  25489  dvsincos  25490  dvlipcn  25503  dvivthlem1  25517  lhop2  25524  dvcvx  25529  dvfsumle  25530  dvfsumabs  25532  dvfsumlem1  25535  dvfsumlem2  25536  itgpowd  25559  ply1divex  25646  fta1glem1  25675  dgrcolem1  25779  dgrcolem2  25780  vieta1lem1  25815  aaliou3lem2  25848  aaliou3lem8  25850  dvtaylp  25874  dvntaylp  25875  taylthlem1  25877  taylthlem2  25878  abelthlem1  25935  abelthlem2  25936  abelthlem6  25940  abelthlem7  25942  logdivlti  26120  advlog  26154  advlogexp  26155  logtayl  26160  cxpmul2  26189  dvcxp1  26238  dvcxp2  26239  dvcncxp1  26241  dvcnsqrt  26242  loglesqrt  26256  relogbdiv  26274  ang180lem4  26307  ang180lem5  26308  isosctrlem2  26314  isosctrlem3  26315  affineequiv  26318  affineequiv2  26319  affineequiv3  26320  angpieqvdlem  26323  chordthmlem2  26328  chordthmlem3  26329  chordthmlem5  26331  dcubic2  26339  dcubic  26341  quart1lem  26350  quart1  26351  quart  26356  asinlem  26363  asinlem3  26366  atansopn  26427  dvatan  26430  leibpi  26437  birthdaylem2  26447  efrlim  26464  cxplim  26466  divsqrtsumlem  26474  logdifbnd  26488  emcllem2  26491  emcllem3  26492  emcllem5  26494  zetacvg  26509  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamgulm2  26530  lgamcvg2  26549  gamcvg  26550  gamcvg2lem  26553  lgam1  26558  gamfac  26561  wilthlem2  26563  wilthimp  26566  ftalem5  26571  basellem3  26577  basellem5  26579  basellem8  26582  basellem9  26583  sqff1o  26676  muinv  26687  logfaclbnd  26715  logfacrlim  26717  logexprlim  26718  perfectlem2  26723  dchr1cl  26744  dchrinvcl  26746  dchrfi  26748  dchr1  26750  dchrsum2  26761  bcmono  26770  bcp1ctr  26772  bclbnd  26773  bposlem9  26785  gausslemma2dlem1a  26858  gausslemma2dlem5  26864  lgseisenlem4  26871  lgsquadlem1  26873  m1lgs  26881  2lgslem3a  26889  2lgslem3b  26890  2lgslem3c  26891  2lgslem3d  26892  2lgslem3d1  26896  2lgsoddprmlem1  26901  2sqlem8  26919  2sq2  26926  addsqn2reu  26934  addsqrexnreu  26935  addsqnreup  26936  addsq2nreurex  26937  chtppilim  26968  rpvmasumlem  26980  dchrisumlem1  26982  dchrisum0re  27006  dchrisum0lem2a  27010  mudivsum  27023  mulogsumlem  27024  mulogsum  27025  2vmadivsumlem  27033  selberg4lem1  27053  pntrsumo1  27058  selberg34r  27064  pntrlog2bndlem2  27071  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntibndlem2  27084  pntlemg  27091  pntlemr  27095  pntlemf  27098  pntlemk  27099  pntlemo  27100  pntlem3  27102  ostth2lem2  27127  ttgcontlem1  28132  cusgrsize2inds  28700  wlklenvclwlk  28902  pthdadjvtx  28977  crctcshwlkn0lem1  29054  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  wlklnwwlkln2lem  29126  wlknwwlksnbij  29132  wwlksnred  29136  wwlksnext  29137  wwlksnextbi  29138  wwlksnredwwlkn  29139  wwlksnextwrd  29141  wwlksnextinj  29143  wwlksnextproplem2  29154  wwlksnextproplem3  29155  clwwlkccatlem  29232  clwlkclwwlklem2a1  29235  clwlkclwwlklem2a4  29240  clwlkclwwlklem2a  29241  clwlkclwwlklem2  29243  clwlkclwwlklem3  29244  clwlkclwwlk  29245  clwwisshclwwslemlem  29256  clwwisshclwws  29258  clwwlkel  29289  clwwlkf  29290  clwwlkwwlksb  29297  clwwlkext2edg  29299  wwlksext2clwwlk  29300  clwwlknonex2lem1  29350  clwwlknonex2lem2  29351  eucrct2eupth  29488  numclwwlk1lem2foalem  29594  numclwwlk1lem2fo  29601  numclwlk2lem2f  29620  numclwlk2lem2f1o  29622  numclwwlk6  29633  smcnlem  29938  fzm1ne1  31988  bcm1n  31994  fzom1ne1  32000  ltesubnnd  32016  wrdt2ind  32105  omndmul2  32218  psgnfzto1stlem  32247  cycpmco2lem3  32275  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2lem7  32279  cycpmco2  32280  archirngz  32323  archiabllem1a  32325  archiabllem2c  32329  freshmansdream  32370  ccfldextdgrr  32735  1smat1  32773  madjusmdetlem2  32797  madjusmdetlem4  32799  dya2icoseg  33265  iwrdsplit  33375  fibp1  33389  ballotlemfp1  33479  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemic  33494  ballotlem1c  33495  ballotlemsgt1  33498  ballotlemsdom  33499  ballotlemsel1i  33500  ballotlemsi  33502  ballotlemsima  33503  ballotlem1ri  33522  sgn0bi  33535  signstfvn  33569  signsvtn0  33570  signstfveq0  33577  signsvfn  33582  signsvtn  33584  signshf  33588  hashreprin  33621  circlemeth  33641  logdivsqrle  33651  revpfxsfxrev  34095  revwlk  34104  swrdwlk  34106  subfacp1lem1  34159  subfacp1lem5  34164  cvxpconn  34222  sinccvglem  34646  divcnvlin  34691  bcm1nt  34696  bcprod  34697  bccolsum  34698  iprodgam  34701  faclimlem1  34702  faclimlem2  34703  faclimlem3  34704  faclim  34705  iprodfac  34706  faclim2  34707  fwddifnp1  35126  gg-expcn  35153  gg-iihalf2cn  35157  gg-icchmeo  35159  gg-dvfsumle  35171  gg-dvfsumlem2  35172  dnizphlfeqhlf  35341  dnibndlem3  35345  dnibndlem13  35355  unblimceq0  35372  knoppndvlem6  35382  knoppndvlem9  35385  knoppndvlem14  35390  knoppndvlem15  35391  knoppndvlem16  35392  knoppndvlem17  35393  bj-bary1lem1  36181  irrdiff  36196  poimirlem25  36502  poimirlem26  36503  poimirlem32  36509  opnmbllem0  36513  itg2addnclem2  36529  dvasin  36561  dvacos  36562  areacirclem1  36565  areacirclem4  36568  areacirc  36570  bfp  36681  fzsplitnd  40837  lcmfunnnd  40866  lcmineqlem1  40883  lcmineqlem3  40885  lcmineqlem4  40886  lcmineqlem7  40889  lcmineqlem8  40890  lcmineqlem10  40892  lcmineqlem11  40893  lcmineqlem12  40894  lcmineqlem18  40900  lcmineqlem19  40901  lcmineqlem22  40904  lcmineqlem23  40905  dvrelogpow2b  40922  aks4d1p1p4  40925  aks4d1p1p6  40927  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p3  40932  aks4d1p7d1  40936  2np3bcnp1  40949  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones16  40967  sticksstones22  40973  metakunt8  40981  metakunt12  40985  metakunt15  40988  metakunt16  40989  metakunt28  41001  nnadd1com  41179  nnaddcom  41180  nnadddir  41182  nnmul1com  41183  nnmulcom  41184  fz1sump1  41204  oddnumth  41205  nicomachus  41206  sumcubes  41207  reixi  41292  sn-mullid  41305  sn-0tie0  41309  renegmulnnass  41323  fltnltalem  41401  fltnlta  41402  3cubeslem1  41408  3cubeslem2  41409  3cubeslem4  41413  pell1qrge1  41594  rmspecfund  41633  acongeq  41708  jm2.18  41713  jm2.19lem3  41716  jm2.25  41724  jm2.16nn0  41729  jm3.1lem1  41742  jm3.1lem2  41743  areaquad  41951  relexpmulnn  42446  relexpaddss  42455  cvgdvgrat  43058  radcnvrat  43059  hashnzfzclim  43067  ofdivrec  43071  expgrowthi  43078  bccm1k  43087  dvradcnv2  43092  binomcxplemwb  43093  binomcxplemnn0  43094  binomcxplemrat  43095  binomcxplemfrat  43096  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  refsum2cnlem1  43707  fzisoeu  43997  fperiodmullem  44000  fzdifsuc2  44007  xralrple2  44051  nnsplit  44055  infleinflem2  44068  fmul01lt1lem2  44288  fprodcn  44303  clim1fr1  44304  isumneg  44305  climneg  44313  sumnnodd  44333  reclimc  44356  coseq0  44567  coskpi2  44569  cosknegpi  44572  fprodcncf  44603  fprodsubrecnncnvlem  44610  fprodaddrecnncnvlem  44612  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnxpaek  44645  dvnmul  44646  dvmptfprod  44648  dvnprodlem3  44651  itgsinexp  44658  itgiccshift  44683  itgperiod  44684  itgsbtaddcnst  44685  stoweidlem1  44704  stoweidlem7  44710  stoweidlem10  44713  stoweidlem11  44714  stoweidlem14  44717  stoweidlem17  44720  stoweidlem34  44737  stoweidlem42  44745  wallispilem3  44770  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  wallispi2  44776  stirlinglem1  44777  stirlinglem3  44779  stirlinglem4  44780  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem8  44784  stirlinglem10  44786  stirlinglem11  44787  stirlinglem12  44788  stirlinglem13  44789  stirlinglem15  44791  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  dirkertrigeq  44804  dirkercncflem1  44806  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem11  44821  fourierdlem15  44825  fourierdlem26  44836  fourierdlem36  44846  fourierdlem40  44850  fourierdlem41  44851  fourierdlem42  44852  fourierdlem48  44857  fourierdlem49  44858  fourierdlem56  44865  fourierdlem58  44867  fourierdlem59  44868  fourierdlem62  44871  fourierdlem64  44873  fourierdlem65  44874  fourierdlem78  44887  fourierdlem79  44888  sqwvfoura  44931  fourierswlem  44933  fouriersw  44934  etransclem23  44960  etransclem24  44961  etransclem28  44965  etransclem35  44972  etransclem38  44975  nnfoctbdjlem  45158  smfmullem1  45494  sigaradd  45569  deccarry  46006  fargshiftf1  46096  fargshiftfo  46097  fmtnof1  46190  sqrtpwpw2p  46193  fmtnorec2lem  46197  fmtnorec4  46204  fmtnoprmfac1lem  46219  fmtnoprmfac1  46220  fmtnoprmfac2  46222  2pwp1prm  46244  mod42tp1mod8  46257  sfprmdvdsmersenne  46258  lighneallem3  46262  lighneallem4  46265  onego  46301  zofldiv2ALTV  46317  oexpnegALTV  46332  opoeALTV  46338  opeoALTV  46339  epee  46360  perfectALTVlem1  46376  fppr2odd  46386  fpprwppr  46394  0nodd  46567  2nodd  46569  nnsgrpnmnd  46575  1neven  46784  altgsumbc  46982  pw2m1lepw2m1  47155  m1modmmod  47161  zofldiv2  47171  nnpw2pmod  47223  blen1b  47228  blennn0em1  47231  dignn0flhalflem1  47255  dignn0flhalflem2  47256  nn0sumshdiglemB  47260  nn0sumshdiglem1  47261  nn0sumshdiglem2  47262  itcovalpclem2  47311  ackval1  47321  ackval2  47322  ackval3  47323  affineid  47344  1subrec1sub  47345  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  rrx2vlinest  47381