Theorem 1cnd 10056

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

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   1c1 9937

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

This theorem is referenced by:  adddirp1d  10066  1p1times  10207  addcom  10222  addcomd  10238  muladd11r  10249  pncan1  10454  npcan1  10455  muls1d  10491  mulsubfacd  10492  recrec  10722  rec11  10723  rec11r  10724  rereccl  10743  subrec  10854  nn1m1nn  11040  add1p1  11283  sub1m1  11284  cnm2m1cnm3  11285  xp1d2m1eqxm1d2  11286  div4p1lem1div2  11287  nn0n0n1ge2  11358  zneo  11460  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  lincmb01cmp  12315  iccf1o  12316  xov1plusxeqvd  12318  zpnn0elfzo1  12541  ubmelm1fzo  12564  fzosplitpr  12577  fzosplitprm1  12578  fzoshftral  12585  fladdz  12626  2tnp1ge0ge0  12630  ltdifltdiv  12635  dfceil2  12640  negmod  12715  modnegd  12725  addmodlteq  12745  binom2sub1  12982  binom3  12985  zesq  12987  sqoddm1div8  13028  bcm1k  13102  bcp1n  13103  bcp1m1  13107  bcpasc  13108  bcn2m1  13111  hashfz  13214  hashfzo  13216  hashfzp1  13218  hashf1lem2  13240  hashf1  13241  brfi1indlem  13278  lswccatn0lsw  13373  swrdccatwrd  13468  revccat  13515  repswrevw  13533  cshwidxm1  13553  cshwidxn  13555  cshweqrep  13567  cshimadifsn0  13576  swrd2lsw  13695  relexpaddnn  13791  absexpz  14045  reccn2  14327  rlimno1  14384  isercolllem1  14395  isercoll2  14399  iseraltlem2  14413  iseraltlem3  14414  hashiun  14554  hash2iun1dif1  14556  binomlem  14561  bcxmas  14567  incexc  14569  incexc2  14570  climcndslem1  14581  arisum  14592  arisum2  14593  trireciplem  14594  pwm1geoser  14600  geolim2  14602  georeclim  14603  mertenslem1  14616  prodfrec  14627  ntrivcvg  14629  ntrivcvgtail  14632  prodrblem  14659  prodmolem2a  14664  fprodntriv  14672  prod1  14674  fprodser  14679  fprodcl  14682  fprodm1  14697  fprodp1  14699  risefacval2  14741  fallfacval2  14742  risefacp1  14760  fallfacp1  14761  risefacfac  14766  fallfacfwd  14767  binomfallfaclem2  14771  fallfacval4  14774  bpolydiflem  14785  ef0lem  14809  tanaddlem  14896  tanadd  14897  cos01bnd  14916  oddm1even  15067  oddp1even  15068  oexpneg  15069  ltoddhalfle  15085  halfleoddlt  15086  nn0ob  15100  pwp1fsum  15114  flodddiv4  15137  bitsp1o  15155  bitsf1  15168  sadcp1  15177  qredeu  15372  prmdiv  15490  prmdiveq  15491  vfermltlALT  15507  pcexp  15564  pc2dvds  15583  4sqlem11  15659  4sqlem12  15660  vdwapun  15678  vdwlem3  15687  vdwlem6  15690  vdwlem9  15693  ramub1lem2  15731  prmop1  15742  prmdvdsprmo  15746  prmgaplem8  15762  cshwshashnsame  15810  gsumccat  17378  mulgnnass  17576  mulgnnassOLD  17577  psgnunilem5  17914  psgnunilem2  17915  sylow1lem1  18013  efgredlemc  18158  odadd2  18252  srgbinomlem3  18542  srgbinomlem4  18543  cncrng  19767  cnfldmulg  19778  gzrngunit  19812  zringunit  19836  prmirredlem  19841  cayhamlem1  20671  expcn  22675  iirevcn  22729  iihalf2cn  22733  icchmeo  22740  icopnfcnv  22741  icopnfhmeo  22742  evth  22758  pjthlem1  23208  ovolunlem1a  23264  ovolunlem1  23265  opnmbllem  23369  mbfi1fseqlem6  23487  bddibl  23606  dvnadd  23692  dvmptid  23720  dvmptdiv  23737  dvcnvlem  23739  dveflem  23742  dvsincos  23744  dvlipcn  23757  dvivthlem1  23771  lhop2  23778  dvcvx  23783  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem2  23790  ply1divex  23896  fta1glem1  23925  dgrcolem1  24029  dgrcolem2  24030  aaliou3lem2  24098  aaliou3lem8  24100  dvtaylp  24124  dvntaylp  24125  taylthlem1  24127  taylthlem2  24128  abelthlem1  24185  abelthlem2  24186  abelthlem6  24190  abelthlem7  24192  logdivlti  24366  advlog  24400  advlogexp  24401  logtayl  24406  cxpmul2  24435  dvcxp1  24481  dvcxp2  24482  dvcncxp1  24484  dvcnsqrt  24485  loglesqrt  24499  relogbdiv  24517  ang180lem4  24542  ang180lem5  24543  isosctrlem2  24549  isosctrlem3  24550  affineequiv  24553  affineequiv2  24554  angpieqvdlem  24555  chordthmlem2  24560  chordthmlem3  24561  chordthmlem5  24563  dcubic2  24571  dcubic  24573  quart1lem  24582  quart1  24583  quart  24588  asinlem  24595  asinlem3  24598  atansopn  24659  dvatan  24662  leibpi  24669  birthdaylem2  24679  efrlim  24696  cxplim  24698  divsqrtsumlem  24706  logdifbnd  24720  emcllem2  24723  emcllem3  24724  emcllem5  24726  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  lgam1  24790  gamfac  24793  wilthimp  24798  ftalem5  24803  basellem3  24809  basellem5  24811  basellem8  24814  basellem9  24815  sqff1o  24908  muinv  24919  logfaclbnd  24947  logfacrlim  24949  logexprlim  24950  perfectlem2  24955  dchr1cl  24976  dchrinvcl  24978  dchrfi  24980  dchr1  24982  dchrsum2  24993  bcmono  25002  bcp1ctr  25004  bclbnd  25005  bposlem1  25009  bposlem9  25017  gausslemma2dlem1a  25090  gausslemma2dlem5  25096  lgseisenlem4  25103  lgsquadlem1  25105  m1lgs  25113  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgslem3d1  25128  2lgsoddprmlem1  25133  2sqlem8  25151  chtppilim  25164  rpvmasumlem  25176  dchrisumlem1  25178  dchrisum0re  25202  dchrisum0lem2a  25206  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  2vmadivsumlem  25229  selberg4lem1  25249  pntrsumo1  25254  selberg34r  25260  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntibndlem2  25280  pntlemg  25287  pntlemr  25291  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntlem3  25298  ostth2lem2  25323  ttgcontlem1  25765  cusgrsize2inds  26349  wlklenvclwlk  26551  pthdadjvtx  26626  crctcshwlkn0lem1  26702  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  wlklnwwlkln2lem  26768  wwlksnred  26787  wwlksnextbi  26789  wwlksnredwwlkn  26790  wwlksnextwrd  26792  wwlksnextinj  26794  wwlksnextproplem2  26805  wwlksnextproplem3  26806  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwlkclwwlklem3  26902  clwlkclwwlk  26903  clwwlksel  26914  clwwlksf  26915  clwwlksext2edg  26923  wwlksext2clwwlk  26924  clwwisshclwwslemlem  26926  clwwisshclwws  26928  eucrct2eupth  27105  extwwlkfablem1  27207  numclwwlkovf2exlem1  27211  numclwwlkovf2exlem2  27212  numclwlk1lem2foalem  27222  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  numclwwlk6  27248  smcnlem  27552  bcm1n  29554  ltesubnnd  29568  omndmul2  29712  archirngz  29743  archiabllem1a  29745  archiabllem2c  29749  psgnfzto1stlem  29850  1smat1  29870  madjusmdetlem2  29894  madjusmdetlem4  29896  dya2icoseg  30339  iwrdsplit  30449  fibp1  30463  ballotlemfp1  30553  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemic  30568  ballotlem1c  30569  ballotlemsgt1  30572  ballotlemsdom  30573  ballotlemsel1i  30574  ballotlemsi  30576  ballotlemsima  30577  ballotlem1ri  30596  sgn0bi  30609  signstfvn  30646  signsvtn0  30647  signstfveq0  30654  signsvfn  30659  signsvtn  30661  signshf  30665  hashreprin  30698  circlemeth  30718  logdivsqrle  30728  subfacp1lem1  31161  subfacp1lem5  31166  cvxpconn  31224  sinccvglem  31566  divcnvlin  31618  bcm1nt  31623  bcprod  31624  bccolsum  31625  iprodgam  31628  faclimlem1  31629  faclimlem2  31630  faclimlem3  31631  faclim  31632  iprodfac  31633  faclim2  31634  fwddifnp1  32272  dnizphlfeqhlf  32466  dnibndlem3  32470  dnibndlem13  32480  unblimceq0  32498  knoppndvlem6  32508  knoppndvlem9  32511  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem16  32518  knoppndvlem17  32519  bj-bary1lem1  33161  poimirlem25  33434  poimirlem26  33435  poimirlem32  33441  opnmbllem0  33445  itg2addnclem2  33462  dvasin  33496  dvacos  33497  areacirclem1  33500  areacirclem4  33503  areacirc  33505  bfp  33623  pell1qrge1  37434  rmspecfund  37474  acongeq  37550  jm2.18  37555  jm2.19lem3  37558  jm2.25  37566  jm2.16nn0  37571  jm3.1lem1  37584  jm3.1lem2  37585  itgpowd  37800  areaquad  37802  relexpmulnn  38001  relexpaddss  38010  cvgdvgrat  38512  radcnvrat  38513  hashnzfzclim  38521  ofdivrec  38525  expgrowthi  38532  bccm1k  38541  dvradcnv2  38546  binomcxplemwb  38547  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  refsum2cnlem1  39196  fzisoeu  39514  fperiodmullem  39517  fzdifsuc2  39525  xralrple2  39570  nnsplit  39574  infleinflem2  39587  fmul01lt1lem2  39817  fprodcn  39832  clim1fr1  39833  isumneg  39834  climneg  39842  sumnnodd  39862  reclimc  39885  coseq0  40075  coskpi2  40077  cosknegpi  40080  fprodcncf  40114  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnxpaek  40157  dvnmul  40158  dvmptfprod  40160  dvnprodlem3  40163  itgsinexp  40170  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem1  40218  stoweidlem7  40224  stoweidlem10  40227  stoweidlem11  40228  stoweidlem14  40231  stoweidlem17  40234  stoweidlem34  40251  stoweidlem42  40259  wallispilem3  40284  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem15  40305  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem11  40335  fourierdlem15  40339  fourierdlem26  40350  fourierdlem36  40360  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem56  40379  fourierdlem58  40381  fourierdlem59  40382  fourierdlem62  40385  fourierdlem64  40387  fourierdlem65  40388  fourierdlem78  40401  fourierdlem79  40402  sqwvfoura  40445  fourierswlem  40447  fouriersw  40448  etransclem23  40474  etransclem24  40475  etransclem28  40479  etransclem35  40486  etransclem38  40489  nnfoctbdjlem  40672  smfmullem1  40998  sigaradd  41055  deccarry  41321  fargshiftf1  41377  fargshiftfo  41378  fmtnof1  41447  sqrtpwpw2p  41450  fmtnorec2lem  41454  fmtnorec4  41461  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  fmtnoprmfac2  41479  pwdif  41501  pwm1geoserALT  41502  2pwp1prm  41503  mod42tp1mod8  41519  sfprmdvdsmersenne  41520  lighneallem3  41524  lighneallem4  41527  onego  41559  zofldiv2ALTV  41574  oexpnegALTV  41588  opoeALTV  41594  opeoALTV  41595  epee  41614  perfectALTVlem1  41630  0nodd  41810  2nodd  41812  nnsgrpnmnd  41818  1neven  41932  altgsumbc  42130  pw2m1lepw2m1  42310  m1modmmod  42316  zofldiv2  42325  nnpw2pmod  42377  blen1b  42382  blennn0em1  42385  dignn0flhalflem1  42409  dignn0flhalflem2  42410  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  nn0sumshdiglem2  42416