Theorem 1cnd 10707

Description: One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 10666	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 10606  1c1 10609

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

This theorem is referenced by:  adddirp1d  10738  1p1times  10882  addcom  10897  addcomd  10913  muladd11r  10924  pncan1  11135  npcan1  11136  muls1d  11171  mulsubfacd  11172  recrec  11408  rec11  11409  rec11r  11410  rereccl  11429  subrec  11540  nn1m1nn  11730  add1p1  11960  sub1m1  11961  cnm2m1cnm3  11962  xp1d2m1eqxm1d2  11963  div4p1lem1div2  11964  nn0n0n1ge2  12036  zneo  12139  rpnnen1lem5  12456  lincmb01cmp  12962  iccf1o  12963  xov1plusxeqvd  12965  zpnn0elfzo1  13195  ubmelm1fzo  13217  fzosplitpr  13230  fzosplitprm1  13231  fzoshftral  13238  fladdz  13279  2tnp1ge0ge0  13283  ltdifltdiv  13288  dfceil2  13293  negmod  13368  modnegd  13378  addmodlteq  13398  binom2sub1  13667  binom3  13670  zesq  13672  sqoddm1div8  13689  bcm1k  13760  bcp1n  13761  bcp1m1  13765  bcpasc  13766  bcn2m1  13769  hashfz  13873  hashfzo  13875  hashfzp1  13877  hashf1lem2  13901  hashf1  13902  hashdifsnp1  13941  lswccatn0lsw  14027  ccatws1lenp1b  14057  revccat  14210  repswrevw  14231  cshwidxm1  14251  cshwidxn  14253  cshweqrep  14265  cshimadifsn0  14274  swrds2m  14385  swrd2lsw  14396  relexpaddnn  14493  absexpz  14748  reccn2  15037  rlimno1  15096  isercolllem1  15107  isercoll2  15111  iseraltlem2  15125  iseraltlem3  15126  hashiun  15263  hash2iun1dif1  15265  binomlem  15270  bcxmas  15276  incexc  15278  incexc2  15279  climcndslem1  15290  arisum  15301  arisum2  15302  trireciplem  15303  pwdif  15309  pwm1geoser  15310  geolim2  15312  georeclim  15313  mertenslem1  15325  prodfrec  15336  ntrivcvg  15338  ntrivcvgtail  15341  prodrblem  15368  prodmolem2a  15373  fprodntriv  15381  prod1  15383  fprodser  15388  fprodcl  15391  fprodm1  15406  fprodp1  15408  fprodclf  15431  risefacval2  15449  fallfacval2  15450  risefacp1  15468  fallfacp1  15469  risefacfac  15474  fallfacfwd  15475  binomfallfaclem2  15479  fallfacval4  15482  bpolydiflem  15493  ef0lem  15517  tanaddlem  15604  tanadd  15605  cos01bnd  15624  oddm1even  15781  oddp1even  15782  oexpneg  15783  ltoddhalfle  15799  halfleoddlt  15800  nn0ob  15822  pwp1fsum  15829  flodddiv4  15851  bitsp1o  15869  bitsf1  15882  sadcp1  15891  qredeu  16092  prmdiv  16215  prmdiveq  16216  vfermltlALT  16232  pc2dvds  16308  4sqlem11  16384  4sqlem12  16385  vdwapun  16403  vdwlem3  16412  vdwlem6  16415  vdwlem9  16418  ramub1lem2  16456  prmop1  16467  prmdvdsprmo  16471  prmgaplem8  16487  cshwshashnsame  16533  gsumsgrpccat  18113  gsumccatOLD  18114  psgnunilem5  18733  psgnunilem2  18734  sylow1lem1  18834  efgredlemc  18982  odadd2  19081  ablsimpgfindlem1  19341  srgbinomlem3  19404  srgbinomlem4  19405  cncrng  20231  gzrngunit  20276  zringunit  20300  prmirredlem  20306  mhppwdeg  20937  cayhamlem1  21610  expcn  23617  iirevcn  23675  iihalf2cn  23679  icchmeo  23686  icopnfcnv  23687  icopnfhmeo  23688  evth  23704  pcoass  23769  pjthlem1  24182  ovolunlem1a  24241  ovolunlem1  24242  opnmbllem  24346  mbfi1fseqlem6  24465  bddibl  24584  dvnadd  24673  dvmptid  24701  dvmptdiv  24718  dvcnvlem  24720  dveflem  24723  dvef  24724  dvsincos  24725  dvlipcn  24738  dvivthlem1  24752  lhop2  24759  dvcvx  24764  dvfsumle  24765  dvfsumabs  24767  dvfsumlem1  24770  dvfsumlem2  24771  itgpowd  24794  ply1divex  24881  fta1glem1  24910  dgrcolem1  25014  dgrcolem2  25015  vieta1lem1  25050  aaliou3lem2  25083  aaliou3lem8  25085  dvtaylp  25109  dvntaylp  25110  taylthlem1  25112  taylthlem2  25113  abelthlem1  25170  abelthlem2  25171  abelthlem6  25175  abelthlem7  25177  logdivlti  25355  advlog  25389  advlogexp  25390  logtayl  25395  cxpmul2  25424  dvcxp1  25473  dvcxp2  25474  dvcncxp1  25476  dvcnsqrt  25477  loglesqrt  25491  relogbdiv  25509  ang180lem4  25542  ang180lem5  25543  isosctrlem2  25549  isosctrlem3  25550  affineequiv  25553  affineequiv2  25554  affineequiv3  25555  angpieqvdlem  25558  chordthmlem2  25563  chordthmlem3  25564  chordthmlem5  25566  dcubic2  25574  dcubic  25576  quart1lem  25585  quart1  25586  quart  25591  asinlem  25598  asinlem3  25601  atansopn  25662  dvatan  25665  leibpi  25672  birthdaylem2  25682  efrlim  25699  cxplim  25701  divsqrtsumlem  25709  logdifbnd  25723  emcllem2  25726  emcllem3  25727  emcllem5  25729  zetacvg  25744  lgamgulmlem2  25759  lgamgulmlem3  25760  lgamgulmlem4  25761  lgamgulmlem5  25762  lgamgulmlem6  25763  lgamgulm2  25765  lgamcvg2  25784  gamcvg  25785  gamcvg2lem  25788  lgam1  25793  gamfac  25796  wilthlem2  25798  wilthimp  25801  ftalem5  25806  basellem3  25812  basellem5  25814  basellem8  25817  basellem9  25818  sqff1o  25911  muinv  25922  logfaclbnd  25950  logfacrlim  25952  logexprlim  25953  perfectlem2  25958  dchr1cl  25979  dchrinvcl  25981  dchrfi  25983  dchr1  25985  dchrsum2  25996  bcmono  26005  bcp1ctr  26007  bclbnd  26008  bposlem9  26020  gausslemma2dlem1a  26093  gausslemma2dlem5  26099  lgseisenlem4  26106  lgsquadlem1  26108  m1lgs  26116  2lgslem3a  26124  2lgslem3b  26125  2lgslem3c  26126  2lgslem3d  26127  2lgslem3d1  26131  2lgsoddprmlem1  26136  2sqlem8  26154  2sq2  26161  addsqn2reu  26169  addsqrexnreu  26170  addsqnreup  26171  addsq2nreurex  26172  chtppilim  26203  rpvmasumlem  26215  dchrisumlem1  26217  dchrisum0re  26241  dchrisum0lem2a  26245  mudivsum  26258  mulogsumlem  26259  mulogsum  26260  2vmadivsumlem  26268  selberg4lem1  26288  pntrsumo1  26293  selberg34r  26299  pntrlog2bndlem2  26306  pntrlog2bndlem4  26308  pntrlog2bndlem5  26309  pntrlog2bndlem6  26311  pntibndlem2  26319  pntlemg  26326  pntlemr  26330  pntlemf  26333  pntlemk  26334  pntlemo  26335  pntlem3  26337  ostth2lem2  26362  ttgcontlem1  26823  cusgrsize2inds  27387  wlklenvclwlk  27588  wlklenvclwlkOLD  27589  pthdadjvtx  27663  crctcshwlkn0lem1  27740  crctcshwlkn0lem4  27743  crctcshwlkn0lem5  27744  wlklnwwlkln2lem  27812  wlknwwlksnbij  27818  wwlksnred  27822  wwlksnext  27823  wwlksnextbi  27824  wwlksnredwwlkn  27825  wwlksnextwrd  27827  wwlksnextinj  27829  wwlksnextproplem2  27840  wwlksnextproplem3  27841  clwwlkccatlem  27918  clwlkclwwlklem2a1  27921  clwlkclwwlklem2a4  27926  clwlkclwwlklem2a  27927  clwlkclwwlklem2  27929  clwlkclwwlklem3  27930  clwlkclwwlk  27931  clwwisshclwwslemlem  27942  clwwisshclwws  27944  clwwlkel  27975  clwwlkf  27976  clwwlkwwlksb  27983  clwwlkext2edg  27985  wwlksext2clwwlk  27986  clwwlknonex2lem1  28036  clwwlknonex2lem2  28037  eucrct2eupth  28174  numclwwlk1lem2foalem  28280  numclwwlk1lem2fo  28287  numclwlk2lem2f  28306  numclwlk2lem2f1o  28308  numclwwlk6  28319  smcnlem  28624  fzm1ne1  30677  bcm1n  30683  fzom1ne1  30689  ltesubnnd  30703  wrdt2ind  30792  omndmul2  30907  psgnfzto1stlem  30936  cycpmco2lem3  30964  cycpmco2lem4  30965  cycpmco2lem5  30966  cycpmco2lem6  30967  cycpmco2lem7  30968  cycpmco2  30969  archirngz  31012  archiabllem1a  31014  archiabllem2c  31018  freshmansdream  31053  ccfldextdgrr  31306  1smat1  31318  madjusmdetlem2  31342  madjusmdetlem4  31344  dya2icoseg  31806  iwrdsplit  31916  fibp1  31930  ballotlemfp1  32020  ballotlemfc0  32021  ballotlemfcc  32022  ballotlemic  32035  ballotlem1c  32036  ballotlemsgt1  32039  ballotlemsdom  32040  ballotlemsel1i  32041  ballotlemsi  32043  ballotlemsima  32044  ballotlem1ri  32063  sgn0bi  32076  signstfvn  32110  signsvtn0  32111  signstfveq0  32118  signsvfn  32123  signsvtn  32125  signshf  32129  hashreprin  32162  circlemeth  32182  logdivsqrle  32192  revpfxsfxrev  32640  revwlk  32649  swrdwlk  32651  subfacp1lem1  32704  subfacp1lem5  32709  cvxpconn  32767  sinccvglem  33193  divcnvlin  33261  bcm1nt  33266  bcprod  33267  bccolsum  33268  iprodgam  33271  faclimlem1  33272  faclimlem2  33273  faclimlem3  33274  faclim  33275  iprodfac  33276  faclim2  33277  fwddifnp1  34097  dnizphlfeqhlf  34286  dnibndlem3  34290  dnibndlem13  34300  unblimceq0  34317  knoppndvlem6  34327  knoppndvlem9  34330  knoppndvlem14  34335  knoppndvlem15  34336  knoppndvlem16  34337  knoppndvlem17  34338  bj-bary1lem1  35091  irrdiff  35106  poimirlem25  35414  poimirlem26  35415  poimirlem32  35421  opnmbllem0  35425  itg2addnclem2  35441  dvasin  35473  dvacos  35474  areacirclem1  35477  areacirclem4  35480  areacirc  35482  bfp  35594  fzsplitnd  39600  lcmfunnnd  39629  lcmineqlem1  39646  lcmineqlem3  39648  lcmineqlem4  39649  lcmineqlem7  39652  lcmineqlem8  39653  lcmineqlem10  39655  lcmineqlem11  39656  lcmineqlem12  39657  lcmineqlem18  39663  lcmineqlem19  39664  lcmineqlem22  39667  lcmineqlem23  39668  dvrelogpow2b  39684  aks4d1p1p4  39687  aks4d1p1p6  39689  aks4d1p1p7  39690  aks4d1p1p5  39691  aks4d1p1  39692  2np3bcnp1  39695  metakunt8  39712  metakunt12  39716  metakunt15  39719  metakunt16  39720  metakunt28  39732  nnadd1com  39857  nnaddcom  39858  nnadddir  39860  nnmul1com  39861  nnmulcom  39862  reixi  39965  sn-mulid2  39978  sn-0tie0  39982  fltnltalem  40055  fltnlta  40056  3cubeslem1  40062  3cubeslem2  40063  3cubeslem4  40067  pell1qrge1  40248  rmspecfund  40287  acongeq  40361  jm2.18  40366  jm2.19lem3  40369  jm2.25  40377  jm2.16nn0  40382  jm3.1lem1  40395  jm3.1lem2  40396  areaquad  40603  relexpmulnn  40847  relexpaddss  40856  cvgdvgrat  41453  radcnvrat  41454  hashnzfzclim  41462  ofdivrec  41466  expgrowthi  41473  bccm1k  41482  dvradcnv2  41487  binomcxplemwb  41488  binomcxplemnn0  41489  binomcxplemrat  41490  binomcxplemfrat  41491  binomcxplemdvbinom  41493  binomcxplemnotnn0  41496  refsum2cnlem1  42102  fzisoeu  42361  fperiodmullem  42364  fzdifsuc2  42371  xralrple2  42415  nnsplit  42419  infleinflem2  42432  fmul01lt1lem2  42652  fprodcn  42667  clim1fr1  42668  isumneg  42669  climneg  42677  sumnnodd  42697  reclimc  42720  coseq0  42931  coskpi2  42933  cosknegpi  42936  fprodcncf  42967  fprodsubrecnncnvlem  42974  fprodaddrecnncnvlem  42976  ioodvbdlimc1lem2  42999  ioodvbdlimc2lem  43001  dvnxpaek  43009  dvnmul  43010  dvmptfprod  43012  dvnprodlem3  43015  itgsinexp  43022  itgiccshift  43047  itgperiod  43048  itgsbtaddcnst  43049  stoweidlem1  43068  stoweidlem7  43074  stoweidlem10  43077  stoweidlem11  43078  stoweidlem14  43081  stoweidlem17  43084  stoweidlem34  43101  stoweidlem42  43109  wallispilem3  43134  wallispilem5  43136  wallispi  43137  wallispi2lem1  43138  wallispi2lem2  43139  wallispi2  43140  stirlinglem1  43141  stirlinglem3  43143  stirlinglem4  43144  stirlinglem5  43145  stirlinglem6  43146  stirlinglem7  43147  stirlinglem8  43148  stirlinglem10  43150  stirlinglem11  43151  stirlinglem12  43152  stirlinglem13  43153  stirlinglem15  43155  dirkertrigeqlem2  43166  dirkertrigeqlem3  43167  dirkertrigeq  43168  dirkercncflem1  43170  dirkercncflem2  43171  dirkercncflem4  43173  fourierdlem11  43185  fourierdlem15  43189  fourierdlem26  43200  fourierdlem36  43210  fourierdlem40  43214  fourierdlem41  43215  fourierdlem42  43216  fourierdlem48  43221  fourierdlem49  43222  fourierdlem56  43229  fourierdlem58  43231  fourierdlem59  43232  fourierdlem62  43235  fourierdlem64  43237  fourierdlem65  43238  fourierdlem78  43251  fourierdlem79  43252  sqwvfoura  43295  fourierswlem  43297  fouriersw  43298  etransclem23  43324  etransclem24  43325  etransclem28  43329  etransclem35  43336  etransclem38  43339  nnfoctbdjlem  43519  smfmullem1  43848  sigaradd  43905  deccarry  44321  fargshiftf1  44411  fargshiftfo  44412  fmtnof1  44505  sqrtpwpw2p  44508  fmtnorec2lem  44512  fmtnorec4  44519  fmtnoprmfac1lem  44534  fmtnoprmfac1  44535  fmtnoprmfac2  44537  2pwp1prm  44559  mod42tp1mod8  44572  sfprmdvdsmersenne  44573  lighneallem3  44577  lighneallem4  44580  onego  44616  zofldiv2ALTV  44632  oexpnegALTV  44647  opoeALTV  44653  opeoALTV  44654  epee  44675  perfectALTVlem1  44691  fppr2odd  44701  fpprwppr  44709  0nodd  44882  2nodd  44884  nnsgrpnmnd  44890  1neven  45008  altgsumbc  45206  pw2m1lepw2m1  45379  m1modmmod  45385  zofldiv2  45395  nnpw2pmod  45447  blen1b  45452  blennn0em1  45455  dignn0flhalflem1  45479  dignn0flhalflem2  45480  nn0sumshdiglemB  45484  nn0sumshdiglem1  45485  nn0sumshdiglem2  45486  itcovalpclem2  45535  ackval1  45545  ackval2  45546  ackval3  45547  affineid  45568  1subrec1sub  45569  eenglngeehlnmlem1  45601  eenglngeehlnmlem2  45602  rrx2vlinest  45605