Theorem 1cnd 11202

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11098  1c1 11101

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

This theorem is referenced by:  adddirp1d  11235  1p1times  11381  addcom  11396  addcomd  11412  muladd11r  11423  pncan1  11638  npcan1  11639  muls1d  11674  mulsubfacd  11675  recrec  11912  rec11  11913  rec11r  11914  rereccl  11933  subrecd  12044  nn1m1nn  12254  nnadd1com  12259  nnaddcom  12260  nnadddir  12292  nnmul1com  12293  nnmulcom  12294  add1p1  12495  sub1m1  12496  cnm2m1cnm3  12497  xp1d2m1eqxm1d2  12498  div4p1lem1div2  12499  nn0n0n1ge2  12572  zneo  12679  rpnnen1lem5  13005  lincmb01cmp  13522  iccf1o  13523  xov1plusxeqvd  13525  zpnn0elfzo1  13768  ubmelm1fzo  13792  fzosplitpr  13806  fzosplitprm1  13807  fzom1ne1  13814  fzoshftral  13816  fladdz  13858  2tnp1ge0ge0  13862  ltdifltdiv  13867  dfceil2  13872  negmod  13952  modnegd  13962  addmodlteq  13982  binom2sub1  14257  binom3  14260  zesq  14262  sqoddm1div8  14279  bcm1k  14351  bcp1n  14352  bcp1m1  14356  bcpasc  14357  bcn2m1  14360  hashfz  14464  hashfzo  14466  hashfzp1  14468  hashf1lem2  14493  hashf1  14494  hashdifsnp1  14543  lswccatn0lsw  14629  ccatws1lenp1b  14659  revccat  14803  repswrevw  14824  cshwidxm1  14844  cshwidxn  14846  cshweqrep  14858  cshimadifsn0  14867  swrds2m  14978  swrd2lsw  14989  relexpaddnn  15088  sgn0bi  15140  absexpz  15356  reccn2  15648  rlimno1  15705  isercolllem1  15716  isercoll2  15720  iseraltlem2  15734  iseraltlem3  15735  fsump1  15807  fsumconst1  15842  hashiun  15874  hash2iun1dif1  15876  indsumhash  15881  binomlem  15883  bcxmas  15889  incexc  15891  incexc2  15892  climcndslem1  15903  arisum  15914  arisum2  15915  trireciplem  15916  pwdif  15922  pwm1geoser  15923  geolim2  15925  georeclim  15926  mertenslem1  15938  prodfrec  15949  ntrivcvg  15951  ntrivcvgtail  15954  prodrblem  15983  prodmolem2a  15988  fprodntriv  15996  prod1  15998  fprodser  16003  fprodcl  16006  fprodm1  16021  fprodp1  16023  fprodclf  16046  risefacval2  16064  fallfacval2  16065  risefacp1  16083  fallfacp1  16084  risefacfac  16089  fallfacfwd  16090  binomfallfaclem2  16094  fallfacval4  16097  bpolydiflem  16108  ef0lem  16132  tanaddlem  16222  tanadd  16223  cos01bnd  16242  oddm1even  16401  oddp1even  16402  oexpneg  16403  ltoddhalfle  16419  halfleoddlt  16420  nn0ob  16442  pwp1fsum  16449  flodddiv4  16473  bitsp1o  16491  bitsf1  16504  sadcp1  16513  qredeu  16716  prmdiv  16844  prmdiveq  16845  vfermltlALT  16862  pc2dvds  16939  4sqlem11  17015  4sqlem12  17016  vdwapun  17034  vdwlem3  17043  vdwlem6  17046  vdwlem9  17049  ramub1lem2  17087  prmop1  17098  prmdvdsprmo  17102  prmgaplem8  17118  cshwshashnsame  17163  chnub  18678  chnlt  18679  chnccat  18682  chnrev  18683  gsumsgrpccat  18899  psgnunilem5  19564  psgnunilem2  19565  sylow1lem1  19668  efgredlemc  19815  odadd2  19919  ablsimpgfindlem1  20179  omndmul2  20203  srgbinomlem3  20310  srgbinomlem4  20311  cncrng  21512  gzrngunit  21552  zringunit  21585  prmirredlem  21591  pzriprnglem12  21611  freshmansdream  21693  mhppwdeg  22282  psdmul  22298  cayhamlem1  22992  expcn  25000  iirevcn  25058  iihalf2cn  25062  icchmeo  25069  icopnfcnv  25070  icopnfhmeo  25071  evth  25087  pcoass  25152  pjthlem1  25565  ovolunlem1a  25624  ovolunlem1  25625  opnmbllem  25729  mbfi1fseqlem6  25848  bddibl  25968  dvnadd  26057  dvmptid  26085  dvmptdiv  26102  dvcnvlem  26104  dveflem  26107  dvef  26108  dvsincos  26109  dvlipcn  26122  dvivthlem1  26136  lhop2  26143  dvcvx  26148  dvfsumle  26149  dvfsumabs  26151  dvfsumlem1  26154  dvfsumlem2  26155  itgpowd  26178  ply1divex  26263  fta1glem1  26294  dgrcolem1  26399  dgrcolem2  26400  vieta1lem1  26440  aaliou3lem2  26473  aaliou3lem8  26475  dvtaylp  26499  dvntaylp  26500  taylthlem1  26502  taylthlem2  26503  abelthlem1  26560  abelthlem2  26561  abelthlem6  26565  abelthlem7  26567  logdivlti  26751  advlog  26785  advlogexp  26786  logtayl  26791  cxpmul2  26820  dvcxp1  26871  dvcxp2  26872  dvcncxp1  26874  dvcnsqrt  26875  loglesqrt  26892  relogbdiv  26910  ang180lem4  26943  ang180lem5  26944  isosctrlem2  26950  isosctrlem3  26951  affineequiv  26954  affineequiv2  26955  affineequiv3  26956  angpieqvdlem  26959  chordthmlem2  26964  chordthmlem3  26965  chordthmlem5  26967  dcubic2  26975  dcubic  26977  quart1lem  26986  quart1  26987  quart  26992  asinlem  26999  asinlem3  27002  atansopn  27063  dvatan  27066  leibpi  27073  birthdaylem2  27083  efrlim  27100  cxplim  27102  divsqrtsumlem  27110  logdifbnd  27124  emcllem2  27127  emcllem3  27128  emcllem5  27130  zetacvg  27145  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamgulmlem4  27162  lgamgulmlem5  27163  lgamgulmlem6  27164  lgamgulm2  27166  lgamcvg2  27185  gamcvg  27186  gamcvg2lem  27189  lgam1  27194  gamfac  27197  wilthlem2  27199  wilthimp  27202  ftalem5  27207  basellem3  27213  basellem5  27215  basellem8  27218  basellem9  27219  sqff1o  27312  muinv  27323  logfaclbnd  27352  logfacrlim  27354  logexprlim  27355  perfectlem2  27360  dchr1cl  27381  dchrinvcl  27383  dchrfi  27385  dchr1  27387  dchrsum2  27398  bcmono  27407  bcp1ctr  27409  bclbnd  27410  bposlem9  27422  gausslemma2dlem1a  27495  gausslemma2dlem5  27501  lgseisenlem4  27508  lgsquadlem1  27510  m1lgs  27518  2lgslem3a  27526  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  2lgslem3d1  27533  2lgsoddprmlem1  27538  2sqlem8  27556  2sq2  27563  addsqn2reu  27571  addsqrexnreu  27572  addsqnreup  27573  addsq2nreurex  27574  chtppilim  27605  rpvmasumlem  27617  dchrisumlem1  27619  dchrisum0re  27643  dchrisum0lem2a  27647  mudivsum  27660  mulogsumlem  27661  mulogsum  27662  2vmadivsumlem  27670  selberg4lem1  27690  pntrsumo1  27695  selberg34r  27701  pntrlog2bndlem2  27708  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntrlog2bndlem6  27713  pntibndlem2  27721  pntlemg  27728  pntlemr  27732  pntlemf  27735  pntlemk  27736  pntlemo  27737  pntlem3  27739  ostth2lem2  27764  ttgcontlem1  29175  cusgrsize2inds  29744  wlklenvclwlk  29944  pthdadjvtx  30018  crctcshwlkn0lem1  30100  crctcshwlkn0lem4  30103  crctcshwlkn0lem5  30104  wlklnwwlkln2lem  30172  wlknwwlksnbij  30178  wwlksnred  30182  wwlksnext  30183  wwlksnextbi  30184  wwlksnredwwlkn  30185  wwlksnextwrd  30187  wwlksnextinj  30189  wwlksnextproplem2  30200  wwlksnextproplem3  30201  clwwlkccatlem  30281  clwlkclwwlklem2a1  30284  clwlkclwwlklem2a4  30289  clwlkclwwlklem2a  30290  clwlkclwwlklem2  30292  clwlkclwwlklem3  30293  clwlkclwwlk  30294  clwwisshclwwslemlem  30305  clwwisshclwws  30307  clwwlkel  30338  clwwlkf  30339  clwwlkwwlksb  30346  clwwlkext2edg  30348  wwlksext2clwwlk  30349  clwwlknonex2lem1  30399  clwwlknonex2lem2  30400  eucrct2eupth  30537  numclwwlk1lem2foalem  30643  numclwwlk1lem2fo  30650  numclwlk2lem2f  30669  numclwlk2lem2f1o  30671  numclwwlk6  30682  smcnlem  30990  receqid  33030  fzm1ne1  33074  bcm1n  33081  ltesubnnd  33108  oexpled  33121  wrdt2ind  33214  gsummptp1  33318  gsummulsubdishift1  33329  psgnfzto1stlem  33361  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  archirngz  33450  archiabllem1a  33452  archiabllem2c  33456  gsumind  33608  esplyind  33910  esplyindfv  33911  esplyfvn  33912  vietadeg1  33913  vietalem  33914  ccfldextdgrr  34007  constrfin  34081  nn0constr  34096  iconstr  34101  constrrecl  34104  constrimcl  34105  constrreinvcl  34107  constrinvcl  34108  constrresqrtcl  34112  2sqr3minply  34115  cos9thpiminplylem1  34117  cos9thpiminplylem2  34118  cos9thpiminplylem3  34119  cos9thpiminply  34123  cos9thpinconstrlem1  34124  1smat1  34139  madjusmdetlem2  34163  madjusmdetlem4  34165  dya2icoseg  34612  iwrdsplit  34722  fibp1  34736  ballotlemfp1  34827  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemic  34842  ballotlem1c  34843  ballotlemsgt1  34846  ballotlemsdom  34847  ballotlemsel1i  34848  ballotlemsi  34850  ballotlemsima  34851  ballotlem1ri  34870  signstfvn  34901  signsvtn0  34902  signstfveq0  34909  signsvfn  34914  signsvtn  34916  signshf  34920  hashreprin  34952  circlemeth  34972  logdivsqrle  34982  revpfxsfxrev  35506  revwlk  35516  swrdwlk  35518  subfacp1lem1  35570  subfacp1lem5  35575  cvxpconn  35633  sinccvglem  36063  divcnvlin  36124  bcm1nt  36128  bcprod  36129  bccolsum  36130  iprodgam  36133  faclimlem1  36134  faclimlem2  36135  faclimlem3  36136  faclim  36137  iprodfac  36138  faclim2  36139  fwddifnp1  36556  dnizphlfeqhlf  36954  dnibndlem3  36958  dnibndlem13  36968  unblimceq0  36985  knoppndvlem6  36995  knoppndvlem9  36998  knoppndvlem14  37003  knoppndvlem15  37004  knoppndvlem16  37005  knoppndvlem17  37006  bj-bary1lem1  37843  irrdiff  37858  qdiff  37859  poimirlem25  38184  poimirlem26  38185  poimirlem32  38191  opnmbllem0  38195  itg2addnclem2  38211  dvasin  38243  dvacos  38244  areacirclem1  38247  areacirclem4  38250  areacirc  38252  bfp  38363  fzsplitnd  42639  lcmfunnnd  42669  lcmineqlem1  42686  lcmineqlem3  42688  lcmineqlem4  42689  lcmineqlem7  42692  lcmineqlem8  42693  lcmineqlem10  42695  lcmineqlem11  42696  lcmineqlem12  42697  lcmineqlem18  42703  lcmineqlem19  42704  lcmineqlem22  42707  lcmineqlem23  42708  dvrelogpow2b  42725  aks4d1p1p4  42728  aks4d1p1p6  42730  aks4d1p1p7  42731  aks4d1p1p5  42732  aks4d1p1  42733  aks4d1p3  42735  aks4d1p7d1  42739  primrootsunit1  42754  posbezout  42757  primrootscoprbij  42759  primrootspoweq0  42763  aks6d1c1  42773  hashscontpow1  42778  2np3bcnp1  42801  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  sticksstones16  42819  sticksstones22  42825  aks6d1c6lem3  42829  aks6d1c7lem1  42837  unitscyglem5  42856  3rdpwhole  42943  fz1sump1  42961  oddnumth  42962  nicomachus  42963  sumcubes  42964  tan3rdpi  43003  redvmptabs  43011  readvrec  43013  reixi  43074  sn-mullid  43087  sn-0tie0  43115  renegmulnnass  43129  fiabv  43196  fltnltalem  43286  fltnlta  43287  3cubeslem1  43307  3cubeslem2  43308  3cubeslem4  43312  pell1qrge1  43489  rmspecfund  43528  acongeq  43602  jm2.18  43607  jm2.19lem3  43610  jm2.25  43618  jm2.16nn0  43623  jm3.1lem1  43636  jm3.1lem2  43637  areaquad  43835  relexpmulnn  44327  relexpaddss  44336  cvgdvgrat  44915  radcnvrat  44916  hashnzfzclim  44924  ofdivrec  44928  expgrowthi  44935  bccm1k  44944  dvradcnv2  44949  binomcxplemwb  44950  binomcxplemnn0  44951  binomcxplemrat  44952  binomcxplemfrat  44953  binomcxplemdvbinom  44955  binomcxplemnotnn0  44958  refsum2cnlem1  45649  fzisoeu  45911  fperiodmullem  45914  fzdifsuc2  45921  xralrple2  45962  nnsplit  45966  infleinflem2  45978  fmul01lt1lem2  46193  fprodcn  46208  clim1fr1  46209  isumneg  46210  climneg  46218  sumnnodd  46238  reclimc  46259  coseq0  46470  coskpi2  46472  cosknegpi  46475  fprodcncf  46506  fprodsubrecnncnvlem  46513  fprodaddrecnncnvlem  46515  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  dvnxpaek  46548  dvnmul  46549  dvmptfprod  46551  dvnprodlem3  46554  itgsinexp  46561  itgiccshift  46586  itgperiod  46587  itgsbtaddcnst  46588  stoweidlem1  46607  stoweidlem7  46613  stoweidlem10  46616  stoweidlem11  46617  stoweidlem14  46620  stoweidlem17  46623  stoweidlem34  46640  stoweidlem42  46648  wallispilem3  46673  wallispilem5  46675  wallispi  46676  wallispi2lem1  46677  wallispi2lem2  46678  wallispi2  46679  stirlinglem1  46680  stirlinglem3  46682  stirlinglem4  46683  stirlinglem5  46684  stirlinglem6  46685  stirlinglem7  46686  stirlinglem8  46687  stirlinglem10  46689  stirlinglem11  46690  stirlinglem12  46691  stirlinglem13  46692  stirlinglem15  46694  dirkertrigeqlem2  46705  dirkertrigeqlem3  46706  dirkertrigeq  46707  dirkercncflem1  46709  dirkercncflem2  46710  dirkercncflem4  46712  fourierdlem11  46724  fourierdlem15  46728  fourierdlem26  46739  fourierdlem36  46749  fourierdlem40  46753  fourierdlem41  46754  fourierdlem42  46755  fourierdlem48  46760  fourierdlem49  46761  fourierdlem56  46768  fourierdlem58  46770  fourierdlem59  46771  fourierdlem62  46774  fourierdlem64  46776  fourierdlem65  46777  fourierdlem78  46790  fourierdlem79  46791  sqwvfoura  46834  fourierswlem  46836  fouriersw  46837  etransclem23  46863  etransclem24  46864  etransclem28  46868  etransclem35  46875  etransclem38  46878  nnfoctbdjlem  47061  smfmullem1  47397  sigaradd  47472  chnerlem2  47491  sin3t  47497  cos3t  47498  sin5tlem1  47499  sin5tlem2  47500  sin5tlem4  47502  cos5t  47505  cjnpoly  47515  deccarry  47937  ceilbi  47963  flmrecm1  47969  m1modne  47980  m1modmmod  47990  modm1nep2  48000  modm1nem2  48001  fargshiftf1  48079  fargshiftfo  48080  fmtnof1  48176  sqrtpwpw2p  48179  fmtnorec2lem  48183  fmtnorec4  48190  fmtnoprmfac1lem  48205  fmtnoprmfac1  48206  fmtnoprmfac2  48208  2pwp1prm  48230  mod42tp1mod8  48243  sfprmdvdsmersenne  48244  lighneallem3  48248  lighneallem4  48251  ppivalnnprm  48266  ppivalnnnprmge6  48267  onego  48300  zofldiv2ALTV  48316  oexpnegALTV  48331  opoeALTV  48337  opeoALTV  48338  epee  48359  perfectALTVlem1  48375  fppr2odd  48385  fpprwppr  48393  gpg3nbgrvtx0  48730  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  0nodd  48824  2nodd  48826  nnsgrpnmnd  48832  1neven  48892  altgsumbc  49017  pw2m1lepw2m1  49185  zofldiv2  49196  nnpw2pmod  49248  blen1b  49253  blennn0em1  49256  dignn0flhalflem1  49280  dignn0flhalflem2  49281  nn0sumshdiglemB  49285  nn0sumshdiglem1  49286  nn0sumshdiglem2  49287  itcovalpclem2  49336  ackval1  49346  ackval2  49347  ackval3  49348  affineid  49369  1subrec1sub  49370  eenglngeehlnmlem1  49402  eenglngeehlnmlem2  49403  rrx2vlinest  49406