ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1cnd Unicode version

Theorem 1cnd 7504
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
StepHypRef Expression
1 ax-1cn 7438 . 2  |-  1  e.  CC
21a1i 9 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   CCcc 7348   1c1 7351
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 7438
This theorem is referenced by:  adddirp1d  7514  muladd11r  7638  recrecap  8176  rec11ap  8177  rec11rap  8178  rerecclap  8197  recp1lt1  8360  nn1m1nn  8440  add1p1  8665  sub1m1  8666  cnm2m1cnm3  8667  xp1d2m1eqxm1d2  8668  div4p1lem1div2  8669  peano2z  8786  zaddcllempos  8787  peano2zm  8788  zaddcllemneg  8789  nn0n0n1ge2  8817  zneo  8847  peano5uzti  8854  lincmb01cmp  9420  iccf1o  9421  nnsplit  9548  zpnn0elfzo1  9619  ubmelm1fzo  9637  fzoshftral  9649  exbtwnzlemstep  9659  rebtwn2zlemstep  9664  qbtwnrelemcalc  9667  flqaddz  9704  2tnp1ge0ge0  9708  ceiqm1l  9718  qnegmod  9776  addmodlteq  9805  uzsinds  9848  iseqf1olemab  9918  exp3val  9957  binom2sub1  10068  binom3  10071  zesq  10072  sqoddm1div8  10106  nn0opthlem1d  10128  bcm1k  10168  bcp1n  10169  bcp1m1  10173  bcpasc  10174  bcn2m1  10177  omgadd  10210  hashfz  10229  hashfzo  10230  hashfzp1  10232  zfz1isolemsplit  10243  zfz1isolem1  10245  resqrexlemover  10443  absexpzap  10513  hashiun  10872  hash2iun1dif1  10874  binomlem  10877  bcxmas  10883  arisum  10892  arisum2  10893  trireciplem  10894  geosergap  10900  pwm1geoserap1  10902  geolim  10905  geolim2  10906  georeclim  10907  geoisum1c  10914  cvgratnnlemnexp  10918  cvgratnnlemmn  10919  cvgratnnlemsumlt  10922  cvgratz  10926  mertenslemi1  10929  ef0lem  10950  efsub  10971  tanaddaplem  11029  tanaddap  11030  cos01bnd  11049  zeo3  11146  oddm1even  11153  oddp1even  11154  oexpneg  11155  ltoddhalfle  11171  halfleoddlt  11172  nn0ob  11186  flodddiv4  11212  bezoutlema  11266  bezoutlemb  11267  qredeu  11357  oddennn  11483
  Copyright terms: Public domain W3C validator