Theorem 1cnd 11219

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11115  1c1 11118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1cn 11175

This theorem is used by:  adddirp1d  11252  1p1times  11398  addcom  11413  addcomd  11429  muladd11r  11440  pncan1  11655  npcan1  11656  muls1d  11691  mulsubfacd  11692  recrec  11929  rec11  11930  rec11r  11931  rereccl  11950  subrecd  12061  nn1m1nn  12271  nnadd1com  12276  nnaddcom  12277  nnadddir  12309  nnmul1com  12310  nnmulcom  12311  add1p1  12512  sub1m1  12513  cnm2m1cnm3  12514  xp1d2m1eqxm1d2  12515  div4p1lem1div2  12516  nn0n0n1ge2  12589  zneo  12697  rpnnen1lem5  13023  lincmb01cmp  13540  iccf1o  13541  xov1plusxeqvd  13543  zpnn0elfzo1  13787  ubmelm1fzo  13811  fzosplitpr  13825  fzosplitprm1  13826  fzom1ne1  13833  fzoshftral  13835  fladdz  13878  2tnp1ge0ge0  13882  ltdifltdiv  13887  dfceil2  13892  negmod  13972  modnegd  13982  addmodlteq  14002  binom2sub1  14277  binom3  14280  zesq  14282  sqoddm1div8  14299  bcm1k  14371  bcp1n  14372  bcp1m1  14376  bcpasc  14377  bcn2m1  14380  hashfz  14484  hashfzo  14486  hashfzp1  14488  hashf1lem2  14513  hashf1  14514  hashdifsnp1  14563  lswccatn0lsw  14650  ccatws1lenp1b  14681  revccat  14827  revpfxsfxrev  14829  repswrevw  14850  cshwidxm1  14870  cshwidxn  14872  cshweqrep  14884  cshimadifsn0  14893  swrds2m  15004  swrd2lsw  15015  relexpaddnn  15114  sgn0bi  15166  absexpz  15382  reccn2  15674  rlimno1  15731  isercolllem1  15742  isercoll2  15746  iseraltlem2  15760  iseraltlem3  15761  fsump1  15832  fsumconst1  15867  hashiun  15899  hash2iun1dif1  15901  indsumhash  15906  binomlem  15908  bcxmas  15914  incexc  15916  incexc2  15917  climcndslem1  15928  arisum  15939  arisum2  15940  trireciplem  15941  pwdif  15947  pwm1geoser  15948  geolim2  15950  georeclim  15951  mertenslem1  15963  prodfrec  15974  ntrivcvg  15976  ntrivcvgtail  15979  prodrblem  16008  prodmolem2a  16013  fprodntriv  16021  prod1  16023  fprodser  16028  fprodcl  16031  fprodm1  16046  fprodp1  16048  fprodclf  16071  risefacval2  16089  fallfacval2  16090  risefacp1  16107  fallfacp1  16108  risefacfac  16113  fallfacfwd  16114  binomfallfaclem2  16118  fallfacval4  16121  bpolydiflem  16132  ef0lem  16156  tanaddlem  16246  tanadd  16247  cos01bnd  16266  oddm1even  16425  oddp1even  16426  oexpneg  16427  ltoddhalfle  16443  halfleoddlt  16444  nn0ob  16466  pwp1fsum  16473  flodddiv4  16497  bitsp1o  16515  bitsf1  16528  sadcp1  16537  qredeu  16740  prmdiv  16868  prmdiveq  16869  vfermltlALT  16886  pc2dvds  16963  4sqlem11  17039  4sqlem12  17040  vdwapun  17058  vdwlem3  17067  vdwlem6  17070  vdwlem9  17073  ramub1lem2  17111  prmop1  17122  prmdvdsprmo  17126  prmgaplem8  17142  cshwshashnsame  17187  chnub  18702  chnlt  18703  chnccat  18706  chnrev  18707  gsumsgrpccat  18938  psgnunilem5  19610  psgnunilem2  19611  sylow1lem1  19714  efgredlemc  19861  odadd2  19965  ablsimpgfindlem1  20225  omndmul2  20249  srgbinomlem3  20356  srgbinomlem4  20357  cncrng  21595  gzrngunit  21635  zringunit  21668  prmirredlem  21674  pzriprnglem12  21694  freshmansdream  21776  mhppwdeg  22365  psdmul  22381  cayhamlem1  23075  expcn  25084  iirevcn  25142  iihalf2cn  25146  icchmeo  25153  icopnfcnv  25154  icopnfhmeo  25155  evth  25171  pcoass  25236  pjthlem1  25649  ovolunlem1a  25708  ovolunlem1  25709  opnmbllem  25813  mbfi1fseqlem6  25932  bddibl  26052  dvnadd  26141  dvmptid  26169  dvmptdiv  26186  dvcnvlem  26188  dveflem  26191  dvef  26192  dvsincos  26193  dvlipcn  26206  dvivthlem1  26220  lhop2  26227  dvcvx  26232  dvfsumle  26233  dvfsumabs  26235  dvfsumlem1  26238  dvfsumlem2  26239  itgpowd  26262  ply1divex  26347  fta1glem1  26378  dgrcolem1  26483  dgrcolem2  26484  vieta1lem1  26524  aaliou3lem2  26559  aaliou3lem8  26561  dvtaylp  26586  dvntaylp  26587  taylthlem1  26589  taylthlem2  26590  abelthlem1  26647  abelthlem2  26648  abelthlem6  26652  abelthlem7  26654  logdivlti  26838  advlog  26872  advlogexp  26873  logtayl  26878  cxpmul2  26907  dvcxp1  26958  dvcxp2  26959  dvcncxp1  26961  dvcnsqrt  26962  loglesqrt  26979  relogbdiv  26997  ang180lem4  27030  ang180lem5  27031  isosctrlem2  27037  isosctrlem3  27038  affineequiv  27041  affineequiv2  27042  affineequiv3  27043  angpieqvdlem  27046  chordthmlem2  27051  chordthmlem3  27052  chordthmlem5  27054  dcubic2  27062  dcubic  27064  quart1lem  27073  quart1  27074  quart  27079  asinlem  27086  asinlem3  27089  atansopn  27150  dvatan  27153  leibpi  27160  birthdaylem2  27170  efrlim  27187  cxplim  27189  divsqrtsumlem  27197  logdifbnd  27211  emcllem2  27214  emcllem3  27215  emcllem5  27217  zetacvg  27232  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamgulmlem4  27249  lgamgulmlem5  27250  lgamgulmlem6  27251  lgamgulm2  27253  lgamcvg2  27272  gamcvg  27273  gamcvg2lem  27276  lgam1  27281  gamfac  27284  wilthlem2  27286  wilthimp  27289  ftalem5  27294  basellem3  27300  basellem5  27302  basellem8  27305  basellem9  27306  sqff1o  27399  muinv  27410  logfaclbnd  27439  logfacrlim  27441  logexprlim  27442  perfectlem2  27447  dchr1cl  27468  dchrinvcl  27470  dchrfi  27472  dchr1  27474  dchrsum2  27485  bcmono  27494  bcp1ctr  27496  bclbnd  27497  bposlem9  27509  gausslemma2dlem1a  27582  gausslemma2dlem5  27588  lgseisenlem4  27595  lgsquadlem1  27597  m1lgs  27605  2lgslem3a  27613  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  2lgslem3d1  27620  2lgsoddprmlem1  27625  2sqlem8  27643  2sq2  27650  addsqn2reu  27658  addsqrexnreu  27659  addsqnreup  27660  addsq2nreurex  27661  chtppilim  27692  rpvmasumlem  27704  dchrisumlem1  27706  dchrisum0re  27730  dchrisum0lem2a  27734  mudivsum  27747  mulogsumlem  27748  mulogsum  27749  2vmadivsumlem  27757  selberg4lem1  27777  pntrsumo1  27782  selberg34r  27788  pntrlog2bndlem2  27795  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntrlog2bndlem6  27800  pntibndlem2  27808  pntlemg  27815  pntlemr  27819  pntlemf  27822  pntlemk  27823  pntlemo  27824  pntlem3  27826  ostth2lem2  27851  ttgcontlem1  29291  cusgrsize2inds  29863  wlklenvclwlk  30063  revwlk  30096  swrdwlk  30097  pthdadjvtx  30142  crctcshwlkn0lem1  30228  crctcshwlkn0lem4  30231  crctcshwlkn0lem5  30232  wlklnwwlkln2lem  30300  wlknwwlksnbij  30306  wwlksnred  30310  wwlksnext  30311  wwlksnextbi  30312  wwlksnredwwlkn  30313  wwlksnextwrd  30315  wwlksnextinj  30317  wwlksnextproplem2  30328  wwlksnextproplem3  30329  clwwlkccatlem  30409  clwlkclwwlklem2a1  30412  clwlkclwwlklem2a4  30417  clwlkclwwlklem2a  30418  clwlkclwwlklem2  30420  clwlkclwwlklem3  30421  clwlkclwwlk  30422  clwwisshclwwslemlem  30433  clwwisshclwws  30435  clwwlkel  30466  clwwlkf  30467  clwwlkwwlksb  30474  clwwlkext2edg  30476  wwlksext2clwwlk  30477  clwwlknonex2lem1  30527  clwwlknonex2lem2  30528  eucrct2eupth  30669  numclwwlk1lem2foalem  30775  numclwwlk1lem2fo  30782  numclwlk2lem2f  30801  numclwlk2lem2f1o  30803  numclwwlk6  30814  smcnlem  31122  receqid  33161  fzm1ne1  33205  bcm1n  33212  ltesubnnd  33239  oexpled  33252  wrdt2ind  33341  gsummptp1  33443  gsummulsubdishift1  33454  psgnfzto1stlem  33486  cycpmco2lem3  33514  cycpmco2lem4  33515  cycpmco2lem5  33516  cycpmco2lem6  33517  cycpmco2lem7  33518  cycpmco2  33519  archirngz  33575  archiabllem1a  33577  archiabllem2c  33581  gsumind  33731  esplyind  34031  esplyindfv  34032  esplyfvn  34033  vietadeg1  34034  vietalem  34035  ccfldextdgrr  34128  constrfin  34202  nn0constr  34217  iconstr  34222  constrrecl  34225  constrimcl  34226  constrreinvcl  34228  constrinvcl  34229  constrresqrtcl  34233  2sqr3minply  34236  cos9thpiminplylem1  34238  cos9thpiminplylem2  34239  cos9thpiminplylem3  34240  cos9thpiminply  34244  cos9thpinconstrlem1  34245  1smat1  34260  madjusmdetlem2  34284  madjusmdetlem4  34286  dya2icoseg  34734  iwrdsplit  34844  fibp1  34858  ballotlemfp1  34949  ballotlemfc0  34950  ballotlemfcc  34951  ballotlemic  34964  ballotlem1c  34965  ballotlemsgt1  34968  ballotlemsdom  34969  ballotlemsel1i  34970  ballotlemsi  34972  ballotlemsima  34973  ballotlem1ri  34992  signstfvn  35023  signsvtn0  35024  signstfveq0  35031  signsvfn  35036  signsvtn  35038  signshf  35042  hashreprin  35074  circlemeth  35094  logdivsqrle  35104  subfacp1lem1  35710  subfacp1lem5  35715  cvxpconn  35773  sinccvglem  36203  divcnvlin  36264  bcm1nt  36268  bcprod  36269  bccolsum  36270  iprodgam  36273  faclimlem1  36274  faclimlem2  36275  faclimlem3  36276  faclim  36277  iprodfac  36278  faclim2  36279  fwddifnp1  36696  dnizphlfeqhlf  37124  dnibndlem3  37128  dnibndlem13  37138  unblimceq0  37155  knoppndvlem6  37165  knoppndvlem9  37168  knoppndvlem14  37173  knoppndvlem15  37174  knoppndvlem16  37175  knoppndvlem17  37176  bj-bary1lem1  38014  irrdiff  38029  qdiff  38030  poimirlem25  38355  poimirlem26  38356  poimirlem32  38362  opnmbllem0  38366  itg2addnclem2  38382  dvasin  38414  dvacos  38415  areacirclem1  38418  areacirclem4  38421  areacirc  38423  bfp  38535  fzsplitnd  42809  lcmfunnnd  42839  lcmineqlem1  42856  lcmineqlem3  42858  lcmineqlem4  42859  lcmineqlem7  42862  lcmineqlem8  42863  lcmineqlem10  42865  lcmineqlem11  42866  lcmineqlem12  42867  lcmineqlem18  42873  lcmineqlem19  42874  lcmineqlem22  42877  lcmineqlem23  42878  dvrelogpow2b  42895  aks4d1p1p4  42898  aks4d1p1p6  42900  aks4d1p1p7  42901  aks4d1p1p5  42902  aks4d1p1  42903  aks4d1p3  42905  aks4d1p7d1  42909  primrootsunit1  42924  posbezout  42927  primrootscoprbij  42929  primrootspoweq0  42933  aks6d1c1  42943  hashscontpow1  42948  2np3bcnp1  42971  sticksstones10  42982  sticksstones12a  42984  sticksstones12  42985  sticksstones16  42989  sticksstones22  42995  aks6d1c6lem3  42999  aks6d1c7lem1  43007  unitscyglem5  43026  3rdpwhole  43113  fz1sump1  43131  oddnumth  43132  nicomachus  43133  sumcubes  43134  tan3rdpi  43173  redvmptabs  43181  readvrec  43183  reixi  43244  sn-mullid  43257  sn-0tie0  43285  renegmulnnass  43299  fiabv  43364  fltnltalem  43454  fltnlta  43455  3cubeslem1  43475  3cubeslem2  43476  3cubeslem4  43480  pell1qrge1  43657  rmspecfund  43696  acongeq  43770  jm2.18  43775  jm2.19lem3  43778  jm2.25  43786  jm2.16nn0  43791  jm3.1lem1  43804  jm3.1lem2  43805  areaquad  44003  relexpmulnn  44495  relexpaddss  44504  cvgdvgrat  45083  radcnvrat  45084  hashnzfzclim  45092  ofdivrec  45096  expgrowthi  45103  bccm1k  45112  dvradcnv2  45117  binomcxplemwb  45118  binomcxplemnn0  45119  binomcxplemrat  45120  binomcxplemfrat  45121  binomcxplemdvbinom  45123  binomcxplemnotnn0  45126  refsum2cnlem1  45817  fzisoeu  46079  fperiodmullem  46082  fzdifsuc2  46089  xralrple2  46130  nnsplit  46134  infleinflem2  46146  fmul01lt1lem2  46361  fprodcn  46376  clim1fr1  46377  isumneg  46378  climneg  46386  sumnnodd  46406  reclimc  46427  coseq0  46638  coskpi2  46640  cosknegpi  46643  fprodcncf  46674  fprodsubrecnncnvlem  46681  fprodaddrecnncnvlem  46683  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnxpaek  46716  dvnmul  46717  dvmptfprod  46719  dvnprodlem3  46722  itgsinexp  46729  itgiccshift  46754  itgperiod  46755  itgsbtaddcnst  46756  stoweidlem1  46775  stoweidlem7  46781  stoweidlem10  46784  stoweidlem11  46785  stoweidlem14  46788  stoweidlem17  46791  stoweidlem34  46808  stoweidlem42  46816  wallispilem3  46841  wallispilem5  46843  wallispi  46844  wallispi2lem1  46845  wallispi2lem2  46846  wallispi2  46847  stirlinglem1  46848  stirlinglem3  46850  stirlinglem4  46851  stirlinglem5  46852  stirlinglem6  46853  stirlinglem7  46854  stirlinglem8  46855  stirlinglem10  46857  stirlinglem11  46858  stirlinglem12  46859  stirlinglem13  46860  stirlinglem15  46862  dirkertrigeqlem2  46873  dirkertrigeqlem3  46874  dirkertrigeq  46875  dirkercncflem1  46877  dirkercncflem2  46878  dirkercncflem4  46880  fourierdlem11  46892  fourierdlem15  46896  fourierdlem26  46907  fourierdlem36  46917  fourierdlem40  46921  fourierdlem41  46922  fourierdlem42  46923  fourierdlem48  46928  fourierdlem49  46929  fourierdlem56  46936  fourierdlem58  46938  fourierdlem59  46939  fourierdlem62  46942  fourierdlem64  46944  fourierdlem65  46945  fourierdlem78  46958  fourierdlem79  46959  sqwvfoura  47002  fourierswlem  47004  fouriersw  47005  etransclem23  47031  etransclem24  47032  etransclem28  47036  etransclem35  47043  etransclem38  47046  nnfoctbdjlem  47229  smfmullem1  47565  sigaradd  47640  chnerlem2  47659  sin3t  47668  cos3t  47669  sin5tlem1  47670  sin5tlem2  47671  sin5tlem4  47673  cos5t  47676  cjnpoly  47686  deccarry  48108  ceilbi  48134  flmrecm1  48140  m1modne  48151  m1modmmod  48161  modm1nep2  48171  modm1nem2  48172  fargshiftf1  48250  fargshiftfo  48251  fmtnof1  48347  sqrtpwpw2p  48350  fmtnorec2lem  48354  fmtnorec4  48361  fmtnoprmfac1lem  48376  fmtnoprmfac1  48377  fmtnoprmfac2  48379  2pwp1prm  48401  mod42tp1mod8  48414  sfprmdvdsmersenne  48415  lighneallem3  48419  lighneallem4  48422  ppivalnnprm  48437  ppivalnnnprmge6  48438  onego  48471  zofldiv2ALTV  48487  oexpnegALTV  48502  opoeALTV  48508  opeoALTV  48509  epee  48530  perfectALTVlem1  48546  fppr2odd  48556  fpprwppr  48564  gpg3nbgrvtx0  48901  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  0nodd  48994  2nodd  48996  nnsgrpnmnd  49002  1neven  49062  altgsumbc  49191  pw2m1lepw2m1  49359  zofldiv2  49370  nnpw2pmod  49422  blen1b  49427  blennn0em1  49430  dignn0flhalflem1  49454  dignn0flhalflem2  49455  nn0sumshdiglemB  49459  nn0sumshdiglem1  49460  nn0sumshdiglem2  49461  itcovalpclem2  49510  ackval1  49520  ackval2  49521  ackval3  49522  affineid  49543  1subrec1sub  49544  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  rrx2vlinest  49580