Theorem 1cnd 7970

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

Assertion

Ref	Expression
1cnd	|- ( ph -> 1 e. CC )

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 7901	. 2 |- 1 e. CC
2	1	a1i 9	1 |- ( ph -> 1 e. CC )

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7806   1c1 7809

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

This theorem is referenced by:  adddirp1d  7980  muladd11r  8109  recrecap  8662  rec11ap  8663  rec11rap  8664  rerecclap  8683  subrecap  8792  recp1lt1  8852  nn1m1nn  8933  add1p1  9164  sub1m1  9165  cnm2m1cnm3  9166  xp1d2m1eqxm1d2  9167  div4p1lem1div2  9168  peano2z  9285  zaddcllempos  9286  peano2zm  9287  zaddcllemneg  9288  nn0n0n1ge2  9319  zneo  9350  peano5uzti  9357  lincmb01cmp  9999  iccf1o  10000  nnsplit  10132  zpnn0elfzo1  10203  ubmelm1fzo  10221  fzoshftral  10233  exbtwnzlemstep  10243  rebtwn2zlemstep  10248  qbtwnrelemcalc  10251  flqaddz  10292  2tnp1ge0ge0  10296  ceiqm1l  10306  qnegmod  10364  addmodlteq  10393  uzsinds  10437  seq3shft2  10468  iseqf1olemab  10484  exp3val  10517  binom2sub1  10629  binom3  10632  zesq  10633  sqoddm1div8  10668  nn0opthlem1d  10693  bcm1k  10733  bcp1n  10734  bcp1m1  10738  bcpasc  10739  bcn2m1  10742  omgadd  10775  hashfz  10794  hashfzo  10795  hashfzp1  10797  zfz1isolemsplit  10811  zfz1isolem1  10813  resqrexlemover  11012  absexpzap  11082  reccn2ap  11314  hashiun  11479  hash2iun1dif1  11481  binomlem  11484  bcxmas  11490  arisum  11499  arisum2  11500  trireciplem  11501  geosergap  11507  pwm1geoserap1  11509  geolim  11512  geolim2  11513  georeclim  11514  geoisum1c  11521  cvgratnnlemnexp  11525  cvgratnnlemmn  11526  cvgratnnlemsumlt  11529  cvgratz  11533  mertenslemi1  11536  prodf1f  11544  prodfrecap  11547  ntrivcvgap  11549  prodrbdclem  11572  prodmodclem3  11576  prodmodclem2a  11577  zproddc  11580  fprodseq  11584  fprodntrivap  11585  prod1dc  11587  fprodmul  11592  prodsnf  11593  fprodsplitdc  11597  fprodm1  11599  fprodp1  11601  fprodcl  11608  fprodfac  11616  fprodrec  11630  fprodclf  11636  ef0lem  11661  efsub  11682  tanaddaplem  11739  tanaddap  11740  cos01bnd  11759  zeo3  11865  oddm1even  11872  oddp1even  11873  oexpneg  11874  ltoddhalfle  11890  halfleoddlt  11891  nn0ob  11905  flodddiv4  11931  bezoutlema  11992  bezoutlemb  11993  uzwodc  12030  qredeu  12089  prmdiv  12227  prmdiveq  12228  pc2dvds  12321  oddennn  12385  ennnfonelemp1  12399  cncrng  13332  dveflem  14058  dvef  14059  reeff1oleme  14064  sin0pilem1  14073  logdivlti  14173  rplogbval  14234  lgsvalmod  14291  lgsdir2  14305  lgsdir  14307  2sqlem8  14330  cvgcmp2nlemabs  14640  iooref1o  14642  trilpolemeq1  14648  trilpolemlt1  14649  apdifflemr  14655  iswomni0  14659  nconstwlpolemgt0  14671