Theorem 1cnd 8194

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8029  1c1 8032

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

This theorem is referenced by:  adddirp1d  8205  muladd11r  8334  muls1d  8596  recrecap  8888  rec11ap  8889  rec11rap  8890  rerecclap  8909  subrecap  9018  recp1lt1  9078  nn1m1nn  9160  add1p1  9393  sub1m1  9394  cnm2m1cnm3  9395  xp1d2m1eqxm1d2  9396  div4p1lem1div2  9397  peano2z  9514  zaddcllempos  9515  peano2zm  9516  zaddcllemneg  9517  nn0n0n1ge2  9549  zneo  9580  peano5uzti  9587  lincmb01cmp  10237  iccf1o  10238  nnsplit  10371  zpnn0elfzo1  10452  ubmelm1fzo  10470  fzosplitpr  10478  fzoshftral  10483  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  qbtwnrelemcalc  10514  flqaddz  10556  2tnp1ge0ge0  10560  ceiqm1l  10572  qnegmod  10630  addmodlteq  10659  uzsinds  10705  seq3shft2  10742  iseqf1olemab  10763  exp3val  10802  binom2sub1  10915  binom3  10918  zesq  10919  sqoddm1div8  10954  nn0opthlem1d  10981  bcm1k  11021  bcp1n  11022  bcp1m1  11026  bcpasc  11027  bcn2m1  11030  omgadd  11064  hashfz  11084  hashfzo  11085  hashfzp1  11087  zfz1isolemsplit  11101  zfz1isolem1  11103  lswccatn0lsw  11187  ccatws1lenp1bg  11211  lswccats1  11219  resqrexlemover  11570  absexpzap  11640  reccn2ap  11873  hashiun  12038  hash2iun1dif1  12040  binomlem  12043  bcxmas  12049  arisum  12058  arisum2  12059  trireciplem  12060  geosergap  12066  pwm1geoserap1  12068  geolim  12071  geolim2  12072  georeclim  12073  geoisum1c  12080  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemsumlt  12088  cvgratz  12092  mertenslemi1  12095  prodf1f  12103  prodfrecap  12106  ntrivcvgap  12108  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prod1dc  12146  fprodmul  12151  prodsnf  12152  fprodsplitdc  12156  fprodm1  12158  fprodp1  12160  fprodcl  12167  fprodfac  12175  fprodrec  12189  fprodclf  12195  ef0lem  12220  efsub  12241  tanaddaplem  12298  tanaddap  12299  cos01bnd  12318  zeo3  12428  oddm1even  12435  oddp1even  12436  oexpneg  12437  ltoddhalfle  12453  halfleoddlt  12454  nn0ob  12468  flodddiv4  12496  bitsp1o  12513  bezoutlema  12569  bezoutlemb  12570  uzwodc  12607  qredeu  12668  prmdiv  12806  prmdiveq  12807  pc2dvds  12902  4sqlem11  12973  4sqlem12  12974  oddennn  13012  ennnfonelemp1  13026  gsumfzconst  13927  cncrng  14582  expcn  15292  hoverb  15371  dveflem  15449  dvef  15450  dvply2g  15489  reeff1oleme  15495  sin0pilem1  15504  logdivlti  15604  rpcxpmul2  15636  rplogbval  15668  perfectlem2  15723  lgsvalmod  15747  lgsdir2  15761  lgsdir  15763  gausslemma2dlem1a  15786  gausslemma2dlem5  15794  lgseisenlem4  15801  lgsquadlem1  15805  m1lgs  15813  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3d1  15828  2lgsoddprmlem1  15833  2sqlem8  15851  wlklenvclwlk  16223  clwwlkccatlem  16250  clwwlkext2edg  16272  clwwlknonex2lem1  16287  clwwlknonex2lem2  16288  cvgcmp2nlemabs  16636  iooref1o  16638  trilpolemeq1  16644  trilpolemlt1  16645  apdifflemr  16651  iswomni0  16655  nconstwlpolemgt0  16668  gsumgfsumlem  16683  gsumgfsum  16684