Theorem 1cnd 8162

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 8092	. 2 |- 1 e. CC
2	1	a1i 9	1 |- ( ph -> 1 e. CC )

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   1c1 8000

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

This theorem is referenced by:  adddirp1d  8173  muladd11r  8302  muls1d  8564  recrecap  8856  rec11ap  8857  rec11rap  8858  rerecclap  8877  subrecap  8986  recp1lt1  9046  nn1m1nn  9128  add1p1  9361  sub1m1  9362  cnm2m1cnm3  9363  xp1d2m1eqxm1d2  9364  div4p1lem1div2  9365  peano2z  9482  zaddcllempos  9483  peano2zm  9484  zaddcllemneg  9485  nn0n0n1ge2  9517  zneo  9548  peano5uzti  9555  lincmb01cmp  10199  iccf1o  10200  nnsplit  10333  zpnn0elfzo1  10414  ubmelm1fzo  10432  fzoshftral  10444  exbtwnzlemstep  10467  rebtwn2zlemstep  10472  qbtwnrelemcalc  10475  flqaddz  10517  2tnp1ge0ge0  10521  ceiqm1l  10533  qnegmod  10591  addmodlteq  10620  uzsinds  10666  seq3shft2  10703  iseqf1olemab  10724  exp3val  10763  binom2sub1  10876  binom3  10879  zesq  10880  sqoddm1div8  10915  nn0opthlem1d  10942  bcm1k  10982  bcp1n  10983  bcp1m1  10987  bcpasc  10988  bcn2m1  10991  omgadd  11024  hashfz  11043  hashfzo  11044  hashfzp1  11046  zfz1isolemsplit  11060  zfz1isolem1  11062  lswccatn0lsw  11146  ccatws1lenp1bg  11168  lswccats1  11174  resqrexlemover  11521  absexpzap  11591  reccn2ap  11824  hashiun  11989  hash2iun1dif1  11991  binomlem  11994  bcxmas  12000  arisum  12009  arisum2  12010  trireciplem  12011  geosergap  12017  pwm1geoserap1  12019  geolim  12022  geolim2  12023  georeclim  12024  geoisum1c  12031  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemsumlt  12039  cvgratz  12043  mertenslemi1  12046  prodf1f  12054  prodfrecap  12057  ntrivcvgap  12059  prodrbdclem  12082  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodntrivap  12095  prod1dc  12097  fprodmul  12102  prodsnf  12103  fprodsplitdc  12107  fprodm1  12109  fprodp1  12111  fprodcl  12118  fprodfac  12126  fprodrec  12140  fprodclf  12146  ef0lem  12171  efsub  12192  tanaddaplem  12249  tanaddap  12250  cos01bnd  12269  zeo3  12379  oddm1even  12386  oddp1even  12387  oexpneg  12388  ltoddhalfle  12404  halfleoddlt  12405  nn0ob  12419  flodddiv4  12447  bitsp1o  12464  bezoutlema  12520  bezoutlemb  12521  uzwodc  12558  qredeu  12619  prmdiv  12757  prmdiveq  12758  pc2dvds  12853  4sqlem11  12924  4sqlem12  12925  oddennn  12963  ennnfonelemp1  12977  gsumfzconst  13878  cncrng  14533  expcn  15243  hoverb  15322  dveflem  15400  dvef  15401  dvply2g  15440  reeff1oleme  15446  sin0pilem1  15455  logdivlti  15555  rpcxpmul2  15587  rplogbval  15619  perfectlem2  15674  lgsvalmod  15698  lgsdir2  15712  lgsdir  15714  gausslemma2dlem1a  15737  gausslemma2dlem5  15745  lgseisenlem4  15752  lgsquadlem1  15756  m1lgs  15764  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3d1  15779  2lgsoddprmlem1  15784  2sqlem8  15802  wlklenvclwlk  16084  cvgcmp2nlemabs  16400  iooref1o  16402  trilpolemeq1  16408  trilpolemlt1  16409  apdifflemr  16415  iswomni0  16419  nconstwlpolemgt0  16432