Theorem 1cnd 8087

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 8017	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2175  ℂcc 7922  1c1 7925

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

This theorem is referenced by:  adddirp1d  8098  muladd11r  8227  muls1d  8489  recrecap  8781  rec11ap  8782  rec11rap  8783  rerecclap  8802  subrecap  8911  recp1lt1  8971  nn1m1nn  9053  add1p1  9286  sub1m1  9287  cnm2m1cnm3  9288  xp1d2m1eqxm1d2  9289  div4p1lem1div2  9290  peano2z  9407  zaddcllempos  9408  peano2zm  9409  zaddcllemneg  9410  nn0n0n1ge2  9442  zneo  9473  peano5uzti  9480  lincmb01cmp  10124  iccf1o  10125  nnsplit  10258  zpnn0elfzo1  10335  ubmelm1fzo  10353  fzoshftral  10365  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  qbtwnrelemcalc  10396  flqaddz  10438  2tnp1ge0ge0  10442  ceiqm1l  10454  qnegmod  10512  addmodlteq  10541  uzsinds  10587  seq3shft2  10624  iseqf1olemab  10645  exp3val  10684  binom2sub1  10797  binom3  10800  zesq  10801  sqoddm1div8  10836  nn0opthlem1d  10863  bcm1k  10903  bcp1n  10904  bcp1m1  10908  bcpasc  10909  bcn2m1  10912  omgadd  10945  hashfz  10964  hashfzo  10965  hashfzp1  10967  zfz1isolemsplit  10981  zfz1isolem1  10983  lswccatn0lsw  11065  ccatws1lenp1bg  11087  lswccats1  11093  resqrexlemover  11292  absexpzap  11362  reccn2ap  11595  hashiun  11760  hash2iun1dif1  11762  binomlem  11765  bcxmas  11771  arisum  11780  arisum2  11781  trireciplem  11782  geosergap  11788  pwm1geoserap1  11790  geolim  11793  geolim2  11794  georeclim  11795  geoisum1c  11802  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  cvgratnnlemsumlt  11810  cvgratz  11814  mertenslemi1  11817  prodf1f  11825  prodfrecap  11828  ntrivcvgap  11830  prodrbdclem  11853  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodntrivap  11866  prod1dc  11868  fprodmul  11873  prodsnf  11874  fprodsplitdc  11878  fprodm1  11880  fprodp1  11882  fprodcl  11889  fprodfac  11897  fprodrec  11911  fprodclf  11917  ef0lem  11942  efsub  11963  tanaddaplem  12020  tanaddap  12021  cos01bnd  12040  zeo3  12150  oddm1even  12157  oddp1even  12158  oexpneg  12159  ltoddhalfle  12175  halfleoddlt  12176  nn0ob  12190  flodddiv4  12218  bitsp1o  12235  bezoutlema  12291  bezoutlemb  12292  uzwodc  12329  qredeu  12390  prmdiv  12528  prmdiveq  12529  pc2dvds  12624  4sqlem11  12695  4sqlem12  12696  oddennn  12734  ennnfonelemp1  12748  gsumfzconst  13648  cncrng  14302  expcn  15012  hoverb  15091  dveflem  15169  dvef  15170  dvply2g  15209  reeff1oleme  15215  sin0pilem1  15224  logdivlti  15324  rpcxpmul2  15356  rplogbval  15388  perfectlem2  15443  lgsvalmod  15467  lgsdir2  15481  lgsdir  15483  gausslemma2dlem1a  15506  gausslemma2dlem5  15514  lgseisenlem4  15521  lgsquadlem1  15525  m1lgs  15533  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2lgslem3d1  15548  2lgsoddprmlem1  15553  2sqlem8  15571  cvgcmp2nlemabs  15933  iooref1o  15935  trilpolemeq1  15941  trilpolemlt1  15942  apdifflemr  15948  iswomni0  15952  nconstwlpolemgt0  15965