Theorem 1cnd 8290

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  1c1 8128

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

This theorem is referenced by:  adddirp1d  8300  muladd11r  8429  muls1d  8691  recrecap  8983  rec11ap  8984  rec11rap  8985  rerecclap  9004  subrecap  9113  recp1lt1  9173  nn1m1nn  9255  add1p1  9488  sub1m1  9489  cnm2m1cnm3  9490  xp1d2m1eqxm1d2  9491  div4p1lem1div2  9492  peano2z  9613  zaddcllempos  9614  peano2zm  9615  zaddcllemneg  9616  nn0n0n1ge2  9648  zneo  9679  peano5uzti  9686  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  nnsplit  10471  zpnn0elfzo1  10553  ubmelm1fzo  10571  fzosplitpr  10579  fzoshftral  10584  exbtwnzlemstep  10607  rebtwn2zlemstep  10612  qbtwnrelemcalc  10615  flqaddz  10657  2tnp1ge0ge0  10661  ceiqm1l  10673  qnegmod  10731  addmodlteq  10760  uzsinds  10806  seq3shft2  10843  iseqf1olemab  10864  exp3val  10903  binom2sub1  11016  binom3  11019  zesq  11020  sqoddm1div8  11055  nn0opthlem1d  11082  bcm1k  11122  bcp1n  11123  bcp1m1  11127  bcpasc  11128  bcm1n  11131  bcn2m1  11132  omgadd  11166  hashfz  11186  hashfzo  11187  hashfzp1  11189  zfz1isolemsplit  11210  zfz1isolem1  11212  lswccatn0lsw  11299  ccatws1lenp1bg  11323  lswccats1  11331  resqrexlemover  11695  absexpzap  11765  reccn2ap  11998  hashiun  12164  hash2iun1dif1  12166  binomlem  12169  bcxmas  12175  arisum  12184  arisum2  12185  trireciplem  12186  geosergap  12192  pwm1geoserap1  12194  geolim  12197  geolim2  12198  georeclim  12199  geoisum1c  12206  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemsumlt  12214  cvgratz  12218  mertenslemi1  12221  prodf1f  12229  prodfrecap  12232  ntrivcvgap  12234  prodrbdclem  12257  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodntrivap  12270  prod1dc  12272  fprodmul  12277  prodsnf  12278  fprodsplitdc  12282  fprodm1  12284  fprodp1  12286  fprodcl  12293  fprodfac  12301  fprodrec  12315  fprodclf  12321  ef0lem  12346  efsub  12367  tanaddaplem  12424  tanaddap  12425  cos01bnd  12444  zeo3  12554  oddm1even  12561  oddp1even  12562  oexpneg  12563  ltoddhalfle  12579  halfleoddlt  12580  nn0ob  12594  flodddiv4  12622  bitsp1o  12639  bezoutlema  12695  bezoutlemb  12696  uzwodc  12733  qredeu  12794  prmdiv  12932  prmdiveq  12933  pc2dvds  13028  4sqlem11  13099  4sqlem12  13100  oddennn  13143  ennnfonelemp1  13157  gsumfzconst  14058  gsumsplit0  14063  cncrng  14717  expcn  15434  hoverb  15513  dveflem  15591  dvef  15592  dvply2g  15631  reeff1oleme  15637  sin0pilem1  15646  logdivlti  15746  rpcxpmul2  15778  rplogbval  15810  perfectlem2  15868  lgsvalmod  15892  lgsdir2  15906  lgsdir  15908  gausslemma2dlem1a  15931  gausslemma2dlem5  15939  lgseisenlem4  15946  lgsquadlem1  15950  m1lgs  15958  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgslem3d1  15973  2lgsoddprmlem1  15978  2sqlem8  15996  wlklenvclwlk  16368  clwwlkccatlem  16395  clwwlkext2edg  16417  clwwlknonex2lem1  16432  clwwlknonex2lem2  16433  cvgcmp2nlemabs  16816  iooref1o  16818  trilpolemeq1  16824  trilpolemlt1  16825  apdifflemr  16831  qdiff  16833  iswomni0  16836  nconstwlpolemgt0  16850  gsumgfsumlem  16865  gsumgfsum  16866