Theorem 1cnd 11209

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  1c1 11111

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

This theorem is referenced by:  adddirp1d  11240  1p1times  11385  addcom  11400  addcomd  11416  muladd11r  11427  pncan1  11638  npcan1  11639  muls1d  11674  mulsubfacd  11675  recrec  11911  rec11  11912  rec11r  11913  rereccl  11932  subrec  12043  nn1m1nn  12233  add1p1  12463  sub1m1  12464  cnm2m1cnm3  12465  xp1d2m1eqxm1d2  12466  div4p1lem1div2  12467  nn0n0n1ge2  12539  zneo  12645  rpnnen1lem5  12965  lincmb01cmp  13472  iccf1o  13473  xov1plusxeqvd  13475  zpnn0elfzo1  13706  ubmelm1fzo  13728  fzosplitpr  13741  fzosplitprm1  13742  fzoshftral  13749  fladdz  13790  2tnp1ge0ge0  13794  ltdifltdiv  13799  dfceil2  13804  negmod  13881  modnegd  13891  addmodlteq  13911  binom2sub1  14184  binom3  14187  zesq  14189  sqoddm1div8  14206  bcm1k  14275  bcp1n  14276  bcp1m1  14280  bcpasc  14281  bcn2m1  14284  hashfz  14387  hashfzo  14389  hashfzp1  14391  hashf1lem2  14417  hashf1  14418  hashdifsnp1  14457  lswccatn0lsw  14541  ccatws1lenp1b  14571  revccat  14716  repswrevw  14737  cshwidxm1  14757  cshwidxn  14759  cshweqrep  14771  cshimadifsn0  14781  swrds2m  14892  swrd2lsw  14903  relexpaddnn  14998  absexpz  15252  reccn2  15541  rlimno1  15600  isercolllem1  15611  isercoll2  15615  iseraltlem2  15629  iseraltlem3  15630  fsump1  15702  hashiun  15768  hash2iun1dif1  15770  binomlem  15775  bcxmas  15781  incexc  15783  incexc2  15784  climcndslem1  15795  arisum  15806  arisum2  15807  trireciplem  15808  pwdif  15814  pwm1geoser  15815  geolim2  15817  georeclim  15818  mertenslem1  15830  prodfrec  15841  ntrivcvg  15843  ntrivcvgtail  15846  prodrblem  15873  prodmolem2a  15878  fprodntriv  15886  prod1  15888  fprodser  15893  fprodcl  15896  fprodm1  15911  fprodp1  15913  fprodclf  15936  risefacval2  15954  fallfacval2  15955  risefacp1  15973  fallfacp1  15974  risefacfac  15979  fallfacfwd  15980  binomfallfaclem2  15984  fallfacval4  15987  bpolydiflem  15998  ef0lem  16022  tanaddlem  16109  tanadd  16110  cos01bnd  16129  oddm1even  16286  oddp1even  16287  oexpneg  16288  ltoddhalfle  16304  halfleoddlt  16305  nn0ob  16327  pwp1fsum  16334  flodddiv4  16356  bitsp1o  16374  bitsf1  16387  sadcp1  16396  qredeu  16595  prmdiv  16718  prmdiveq  16719  vfermltlALT  16735  pc2dvds  16812  4sqlem11  16888  4sqlem12  16889  vdwapun  16907  vdwlem3  16916  vdwlem6  16919  vdwlem9  16922  ramub1lem2  16960  prmop1  16971  prmdvdsprmo  16975  prmgaplem8  16991  cshwshashnsame  17037  gsumsgrpccat  18721  psgnunilem5  19362  psgnunilem2  19363  sylow1lem1  19466  efgredlemc  19613  odadd2  19717  ablsimpgfindlem1  19977  srgbinomlem3  20051  srgbinomlem4  20052  cncrng  20966  gzrngunit  21011  zringunit  21036  prmirredlem  21042  mhppwdeg  21693  cayhamlem1  22368  expcn  24388  iirevcn  24446  iihalf2cn  24450  icchmeo  24457  icopnfcnv  24458  icopnfhmeo  24459  evth  24475  pcoass  24540  pjthlem1  24954  ovolunlem1a  25013  ovolunlem1  25014  opnmbllem  25118  mbfi1fseqlem6  25238  bddibl  25357  dvnadd  25446  dvmptid  25474  dvmptdiv  25491  dvcnvlem  25493  dveflem  25496  dvef  25497  dvsincos  25498  dvlipcn  25511  dvivthlem1  25525  lhop2  25532  dvcvx  25537  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem2  25544  itgpowd  25567  ply1divex  25654  fta1glem1  25683  dgrcolem1  25787  dgrcolem2  25788  vieta1lem1  25823  aaliou3lem2  25856  aaliou3lem8  25858  dvtaylp  25882  dvntaylp  25883  taylthlem1  25885  taylthlem2  25886  abelthlem1  25943  abelthlem2  25944  abelthlem6  25948  abelthlem7  25950  logdivlti  26128  advlog  26162  advlogexp  26163  logtayl  26168  cxpmul2  26197  dvcxp1  26248  dvcxp2  26249  dvcncxp1  26251  dvcnsqrt  26252  loglesqrt  26266  relogbdiv  26284  ang180lem4  26317  ang180lem5  26318  isosctrlem2  26324  isosctrlem3  26325  affineequiv  26328  affineequiv2  26329  affineequiv3  26330  angpieqvdlem  26333  chordthmlem2  26338  chordthmlem3  26339  chordthmlem5  26341  dcubic2  26349  dcubic  26351  quart1lem  26360  quart1  26361  quart  26366  asinlem  26373  asinlem3  26376  atansopn  26437  dvatan  26440  leibpi  26447  birthdaylem2  26457  efrlim  26474  cxplim  26476  divsqrtsumlem  26484  logdifbnd  26498  emcllem2  26501  emcllem3  26502  emcllem5  26504  zetacvg  26519  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgamcvg2  26559  gamcvg  26560  gamcvg2lem  26563  lgam1  26568  gamfac  26571  wilthlem2  26573  wilthimp  26576  ftalem5  26581  basellem3  26587  basellem5  26589  basellem8  26592  basellem9  26593  sqff1o  26686  muinv  26697  logfaclbnd  26725  logfacrlim  26727  logexprlim  26728  perfectlem2  26733  dchr1cl  26754  dchrinvcl  26756  dchrfi  26758  dchr1  26760  dchrsum2  26771  bcmono  26780  bcp1ctr  26782  bclbnd  26783  bposlem9  26795  gausslemma2dlem1a  26868  gausslemma2dlem5  26874  lgseisenlem4  26881  lgsquadlem1  26883  m1lgs  26891  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2lgslem3d1  26906  2lgsoddprmlem1  26911  2sqlem8  26929  2sq2  26936  addsqn2reu  26944  addsqrexnreu  26945  addsqnreup  26946  addsq2nreurex  26947  chtppilim  26978  rpvmasumlem  26990  dchrisumlem1  26992  dchrisum0re  27016  dchrisum0lem2a  27020  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  2vmadivsumlem  27043  selberg4lem1  27063  pntrsumo1  27068  selberg34r  27074  pntrlog2bndlem2  27081  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntibndlem2  27094  pntlemg  27101  pntlemr  27105  pntlemf  27108  pntlemk  27109  pntlemo  27110  pntlem3  27112  ostth2lem2  27137  ttgcontlem1  28142  cusgrsize2inds  28710  wlklenvclwlk  28912  pthdadjvtx  28987  crctcshwlkn0lem1  29064  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  wlklnwwlkln2lem  29136  wlknwwlksnbij  29142  wwlksnred  29146  wwlksnext  29147  wwlksnextbi  29148  wwlksnredwwlkn  29149  wwlksnextwrd  29151  wwlksnextinj  29153  wwlksnextproplem2  29164  wwlksnextproplem3  29165  clwwlkccatlem  29242  clwlkclwwlklem2a1  29245  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwlkclwwlklem3  29254  clwlkclwwlk  29255  clwwisshclwwslemlem  29266  clwwisshclwws  29268  clwwlkel  29299  clwwlkf  29300  clwwlkwwlksb  29307  clwwlkext2edg  29309  wwlksext2clwwlk  29310  clwwlknonex2lem1  29360  clwwlknonex2lem2  29361  eucrct2eupth  29498  numclwwlk1lem2foalem  29604  numclwwlk1lem2fo  29611  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  numclwwlk6  29643  smcnlem  29950  fzm1ne1  32000  bcm1n  32006  fzom1ne1  32012  ltesubnnd  32028  wrdt2ind  32117  omndmul2  32230  psgnfzto1stlem  32259  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  archirngz  32335  archiabllem1a  32337  archiabllem2c  32341  freshmansdream  32381  ccfldextdgrr  32746  1smat1  32784  madjusmdetlem2  32808  madjusmdetlem4  32810  dya2icoseg  33276  iwrdsplit  33386  fibp1  33400  ballotlemfp1  33490  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemic  33505  ballotlem1c  33506  ballotlemsgt1  33509  ballotlemsdom  33510  ballotlemsel1i  33511  ballotlemsi  33513  ballotlemsima  33514  ballotlem1ri  33533  sgn0bi  33546  signstfvn  33580  signsvtn0  33581  signstfveq0  33588  signsvfn  33593  signsvtn  33595  signshf  33599  hashreprin  33632  circlemeth  33652  logdivsqrle  33662  revpfxsfxrev  34106  revwlk  34115  swrdwlk  34117  subfacp1lem1  34170  subfacp1lem5  34175  cvxpconn  34233  sinccvglem  34657  divcnvlin  34702  bcm1nt  34707  bcprod  34708  bccolsum  34709  iprodgam  34712  faclimlem1  34713  faclimlem2  34714  faclimlem3  34715  faclim  34716  iprodfac  34717  faclim2  34718  fwddifnp1  35137  gg-expcn  35164  gg-iihalf2cn  35168  gg-icchmeo  35170  gg-dvfsumle  35182  gg-dvfsumlem2  35183  dnizphlfeqhlf  35352  dnibndlem3  35356  dnibndlem13  35366  unblimceq0  35383  knoppndvlem6  35393  knoppndvlem9  35396  knoppndvlem14  35401  knoppndvlem15  35402  knoppndvlem16  35403  knoppndvlem17  35404  bj-bary1lem1  36192  irrdiff  36207  poimirlem25  36513  poimirlem26  36514  poimirlem32  36520  opnmbllem0  36524  itg2addnclem2  36540  dvasin  36572  dvacos  36573  areacirclem1  36576  areacirclem4  36579  areacirc  36581  bfp  36692  fzsplitnd  40848  lcmfunnnd  40877  lcmineqlem1  40894  lcmineqlem3  40896  lcmineqlem4  40897  lcmineqlem7  40900  lcmineqlem8  40901  lcmineqlem10  40903  lcmineqlem11  40904  lcmineqlem12  40905  lcmineqlem18  40911  lcmineqlem19  40912  lcmineqlem22  40915  lcmineqlem23  40916  dvrelogpow2b  40933  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  aks4d1p3  40943  aks4d1p7d1  40947  2np3bcnp1  40960  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  sticksstones16  40978  sticksstones22  40984  metakunt8  40992  metakunt12  40996  metakunt15  40999  metakunt16  41000  metakunt28  41012  nnadd1com  41181  nnaddcom  41182  nnadddir  41184  nnmul1com  41185  nnmulcom  41186  fz1sump1  41208  oddnumth  41209  nicomachus  41210  sumcubes  41211  reixi  41295  sn-mullid  41308  sn-0tie0  41312  renegmulnnass  41326  fltnltalem  41404  fltnlta  41405  3cubeslem1  41422  3cubeslem2  41423  3cubeslem4  41427  pell1qrge1  41608  rmspecfund  41647  acongeq  41722  jm2.18  41727  jm2.19lem3  41730  jm2.25  41738  jm2.16nn0  41743  jm3.1lem1  41756  jm3.1lem2  41757  areaquad  41965  relexpmulnn  42460  relexpaddss  42469  cvgdvgrat  43072  radcnvrat  43073  hashnzfzclim  43081  ofdivrec  43085  expgrowthi  43092  bccm1k  43101  dvradcnv2  43106  binomcxplemwb  43107  binomcxplemnn0  43108  binomcxplemrat  43109  binomcxplemfrat  43110  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  refsum2cnlem1  43721  fzisoeu  44010  fperiodmullem  44013  fzdifsuc2  44020  xralrple2  44064  nnsplit  44068  infleinflem2  44081  fmul01lt1lem2  44301  fprodcn  44316  clim1fr1  44317  isumneg  44318  climneg  44326  sumnnodd  44346  reclimc  44369  coseq0  44580  coskpi2  44582  cosknegpi  44585  fprodcncf  44616  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  dvnmul  44659  dvmptfprod  44661  dvnprodlem3  44664  itgsinexp  44671  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  stoweidlem1  44717  stoweidlem7  44723  stoweidlem10  44726  stoweidlem11  44727  stoweidlem14  44730  stoweidlem17  44733  stoweidlem34  44750  stoweidlem42  44758  wallispilem3  44783  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  wallispi2  44789  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem15  44804  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem11  44834  fourierdlem15  44838  fourierdlem26  44849  fourierdlem36  44859  fourierdlem40  44863  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem56  44878  fourierdlem58  44880  fourierdlem59  44881  fourierdlem62  44884  fourierdlem64  44886  fourierdlem65  44887  fourierdlem78  44900  fourierdlem79  44901  sqwvfoura  44944  fourierswlem  44946  fouriersw  44947  etransclem23  44973  etransclem24  44974  etransclem28  44978  etransclem35  44985  etransclem38  44988  nnfoctbdjlem  45171  smfmullem1  45507  sigaradd  45582  deccarry  46019  fargshiftf1  46109  fargshiftfo  46110  fmtnof1  46203  sqrtpwpw2p  46206  fmtnorec2lem  46210  fmtnorec4  46217  fmtnoprmfac1lem  46232  fmtnoprmfac1  46233  fmtnoprmfac2  46235  2pwp1prm  46257  mod42tp1mod8  46270  sfprmdvdsmersenne  46271  lighneallem3  46275  lighneallem4  46278  onego  46314  zofldiv2ALTV  46330  oexpnegALTV  46345  opoeALTV  46351  opeoALTV  46352  epee  46373  perfectALTVlem1  46389  fppr2odd  46399  fpprwppr  46407  0nodd  46580  2nodd  46582  nnsgrpnmnd  46588  pzriprnglem12  46816  1neven  46830  altgsumbc  47028  pw2m1lepw2m1  47201  m1modmmod  47207  zofldiv2  47217  nnpw2pmod  47269  blen1b  47274  blennn0em1  47277  dignn0flhalflem1  47301  dignn0flhalflem2  47302  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  nn0sumshdiglem2  47308  itcovalpclem2  47357  ackval1  47367  ackval2  47368  ackval3  47369  affineid  47390  1subrec1sub  47391  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  rrx2vlinest  47427