Theorem 1cnd 8195

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  1c1 8033

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

This theorem is referenced by:  adddirp1d  8206  muladd11r  8335  muls1d  8597  recrecap  8889  rec11ap  8890  rec11rap  8891  rerecclap  8910  subrecap  9019  recp1lt1  9079  nn1m1nn  9161  add1p1  9394  sub1m1  9395  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  peano2z  9515  zaddcllempos  9516  peano2zm  9517  zaddcllemneg  9518  nn0n0n1ge2  9550  zneo  9581  peano5uzti  9588  lincmb01cmp  10238  iccf1o  10239  nnsplit  10372  zpnn0elfzo1  10454  ubmelm1fzo  10472  fzosplitpr  10480  fzoshftral  10485  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  qbtwnrelemcalc  10516  flqaddz  10558  2tnp1ge0ge0  10562  ceiqm1l  10574  qnegmod  10632  addmodlteq  10661  uzsinds  10707  seq3shft2  10744  iseqf1olemab  10765  exp3val  10804  binom2sub1  10917  binom3  10920  zesq  10921  sqoddm1div8  10956  nn0opthlem1d  10983  bcm1k  11023  bcp1n  11024  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  omgadd  11066  hashfz  11086  hashfzo  11087  hashfzp1  11089  zfz1isolemsplit  11103  zfz1isolem1  11105  lswccatn0lsw  11192  ccatws1lenp1bg  11216  lswccats1  11224  resqrexlemover  11575  absexpzap  11645  reccn2ap  11878  hashiun  12044  hash2iun1dif1  12046  binomlem  12049  bcxmas  12055  arisum  12064  arisum2  12065  trireciplem  12066  geosergap  12072  pwm1geoserap1  12074  geolim  12077  geolim2  12078  georeclim  12079  geoisum1c  12086  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratnnlemsumlt  12094  cvgratz  12098  mertenslemi1  12101  prodf1f  12109  prodfrecap  12112  ntrivcvgap  12114  prodrbdclem  12137  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodntrivap  12150  prod1dc  12152  fprodmul  12157  prodsnf  12158  fprodsplitdc  12162  fprodm1  12164  fprodp1  12166  fprodcl  12173  fprodfac  12181  fprodrec  12195  fprodclf  12201  ef0lem  12226  efsub  12247  tanaddaplem  12304  tanaddap  12305  cos01bnd  12324  zeo3  12434  oddm1even  12441  oddp1even  12442  oexpneg  12443  ltoddhalfle  12459  halfleoddlt  12460  nn0ob  12474  flodddiv4  12502  bitsp1o  12519  bezoutlema  12575  bezoutlemb  12576  uzwodc  12613  qredeu  12674  prmdiv  12812  prmdiveq  12813  pc2dvds  12908  4sqlem11  12979  4sqlem12  12980  oddennn  13018  ennnfonelemp1  13032  gsumfzconst  13933  gsumsplit0  13938  cncrng  14589  expcn  15299  hoverb  15378  dveflem  15456  dvef  15457  dvply2g  15496  reeff1oleme  15502  sin0pilem1  15511  logdivlti  15611  rpcxpmul2  15643  rplogbval  15675  perfectlem2  15730  lgsvalmod  15754  lgsdir2  15768  lgsdir  15770  gausslemma2dlem1a  15793  gausslemma2dlem5  15801  lgseisenlem4  15808  lgsquadlem1  15812  m1lgs  15820  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgslem3d1  15835  2lgsoddprmlem1  15840  2sqlem8  15858  wlklenvclwlk  16230  clwwlkccatlem  16257  clwwlkext2edg  16279  clwwlknonex2lem1  16294  clwwlknonex2lem2  16295  cvgcmp2nlemabs  16662  iooref1o  16664  trilpolemeq1  16670  trilpolemlt1  16671  apdifflemr  16677  qdiff  16679  iswomni0  16682  nconstwlpolemgt0  16695  gsumgfsumlem  16710  gsumgfsum  16711