Theorem 1cnd 7973

Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 7904	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7809  1c1 7812

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

This theorem is referenced by:  adddirp1d  7984  muladd11r  8113  recrecap  8666  rec11ap  8667  rec11rap  8668  rerecclap  8687  subrecap  8796  recp1lt1  8856  nn1m1nn  8937  add1p1  9168  sub1m1  9169  cnm2m1cnm3  9170  xp1d2m1eqxm1d2  9171  div4p1lem1div2  9172  peano2z  9289  zaddcllempos  9290  peano2zm  9291  zaddcllemneg  9292  nn0n0n1ge2  9323  zneo  9354  peano5uzti  9361  lincmb01cmp  10003  iccf1o  10004  nnsplit  10137  zpnn0elfzo1  10208  ubmelm1fzo  10226  fzoshftral  10238  exbtwnzlemstep  10248  rebtwn2zlemstep  10253  qbtwnrelemcalc  10256  flqaddz  10297  2tnp1ge0ge0  10301  ceiqm1l  10311  qnegmod  10369  addmodlteq  10398  uzsinds  10442  seq3shft2  10473  iseqf1olemab  10489  exp3val  10522  binom2sub1  10635  binom3  10638  zesq  10639  sqoddm1div8  10674  nn0opthlem1d  10700  bcm1k  10740  bcp1n  10741  bcp1m1  10745  bcpasc  10746  bcn2m1  10749  omgadd  10782  hashfz  10801  hashfzo  10802  hashfzp1  10804  zfz1isolemsplit  10818  zfz1isolem1  10820  resqrexlemover  11019  absexpzap  11089  reccn2ap  11321  hashiun  11486  hash2iun1dif1  11488  binomlem  11491  bcxmas  11497  arisum  11506  arisum2  11507  trireciplem  11508  geosergap  11514  pwm1geoserap1  11516  geolim  11519  geolim2  11520  georeclim  11521  geoisum1c  11528  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemsumlt  11536  cvgratz  11540  mertenslemi1  11543  prodf1f  11551  prodfrecap  11554  ntrivcvgap  11556  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prod1dc  11594  fprodmul  11599  prodsnf  11600  fprodsplitdc  11604  fprodm1  11606  fprodp1  11608  fprodcl  11615  fprodfac  11623  fprodrec  11637  fprodclf  11643  ef0lem  11668  efsub  11689  tanaddaplem  11746  tanaddap  11747  cos01bnd  11766  zeo3  11873  oddm1even  11880  oddp1even  11881  oexpneg  11882  ltoddhalfle  11898  halfleoddlt  11899  nn0ob  11913  flodddiv4  11939  bezoutlema  12000  bezoutlemb  12001  uzwodc  12038  qredeu  12097  prmdiv  12235  prmdiveq  12236  pc2dvds  12329  oddennn  12393  ennnfonelemp1  12407  cncrng  13466  dveflem  14190  dvef  14191  reeff1oleme  14196  sin0pilem1  14205  logdivlti  14305  rplogbval  14366  lgsvalmod  14423  lgsdir2  14437  lgsdir  14439  m1lgs  14455  2lgsoddprmlem1  14456  2sqlem8  14473  cvgcmp2nlemabs  14783  iooref1o  14785  trilpolemeq1  14791  trilpolemlt1  14792  apdifflemr  14798  iswomni0  14802  nconstwlpolemgt0  14814