Theorem 1cnd 11228

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  1c1 11128

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

This theorem is referenced by:  adddirp1d  11259  1p1times  11404  addcom  11419  addcomd  11435  muladd11r  11446  pncan1  11659  npcan1  11660  muls1d  11695  mulsubfacd  11696  recrec  11936  rec11  11937  rec11r  11938  rereccl  11957  subrecd  12068  nn1m1nn  12259  add1p1  12490  sub1m1  12491  cnm2m1cnm3  12492  xp1d2m1eqxm1d2  12493  div4p1lem1div2  12494  nn0n0n1ge2  12567  zneo  12674  rpnnen1lem5  12995  lincmb01cmp  13510  iccf1o  13511  xov1plusxeqvd  13513  zpnn0elfzo1  13753  ubmelm1fzo  13777  fzosplitpr  13790  fzosplitprm1  13791  fzoshftral  13798  fladdz  13840  2tnp1ge0ge0  13844  ltdifltdiv  13849  dfceil2  13854  negmod  13932  modnegd  13942  addmodlteq  13962  binom2sub1  14237  binom3  14240  zesq  14242  sqoddm1div8  14259  bcm1k  14331  bcp1n  14332  bcp1m1  14336  bcpasc  14337  bcn2m1  14340  hashfz  14443  hashfzo  14445  hashfzp1  14447  hashf1lem2  14472  hashf1  14473  hashdifsnp1  14522  lswccatn0lsw  14607  ccatws1lenp1b  14637  revccat  14782  repswrevw  14803  cshwidxm1  14823  cshwidxn  14825  cshweqrep  14837  cshimadifsn0  14847  swrds2m  14958  swrd2lsw  14969  relexpaddnn  15068  absexpz  15322  reccn2  15611  rlimno1  15668  isercolllem1  15679  isercoll2  15683  iseraltlem2  15697  iseraltlem3  15698  fsump1  15770  hashiun  15836  hash2iun1dif1  15838  binomlem  15843  bcxmas  15849  incexc  15851  incexc2  15852  climcndslem1  15863  arisum  15874  arisum2  15875  trireciplem  15876  pwdif  15882  pwm1geoser  15883  geolim2  15885  georeclim  15886  mertenslem1  15898  prodfrec  15909  ntrivcvg  15911  ntrivcvgtail  15914  prodrblem  15943  prodmolem2a  15948  fprodntriv  15956  prod1  15958  fprodser  15963  fprodcl  15966  fprodm1  15981  fprodp1  15983  fprodclf  16006  risefacval2  16024  fallfacval2  16025  risefacp1  16043  fallfacp1  16044  risefacfac  16049  fallfacfwd  16050  binomfallfaclem2  16054  fallfacval4  16057  bpolydiflem  16068  ef0lem  16092  tanaddlem  16182  tanadd  16183  cos01bnd  16202  oddm1even  16360  oddp1even  16361  oexpneg  16362  ltoddhalfle  16378  halfleoddlt  16379  nn0ob  16401  pwp1fsum  16408  flodddiv4  16432  bitsp1o  16450  bitsf1  16463  sadcp1  16472  qredeu  16675  prmdiv  16802  prmdiveq  16803  vfermltlALT  16820  pc2dvds  16897  4sqlem11  16973  4sqlem12  16974  vdwapun  16992  vdwlem3  17001  vdwlem6  17004  vdwlem9  17007  ramub1lem2  17045  prmop1  17056  prmdvdsprmo  17060  prmgaplem8  17076  cshwshashnsame  17121  gsumsgrpccat  18816  psgnunilem5  19473  psgnunilem2  19474  sylow1lem1  19577  efgredlemc  19724  odadd2  19828  ablsimpgfindlem1  20088  srgbinomlem3  20186  srgbinomlem4  20187  cncrng  21349  cncrngOLD  21350  gzrngunit  21399  zringunit  21425  prmirredlem  21431  pzriprnglem12  21451  freshmansdream  21533  mhppwdeg  22086  psdmul  22102  cayhamlem1  22802  expcn  24812  expcnOLD  24814  iirevcn  24873  iihalf2cn  24878  iihalf2cnOLD  24879  icchmeo  24887  icchmeoOLD  24888  icopnfcnv  24889  icopnfhmeo  24890  evth  24907  pcoass  24973  pjthlem1  25387  ovolunlem1a  25447  ovolunlem1  25448  opnmbllem  25552  mbfi1fseqlem6  25671  bddibl  25791  dvnadd  25881  dvmptid  25911  dvmptdiv  25928  dvcnvlem  25930  dveflem  25933  dvef  25934  dvsincos  25935  dvlipcn  25949  dvivthlem1  25963  lhop2  25970  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgpowd  26007  ply1divex  26092  fta1glem1  26123  dgrcolem1  26229  dgrcolem2  26230  vieta1lem1  26268  aaliou3lem2  26301  aaliou3lem8  26303  dvtaylp  26328  dvntaylp  26329  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  abelthlem1  26391  abelthlem2  26392  abelthlem6  26396  abelthlem7  26398  logdivlti  26579  advlog  26613  advlogexp  26614  logtayl  26619  cxpmul2  26648  dvcxp1  26699  dvcxp2  26700  dvcncxp1  26702  dvcnsqrt  26703  loglesqrt  26721  relogbdiv  26739  ang180lem4  26772  ang180lem5  26773  isosctrlem2  26779  isosctrlem3  26780  affineequiv  26783  affineequiv2  26784  affineequiv3  26785  angpieqvdlem  26788  chordthmlem2  26793  chordthmlem3  26794  chordthmlem5  26796  dcubic2  26804  dcubic  26806  quart1lem  26815  quart1  26816  quart  26821  asinlem  26828  asinlem3  26831  atansopn  26892  dvatan  26895  leibpi  26902  birthdaylem2  26912  efrlim  26929  efrlimOLD  26930  cxplim  26932  divsqrtsumlem  26940  logdifbnd  26954  emcllem2  26957  emcllem3  26958  emcllem5  26960  zetacvg  26975  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamgulm2  26996  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  lgam1  27024  gamfac  27027  wilthlem2  27029  wilthimp  27032  ftalem5  27037  basellem3  27043  basellem5  27045  basellem8  27048  basellem9  27049  sqff1o  27142  muinv  27153  logfaclbnd  27183  logfacrlim  27185  logexprlim  27186  perfectlem2  27191  dchr1cl  27212  dchrinvcl  27214  dchrfi  27216  dchr1  27218  dchrsum2  27229  bcmono  27238  bcp1ctr  27240  bclbnd  27241  bposlem9  27253  gausslemma2dlem1a  27326  gausslemma2dlem5  27332  lgseisenlem4  27339  lgsquadlem1  27341  m1lgs  27349  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2lgslem3d1  27364  2lgsoddprmlem1  27369  2sqlem8  27387  2sq2  27394  addsqn2reu  27402  addsqrexnreu  27403  addsqnreup  27404  addsq2nreurex  27405  chtppilim  27436  rpvmasumlem  27448  dchrisumlem1  27450  dchrisum0re  27474  dchrisum0lem2a  27478  mudivsum  27491  mulogsumlem  27492  mulogsum  27493  2vmadivsumlem  27501  selberg4lem1  27521  pntrsumo1  27526  selberg34r  27532  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntibndlem2  27552  pntlemg  27559  pntlemr  27563  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntlem3  27570  ostth2lem2  27595  ttgcontlem1  28810  cusgrsize2inds  29379  wlklenvclwlk  29581  pthdadjvtx  29656  crctcshwlkn0lem1  29738  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  wlklnwwlkln2lem  29810  wlknwwlksnbij  29816  wwlksnred  29820  wwlksnext  29821  wwlksnextbi  29822  wwlksnredwwlkn  29823  wwlksnextwrd  29825  wwlksnextinj  29827  wwlksnextproplem2  29838  wwlksnextproplem3  29839  clwwlkccatlem  29916  clwlkclwwlklem2a1  29919  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwlkclwwlklem3  29928  clwlkclwwlk  29929  clwwisshclwwslemlem  29940  clwwisshclwws  29942  clwwlkel  29973  clwwlkf  29974  clwwlkwwlksb  29981  clwwlkext2edg  29983  wwlksext2clwwlk  29984  clwwlknonex2lem1  30034  clwwlknonex2lem2  30035  eucrct2eupth  30172  numclwwlk1lem2foalem  30278  numclwwlk1lem2fo  30285  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  numclwwlk6  30317  smcnlem  30624  receqid  32668  fzm1ne1  32711  bcm1n  32718  fzom1ne1  32724  ltesubnnd  32747  sgn0bi  32765  oexpled  32772  wrdt2ind  32875  chnub  32938  chnlt  32939  omndmul2  33026  psgnfzto1stlem  33057  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  archirngz  33133  archiabllem1a  33135  archiabllem2c  33139  ccfldextdgrr  33659  constrfin  33726  nn0constr  33741  iconstr  33746  constrrecl  33749  constrimcl  33750  constrreinvcl  33752  constrinvcl  33753  constrresqrtcl  33757  2sqr3minply  33760  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminply  33768  cos9thpinconstrlem1  33769  1smat1  33781  madjusmdetlem2  33805  madjusmdetlem4  33807  dya2icoseg  34255  iwrdsplit  34365  fibp1  34379  ballotlemfp1  34470  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemic  34485  ballotlem1c  34486  ballotlemsgt1  34489  ballotlemsdom  34490  ballotlemsel1i  34491  ballotlemsi  34493  ballotlemsima  34494  ballotlem1ri  34513  signstfvn  34547  signsvtn0  34548  signstfveq0  34555  signsvfn  34560  signsvtn  34562  signshf  34566  hashreprin  34598  circlemeth  34618  logdivsqrle  34628  revpfxsfxrev  35084  revwlk  35093  swrdwlk  35095  subfacp1lem1  35147  subfacp1lem5  35152  cvxpconn  35210  sinccvglem  35640  divcnvlin  35696  bcm1nt  35700  bcprod  35701  bccolsum  35702  iprodgam  35705  faclimlem1  35706  faclimlem2  35707  faclimlem3  35708  faclim  35709  iprodfac  35710  faclim2  35711  fwddifnp1  36129  dnizphlfeqhlf  36440  dnibndlem3  36444  dnibndlem13  36454  unblimceq0  36471  knoppndvlem6  36481  knoppndvlem9  36484  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem16  36491  knoppndvlem17  36492  bj-bary1lem1  37275  irrdiff  37290  poimirlem25  37615  poimirlem26  37616  poimirlem32  37622  opnmbllem0  37626  itg2addnclem2  37642  dvasin  37674  dvacos  37675  areacirclem1  37678  areacirclem4  37681  areacirc  37683  bfp  37794  fzsplitnd  41941  lcmfunnnd  41971  lcmineqlem1  41988  lcmineqlem3  41990  lcmineqlem4  41991  lcmineqlem7  41994  lcmineqlem8  41995  lcmineqlem10  41997  lcmineqlem11  41998  lcmineqlem12  41999  lcmineqlem18  42005  lcmineqlem19  42006  lcmineqlem22  42009  lcmineqlem23  42010  dvrelogpow2b  42027  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p3  42037  aks4d1p7d1  42041  primrootsunit1  42056  posbezout  42059  primrootscoprbij  42061  primrootspoweq0  42065  aks6d1c1  42075  hashscontpow1  42080  2np3bcnp1  42103  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones16  42121  sticksstones22  42127  aks6d1c6lem3  42131  aks6d1c7lem1  42139  unitscyglem5  42158  metakunt8  42171  metakunt12  42175  metakunt15  42178  metakunt16  42179  metakunt28  42191  nnadd1com  42264  nnaddcom  42265  nnadddir  42267  nnmul1com  42268  nnmulcom  42269  fz1sump1  42306  oddnumth  42307  nicomachus  42308  sumcubes  42309  tan3rdpi  42346  redvmptabs  42350  readvrec  42352  reixi  42412  sn-mullid  42425  sn-0tie0  42429  renegmulnnass  42443  fiabv  42506  fltnltalem  42632  fltnlta  42633  3cubeslem1  42654  3cubeslem2  42655  3cubeslem4  42659  pell1qrge1  42840  rmspecfund  42879  acongeq  42954  jm2.18  42959  jm2.19lem3  42962  jm2.25  42970  jm2.16nn0  42975  jm3.1lem1  42988  jm3.1lem2  42989  areaquad  43187  relexpmulnn  43680  relexpaddss  43689  cvgdvgrat  44285  radcnvrat  44286  hashnzfzclim  44294  ofdivrec  44298  expgrowthi  44305  bccm1k  44314  dvradcnv2  44319  binomcxplemwb  44320  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  refsum2cnlem1  45009  fzisoeu  45277  fperiodmullem  45280  fzdifsuc2  45287  xralrple2  45329  nnsplit  45333  infleinflem2  45346  fmul01lt1lem2  45562  fprodcn  45577  clim1fr1  45578  isumneg  45579  climneg  45587  sumnnodd  45607  reclimc  45630  coseq0  45841  coskpi2  45843  cosknegpi  45846  fprodcncf  45877  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnxpaek  45919  dvnmul  45920  dvmptfprod  45922  dvnprodlem3  45925  itgsinexp  45932  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem1  45978  stoweidlem7  45984  stoweidlem10  45987  stoweidlem11  45988  stoweidlem14  45991  stoweidlem17  45994  stoweidlem34  46011  stoweidlem42  46019  wallispilem3  46044  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem15  46065  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem11  46095  fourierdlem15  46099  fourierdlem26  46110  fourierdlem36  46120  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem56  46139  fourierdlem58  46141  fourierdlem59  46142  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem78  46161  fourierdlem79  46162  sqwvfoura  46205  fourierswlem  46207  fouriersw  46208  etransclem23  46234  etransclem24  46235  etransclem28  46239  etransclem35  46246  etransclem38  46249  nnfoctbdjlem  46432  smfmullem1  46768  sigaradd  46843  deccarry  47288  ceilbi  47310  m1modne  47325  fargshiftf1  47403  fargshiftfo  47404  fmtnof1  47497  sqrtpwpw2p  47500  fmtnorec2lem  47504  fmtnorec4  47511  fmtnoprmfac1lem  47526  fmtnoprmfac1  47527  fmtnoprmfac2  47529  2pwp1prm  47551  mod42tp1mod8  47564  sfprmdvdsmersenne  47565  lighneallem3  47569  lighneallem4  47572  onego  47608  zofldiv2ALTV  47624  oexpnegALTV  47639  opoeALTV  47645  opeoALTV  47646  epee  47667  perfectALTVlem1  47683  fppr2odd  47693  fpprwppr  47701  gpg3nbgrvtx0  48026  0nodd  48093  2nodd  48095  nnsgrpnmnd  48101  1neven  48161  altgsumbc  48275  pw2m1lepw2m1  48444  m1modmmod  48449  zofldiv2  48459  nnpw2pmod  48511  blen1b  48516  blennn0em1  48519  dignn0flhalflem1  48543  dignn0flhalflem2  48544  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  nn0sumshdiglem2  48550  itcovalpclem2  48599  ackval1  48609  ackval2  48610  ackval3  48611  affineid  48632  1subrec1sub  48633  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2vlinest  48669