MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1cnd Structured version   Visualization version   GIF version

Theorem 1cnd 11151
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
StepHypRef Expression
1 ax-1cn 11110 . 2 1 ∈ ℂ
21a1i 11 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 11050  1c1 11053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 11110
This theorem is referenced by:  adddirp1d  11182  1p1times  11327  addcom  11342  addcomd  11358  muladd11r  11369  pncan1  11580  npcan1  11581  muls1d  11616  mulsubfacd  11617  recrec  11853  rec11  11854  rec11r  11855  rereccl  11874  subrec  11985  nn1m1nn  12175  add1p1  12405  sub1m1  12406  cnm2m1cnm3  12407  xp1d2m1eqxm1d2  12408  div4p1lem1div2  12409  nn0n0n1ge2  12481  zneo  12587  rpnnen1lem5  12907  lincmb01cmp  13413  iccf1o  13414  xov1plusxeqvd  13416  zpnn0elfzo1  13647  ubmelm1fzo  13669  fzosplitpr  13682  fzosplitprm1  13683  fzoshftral  13690  fladdz  13731  2tnp1ge0ge0  13735  ltdifltdiv  13740  dfceil2  13745  negmod  13822  modnegd  13832  addmodlteq  13852  binom2sub1  14125  binom3  14128  zesq  14130  sqoddm1div8  14147  bcm1k  14216  bcp1n  14217  bcp1m1  14221  bcpasc  14222  bcn2m1  14225  hashfz  14328  hashfzo  14330  hashfzp1  14332  hashf1lem2  14356  hashf1  14357  hashdifsnp1  14396  lswccatn0lsw  14480  ccatws1lenp1b  14510  revccat  14655  repswrevw  14676  cshwidxm1  14696  cshwidxn  14698  cshweqrep  14710  cshimadifsn0  14720  swrds2m  14831  swrd2lsw  14842  relexpaddnn  14937  absexpz  15191  reccn2  15480  rlimno1  15539  isercolllem1  15550  isercoll2  15554  iseraltlem2  15568  iseraltlem3  15569  hashiun  15708  hash2iun1dif1  15710  binomlem  15715  bcxmas  15721  incexc  15723  incexc2  15724  climcndslem1  15735  arisum  15746  arisum2  15747  trireciplem  15748  pwdif  15754  pwm1geoser  15755  geolim2  15757  georeclim  15758  mertenslem1  15770  prodfrec  15781  ntrivcvg  15783  ntrivcvgtail  15786  prodrblem  15813  prodmolem2a  15818  fprodntriv  15826  prod1  15828  fprodser  15833  fprodcl  15836  fprodm1  15851  fprodp1  15853  fprodclf  15876  risefacval2  15894  fallfacval2  15895  risefacp1  15913  fallfacp1  15914  risefacfac  15919  fallfacfwd  15920  binomfallfaclem2  15924  fallfacval4  15927  bpolydiflem  15938  ef0lem  15962  tanaddlem  16049  tanadd  16050  cos01bnd  16069  oddm1even  16226  oddp1even  16227  oexpneg  16228  ltoddhalfle  16244  halfleoddlt  16245  nn0ob  16267  pwp1fsum  16274  flodddiv4  16296  bitsp1o  16314  bitsf1  16327  sadcp1  16336  qredeu  16535  prmdiv  16658  prmdiveq  16659  vfermltlALT  16675  pc2dvds  16752  4sqlem11  16828  4sqlem12  16829  vdwapun  16847  vdwlem3  16856  vdwlem6  16859  vdwlem9  16862  ramub1lem2  16900  prmop1  16911  prmdvdsprmo  16915  prmgaplem8  16931  cshwshashnsame  16977  gsumsgrpccat  18651  psgnunilem5  19277  psgnunilem2  19278  sylow1lem1  19381  efgredlemc  19528  odadd2  19628  ablsimpgfindlem1  19887  srgbinomlem3  19960  srgbinomlem4  19961  cncrng  20821  gzrngunit  20866  zringunit  20890  prmirredlem  20896  mhppwdeg  21543  cayhamlem1  22218  expcn  24238  iirevcn  24296  iihalf2cn  24300  icchmeo  24307  icopnfcnv  24308  icopnfhmeo  24309  evth  24325  pcoass  24390  pjthlem1  24804  ovolunlem1a  24863  ovolunlem1  24864  opnmbllem  24968  mbfi1fseqlem6  25088  bddibl  25207  dvnadd  25296  dvmptid  25324  dvmptdiv  25341  dvcnvlem  25343  dveflem  25346  dvef  25347  dvsincos  25348  dvlipcn  25361  dvivthlem1  25375  lhop2  25382  dvcvx  25387  dvfsumle  25388  dvfsumabs  25390  dvfsumlem1  25393  dvfsumlem2  25394  itgpowd  25417  ply1divex  25504  fta1glem1  25533  dgrcolem1  25637  dgrcolem2  25638  vieta1lem1  25673  aaliou3lem2  25706  aaliou3lem8  25708  dvtaylp  25732  dvntaylp  25733  taylthlem1  25735  taylthlem2  25736  abelthlem1  25793  abelthlem2  25794  abelthlem6  25798  abelthlem7  25800  logdivlti  25978  advlog  26012  advlogexp  26013  logtayl  26018  cxpmul2  26047  dvcxp1  26096  dvcxp2  26097  dvcncxp1  26099  dvcnsqrt  26100  loglesqrt  26114  relogbdiv  26132  ang180lem4  26165  ang180lem5  26166  isosctrlem2  26172  isosctrlem3  26173  affineequiv  26176  affineequiv2  26177  affineequiv3  26178  angpieqvdlem  26181  chordthmlem2  26186  chordthmlem3  26187  chordthmlem5  26189  dcubic2  26197  dcubic  26199  quart1lem  26208  quart1  26209  quart  26214  asinlem  26221  asinlem3  26224  atansopn  26285  dvatan  26288  leibpi  26295  birthdaylem2  26305  efrlim  26322  cxplim  26324  divsqrtsumlem  26332  logdifbnd  26346  emcllem2  26349  emcllem3  26350  emcllem5  26352  zetacvg  26367  lgamgulmlem2  26382  lgamgulmlem3  26383  lgamgulmlem4  26384  lgamgulmlem5  26385  lgamgulmlem6  26386  lgamgulm2  26388  lgamcvg2  26407  gamcvg  26408  gamcvg2lem  26411  lgam1  26416  gamfac  26419  wilthlem2  26421  wilthimp  26424  ftalem5  26429  basellem3  26435  basellem5  26437  basellem8  26440  basellem9  26441  sqff1o  26534  muinv  26545  logfaclbnd  26573  logfacrlim  26575  logexprlim  26576  perfectlem2  26581  dchr1cl  26602  dchrinvcl  26604  dchrfi  26606  dchr1  26608  dchrsum2  26619  bcmono  26628  bcp1ctr  26630  bclbnd  26631  bposlem9  26643  gausslemma2dlem1a  26716  gausslemma2dlem5  26722  lgseisenlem4  26729  lgsquadlem1  26731  m1lgs  26739  2lgslem3a  26747  2lgslem3b  26748  2lgslem3c  26749  2lgslem3d  26750  2lgslem3d1  26754  2lgsoddprmlem1  26759  2sqlem8  26777  2sq2  26784  addsqn2reu  26792  addsqrexnreu  26793  addsqnreup  26794  addsq2nreurex  26795  chtppilim  26826  rpvmasumlem  26838  dchrisumlem1  26840  dchrisum0re  26864  dchrisum0lem2a  26868  mudivsum  26881  mulogsumlem  26882  mulogsum  26883  2vmadivsumlem  26891  selberg4lem1  26911  pntrsumo1  26916  selberg34r  26922  pntrlog2bndlem2  26929  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntrlog2bndlem6  26934  pntibndlem2  26942  pntlemg  26949  pntlemr  26953  pntlemf  26956  pntlemk  26957  pntlemo  26958  pntlem3  26960  ostth2lem2  26985  ttgcontlem1  27836  cusgrsize2inds  28404  wlklenvclwlk  28606  pthdadjvtx  28681  crctcshwlkn0lem1  28758  crctcshwlkn0lem4  28761  crctcshwlkn0lem5  28762  wlklnwwlkln2lem  28830  wlknwwlksnbij  28836  wwlksnred  28840  wwlksnext  28841  wwlksnextbi  28842  wwlksnredwwlkn  28843  wwlksnextwrd  28845  wwlksnextinj  28847  wwlksnextproplem2  28858  wwlksnextproplem3  28859  clwwlkccatlem  28936  clwlkclwwlklem2a1  28939  clwlkclwwlklem2a4  28944  clwlkclwwlklem2a  28945  clwlkclwwlklem2  28947  clwlkclwwlklem3  28948  clwlkclwwlk  28949  clwwisshclwwslemlem  28960  clwwisshclwws  28962  clwwlkel  28993  clwwlkf  28994  clwwlkwwlksb  29001  clwwlkext2edg  29003  wwlksext2clwwlk  29004  clwwlknonex2lem1  29054  clwwlknonex2lem2  29055  eucrct2eupth  29192  numclwwlk1lem2foalem  29298  numclwwlk1lem2fo  29305  numclwlk2lem2f  29324  numclwlk2lem2f1o  29326  numclwwlk6  29337  smcnlem  29642  fzm1ne1  31695  bcm1n  31701  fzom1ne1  31707  ltesubnnd  31721  wrdt2ind  31810  omndmul2  31923  psgnfzto1stlem  31952  cycpmco2lem3  31980  cycpmco2lem4  31981  cycpmco2lem5  31982  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmco2  31985  archirngz  32028  archiabllem1a  32030  archiabllem2c  32034  freshmansdream  32070  ccfldextdgrr  32359  1smat1  32388  madjusmdetlem2  32412  madjusmdetlem4  32414  dya2icoseg  32880  iwrdsplit  32990  fibp1  33004  ballotlemfp1  33094  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemic  33109  ballotlem1c  33110  ballotlemsgt1  33113  ballotlemsdom  33114  ballotlemsel1i  33115  ballotlemsi  33117  ballotlemsima  33118  ballotlem1ri  33137  sgn0bi  33150  signstfvn  33184  signsvtn0  33185  signstfveq0  33192  signsvfn  33197  signsvtn  33199  signshf  33203  hashreprin  33236  circlemeth  33256  logdivsqrle  33266  revpfxsfxrev  33712  revwlk  33721  swrdwlk  33723  subfacp1lem1  33776  subfacp1lem5  33781  cvxpconn  33839  sinccvglem  34263  divcnvlin  34308  bcm1nt  34313  bcprod  34314  bccolsum  34315  iprodgam  34318  faclimlem1  34319  faclimlem2  34320  faclimlem3  34321  faclim  34322  iprodfac  34323  faclim2  34324  fwddifnp1  34753  dnizphlfeqhlf  34942  dnibndlem3  34946  dnibndlem13  34956  unblimceq0  34973  knoppndvlem6  34983  knoppndvlem9  34986  knoppndvlem14  34991  knoppndvlem15  34992  knoppndvlem16  34993  knoppndvlem17  34994  bj-bary1lem1  35785  irrdiff  35800  poimirlem25  36106  poimirlem26  36107  poimirlem32  36113  opnmbllem0  36117  itg2addnclem2  36133  dvasin  36165  dvacos  36166  areacirclem1  36169  areacirclem4  36172  areacirc  36174  bfp  36286  fzsplitnd  40443  lcmfunnnd  40472  lcmineqlem1  40489  lcmineqlem3  40491  lcmineqlem4  40492  lcmineqlem7  40495  lcmineqlem8  40496  lcmineqlem10  40498  lcmineqlem11  40499  lcmineqlem12  40500  lcmineqlem18  40506  lcmineqlem19  40507  lcmineqlem22  40510  lcmineqlem23  40511  dvrelogpow2b  40528  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p3  40538  aks4d1p7d1  40542  2np3bcnp1  40555  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  sticksstones16  40573  sticksstones22  40579  metakunt8  40587  metakunt12  40591  metakunt15  40594  metakunt16  40595  metakunt28  40607  nnadd1com  40786  nnaddcom  40787  nnadddir  40789  nnmul1com  40790  nnmulcom  40791  reixi  40894  sn-mulid2  40907  sn-0tie0  40911  renegmulnnass  40925  fltnltalem  41003  fltnlta  41004  3cubeslem1  41010  3cubeslem2  41011  3cubeslem4  41015  pell1qrge1  41196  rmspecfund  41235  acongeq  41310  jm2.18  41315  jm2.19lem3  41318  jm2.25  41326  jm2.16nn0  41331  jm3.1lem1  41344  jm3.1lem2  41345  areaquad  41553  relexpmulnn  41988  relexpaddss  41997  cvgdvgrat  42600  radcnvrat  42601  hashnzfzclim  42609  ofdivrec  42613  expgrowthi  42620  bccm1k  42629  dvradcnv2  42634  binomcxplemwb  42635  binomcxplemnn0  42636  binomcxplemrat  42637  binomcxplemfrat  42638  binomcxplemdvbinom  42640  binomcxplemnotnn0  42643  refsum2cnlem1  43249  fzisoeu  43541  fperiodmullem  43544  fzdifsuc2  43551  xralrple2  43595  nnsplit  43599  infleinflem2  43612  fmul01lt1lem2  43833  fprodcn  43848  clim1fr1  43849  isumneg  43850  climneg  43858  sumnnodd  43878  reclimc  43901  coseq0  44112  coskpi2  44114  cosknegpi  44117  fprodcncf  44148  fprodsubrecnncnvlem  44155  fprodaddrecnncnvlem  44157  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvnxpaek  44190  dvnmul  44191  dvmptfprod  44193  dvnprodlem3  44196  itgsinexp  44203  itgiccshift  44228  itgperiod  44229  itgsbtaddcnst  44230  stoweidlem1  44249  stoweidlem7  44255  stoweidlem10  44258  stoweidlem11  44259  stoweidlem14  44262  stoweidlem17  44265  stoweidlem34  44282  stoweidlem42  44290  wallispilem3  44315  wallispilem5  44317  wallispi  44318  wallispi2lem1  44319  wallispi2lem2  44320  wallispi2  44321  stirlinglem1  44322  stirlinglem3  44324  stirlinglem4  44325  stirlinglem5  44326  stirlinglem6  44327  stirlinglem7  44328  stirlinglem8  44329  stirlinglem10  44331  stirlinglem11  44332  stirlinglem12  44333  stirlinglem13  44334  stirlinglem15  44336  dirkertrigeqlem2  44347  dirkertrigeqlem3  44348  dirkertrigeq  44349  dirkercncflem1  44351  dirkercncflem2  44352  dirkercncflem4  44354  fourierdlem11  44366  fourierdlem15  44370  fourierdlem26  44381  fourierdlem36  44391  fourierdlem40  44395  fourierdlem41  44396  fourierdlem42  44397  fourierdlem48  44402  fourierdlem49  44403  fourierdlem56  44410  fourierdlem58  44412  fourierdlem59  44413  fourierdlem62  44416  fourierdlem64  44418  fourierdlem65  44419  fourierdlem78  44432  fourierdlem79  44433  sqwvfoura  44476  fourierswlem  44478  fouriersw  44479  etransclem23  44505  etransclem24  44506  etransclem28  44510  etransclem35  44517  etransclem38  44520  nnfoctbdjlem  44703  smfmullem1  45039  sigaradd  45114  deccarry  45550  fargshiftf1  45640  fargshiftfo  45641  fmtnof1  45734  sqrtpwpw2p  45737  fmtnorec2lem  45741  fmtnorec4  45748  fmtnoprmfac1lem  45763  fmtnoprmfac1  45764  fmtnoprmfac2  45766  2pwp1prm  45788  mod42tp1mod8  45801  sfprmdvdsmersenne  45802  lighneallem3  45806  lighneallem4  45809  onego  45845  zofldiv2ALTV  45861  oexpnegALTV  45876  opoeALTV  45882  opeoALTV  45883  epee  45904  perfectALTVlem1  45920  fppr2odd  45930  fpprwppr  45938  0nodd  46111  2nodd  46113  nnsgrpnmnd  46119  1neven  46237  altgsumbc  46435  pw2m1lepw2m1  46608  m1modmmod  46614  zofldiv2  46624  nnpw2pmod  46676  blen1b  46681  blennn0em1  46684  dignn0flhalflem1  46708  dignn0flhalflem2  46709  nn0sumshdiglemB  46713  nn0sumshdiglem1  46714  nn0sumshdiglem2  46715  itcovalpclem2  46764  ackval1  46774  ackval2  46775  ackval3  46776  affineid  46797  1subrec1sub  46798  eenglngeehlnmlem1  46830  eenglngeehlnmlem2  46831  rrx2vlinest  46834
  Copyright terms: Public domain W3C validator