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

Theorem elfz2nn0 12168
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 11465 . . . 4 (𝐾 ∈ ℕ0𝐾 ∈ (ℤ‘0))
21anbi1i 726 . . 3 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) ↔ (𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ𝐾)))
3 eluznn0 11497 . . . . . 6 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) → 𝑁 ∈ ℕ0)
4 eluzle 11440 . . . . . . 7 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
54adantl 480 . . . . . 6 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) → 𝐾𝑁)
63, 5jca 552 . . . . 5 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) → (𝑁 ∈ ℕ0𝐾𝑁))
7 nn0z 11141 . . . . . . . 8 (𝐾 ∈ ℕ0𝐾 ∈ ℤ)
8 nn0z 11141 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
9 eluz 11441 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐾) ↔ 𝐾𝑁))
107, 8, 9syl2an 492 . . . . . . 7 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁 ∈ (ℤ𝐾) ↔ 𝐾𝑁))
1110biimprd 236 . . . . . 6 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐾𝑁𝑁 ∈ (ℤ𝐾)))
1211impr 646 . . . . 5 ((𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)) → 𝑁 ∈ (ℤ𝐾))
136, 12impbida 872 . . . 4 (𝐾 ∈ ℕ0 → (𝑁 ∈ (ℤ𝐾) ↔ (𝑁 ∈ ℕ0𝐾𝑁)))
1413pm5.32i 666 . . 3 ((𝐾 ∈ ℕ0𝑁 ∈ (ℤ𝐾)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)))
152, 14bitr3i 264 . 2 ((𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ𝐾)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)))
16 elfzuzb 12075 . 2 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ𝐾)))
17 3anass 1034 . 2 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0𝐾𝑁)))
1815, 16, 173bitr4i 290 1 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  w3a 1030  wcel 1938   class class class wbr 4481  cfv 5689  (class class class)co 6426  0cc0 9691  cle 9830  0cn0 11047  cz 11118  cuz 11427  ...cfz 12065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-om 6834  df-1st 6934  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-er 7505  df-en 7718  df-dom 7719  df-sdom 7720  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-nn 10776  df-n0 11048  df-z 11119  df-uz 11428  df-fz 12066
This theorem is referenced by:  elfznn0  12170  elfz3nn0  12171  0elfz  12173  fz0to3un2pr  12178  elfz0ubfz0  12180  elfz0fzfz0  12181  fz0fzelfz0  12182  uzsubfz0  12184  fz0fzdiffz0  12185  elfzmlbm  12186  elfzmlbp  12187  difelfzle  12189  difelfznle  12190  fvffz0  12194  fzofzim  12250  elfzodifsumelfzo  12269  elfzom1elp1fzo  12270  fzo0to42pr  12290  fzo0sn0fzo1  12292  elfznelfzo  12307  fvinim0ffz  12317  ssnn0fi  12514  fsuppmapnn0fiub  12520  fsuppmapnn0fiubOLD  12521  fsuppmapnn0fiub0  12523  suppssfz  12524  1elfz0hash  12905  swrdn0  13141  swrdtrcfv  13152  swrdeq  13155  swrdlen2  13156  swrdfv2  13157  swrdswrdlem  13170  swrdswrd  13171  swrdccatwrd  13179  swrdccatin1  13193  swrdccatin12lem2b  13196  swrdccatin12lem2  13199  swrdccatin12lem3  13200  swrdccatin12  13201  swrdccat3  13202  swrdccat  13203  swrdccat3blem  13205  swrdccatid  13207  2cshwcshw  13281  cshwcshid  13283  cshwcsh2id  13284  swrds2  13392  prm23lt5  15241  psgnunilem2  17630  gsummoncoe1  19399  mp2pm2mplem4  20336  chfacfisf  20381  chfacfisfcpmat  20382  chfacfpmmulgsum2  20392  aannenlem2  23775  chtublem  24625  lgsquadlem2  24795  pntpbnd2  24965  usgraex0elv  25662  usgraex1elv  25663  usgraex2elv  25664  usgraex3elv  25665  wlkonwlk  25803  cyclnspth  25897  wwlknred  25989  wwlkm1edg  26001  wwlkextproplem3  26009  clwwlkf  26060  wwlksubclwwlk  26070  erclwwlkref  26079  clwlkfclwwlk1hash  26107  clwlkfclwwlk  26109  numclwlk2lem2f  26368  bcm1n  28736  eulerpartlemd  29562  ballotth  29733  ballotthOLD  29771  plymulx0  29795  poimirlem6  32475  poimirlem7  32476  poimirlem28  32497  nnubfi  32606  nninfnub  32607  irrapxlem1  36294  jm2.27a  36480  stoweidlem17  38813  iccpartigtl  39869  iccpartlt  39870  fmtnodvds  39902  fmtnole4prm  39936  pfxeq  40175  pfx2  40183  pfxccatin12lem1  40194  pfxccatin12lem2  40195  pfxccatin12  40196  pfxccat3  40197  pfxccat3a  40200  elfz2z  40282  2elfz3nn0  40283  2elfz2melfz  40285  usgr2pthlem  41074  crctcsh1wlkn0lem4  41121  crctcsh1wlkn0lem7  41124  crctcsh1wlkn0  41129  wwlksm1edg  41183  wwlksnred  41203  wwlksnextproplem3  41222  clwwlksf  41327  wwlksubclwwlks  41337  erclwwlksref  41346  clwlksfclwwlk  41374  upgr4cycl4dv4e  41457  konigsbergiedgw  41521  konigsbergiedgwOLD  41522  konigsberglem1  41527  konigsberglem2  41528  konigsberglem3  41529  konigsberglem4  41530  av-numclwlk2lem2f  41638
  Copyright terms: Public domain W3C validator