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

Theorem elfz2nn0 12469
Description: Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfz2nn0 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))

Proof of Theorem elfz2nn0
StepHypRef Expression
1 elnn0uz 11763 . . . 4 (𝐾 ∈ ℕ0𝐾 ∈ (ℤ‘0))
21anbi1i 731 . . 3 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) ↔ (𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ𝐾)))
3 eluznn0 11795 . . . . . 6 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) → 𝑁 ∈ ℕ0)
4 eluzle 11738 . . . . . . 7 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
54adantl 481 . . . . . 6 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) → 𝐾𝑁)
63, 5jca 553 . . . . 5 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) → (𝑁 ∈ ℕ0𝐾𝑁))
7 nn0z 11438 . . . . . . . 8 (𝐾 ∈ ℕ0𝐾 ∈ ℤ)
8 nn0z 11438 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
9 eluz 11739 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐾) ↔ 𝐾𝑁))
107, 8, 9syl2an 493 . . . . . . 7 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁 ∈ (ℤ𝐾) ↔ 𝐾𝑁))
1110biimprd 238 . . . . . 6 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐾𝑁𝑁 ∈ (ℤ𝐾)))
1211impr 648 . . . . 5 ((𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)) → 𝑁 ∈ (ℤ𝐾))
136, 12impbida 895 . . . 4 (𝐾 ∈ ℕ0 → (𝑁 ∈ (ℤ𝐾) ↔ (𝑁 ∈ ℕ0𝐾𝑁)))
1413pm5.32i 670 . . 3 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)))
152, 14bitr3i 266 . 2 ((𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ𝐾)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)))
16 elfzuzb 12374 . 2 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ𝐾)))
17 3anass 1059 . 2 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)))
1815, 16, 173bitr4i 292 1 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1054  wcel 2030   class class class wbr 4685  cfv 5926  (class class class)co 6690  0cc0 9974  cle 10113  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365
This theorem is referenced by:  elfznn0  12471  elfz3nn0  12472  0elfz  12475  fz0to3un2pr  12480  elfz0ubfz0  12482  elfz0fzfz0  12483  fz0fzelfz0  12484  uzsubfz0  12486  fz0fzdiffz0  12487  elfzmlbm  12488  elfzmlbp  12489  difelfzle  12491  difelfznle  12492  fvffz0  12496  fzofzim  12554  elfzodifsumelfzo  12573  elfzom1elp1fzo  12574  fzo0to42pr  12595  fzo0sn0fzo1  12597  elfznelfzo  12613  fvinim0ffz  12627  ssnn0fi  12824  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  fsuppmapnn0fiub0  12833  suppssfz  12834  1elfz0hash  13217  swrdn0  13476  swrdtrcfv  13487  swrdeq  13490  swrdlen2  13491  swrdfv2  13492  swrdswrdlem  13505  swrdswrd  13506  swrdccatwrd  13514  swrdccatin1  13529  swrdccatin12lem2b  13532  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccatin12  13537  swrdccat3  13538  swrdccat  13539  swrdccat3blem  13541  swrdccatid  13543  2cshwcshw  13617  cshwcshid  13619  cshwcsh2id  13620  swrds2  13731  prm23lt5  15566  psgnunilem2  17961  gsummoncoe1  19722  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  chfacfpmmulgsum2  20718  aannenlem2  24129  chtublem  24981  lgsquadlem2  25151  pntpbnd2  25321  usgrexmplef  26196  usgr2pthlem  26715  crctcshwlkn0lem4  26761  crctcshwlkn0lem7  26764  crctcshwlkn0  26769  wwlksm1edg  26835  wwlksnred  26855  wwlksnextproplem3  26874  erclwwlkref  26977  clwwlkf  27010  wwlksubclwwlk  27023  clwlksfclwwlk  27049  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  konigsberglem4  27233  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  bcm1n  29682  eulerpartlemd  30556  ballotth  30727  plymulx0  30752  poimirlem6  33545  poimirlem7  33546  poimirlem28  33567  nnubfi  33676  nninfnub  33677  irrapxlem1  37703  jm2.27a  37889  stoweidlem17  40552  elfz2z  41650  2elfz3nn0  41651  2elfz2melfz  41653  iccpartigtl  41684  iccpartlt  41685  pfxeq  41729  pfx2  41737  pfxccatin12lem1  41748  pfxccatin12lem2  41749  pfxccatin12  41750  pfxccat3  41751  pfxccat3a  41754  fmtnodvds  41781  fmtnole4prm  41815
  Copyright terms: Public domain W3C validator