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

Theorem elfz2 12883
Description: Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show 𝑀 ∈ ℤ and 𝑁 ∈ ℤ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfz2 (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀𝐾𝐾𝑁)))

Proof of Theorem elfz2
StepHypRef Expression
1 anass 471 . 2 ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀𝐾𝐾𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁))))
2 df-3an 1085 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ))
32anbi1i 625 . 2 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀𝐾𝐾𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀𝐾𝐾𝑁)))
4 elfz1 12881 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁)))
5 3anass 1091 . . . . 5 ((𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁) ↔ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))
6 ibar 531 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))))
75, 6syl5bb 285 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))))
84, 7bitrd 281 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))))
9 fzf 12880 . . . . . . 7 ...:(ℤ × ℤ)⟶𝒫 ℤ
109fdmi 6500 . . . . . 6 dom ... = (ℤ × ℤ)
1110ndmov 7310 . . . . 5 (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ∅)
1211eleq2d 2896 . . . 4 (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ∈ ∅))
13 noel 4273 . . . . . 6 ¬ 𝐾 ∈ ∅
1413pm2.21i 119 . . . . 5 (𝐾 ∈ ∅ → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
15 simpl 485 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
1614, 15pm5.21ni 381 . . . 4 (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ ∅ ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))))
1712, 16bitrd 281 . . 3 (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))))
188, 17pm2.61i 184 . 2 (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁))))
191, 3, 183bitr4ri 306 1 (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀𝐾𝐾𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208  wa 398  w3a 1083  wcel 2114  c0 4269  𝒫 cpw 4515   class class class wbr 5042   × cxp 5529  (class class class)co 7133  cle 10654  cz 11960  ...cfz 12876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-1st 7667  df-2nd 7668  df-neg 10851  df-z 11961  df-fz 12877
This theorem is referenced by:  elfz4  12885  elfzuzb  12886  0nelfz1  12910  uzsubsubfz  12913  fzmmmeqm  12924  ssfzunsnext  12936  fzpreddisj  12940  elfz1b  12960  fzp1nel  12975  elfz0ubfz0  12995  elfz0fzfz0  12996  fz0fzelfz0  12997  fz0fzdiffz0  13000  elfzmlbp  13002  preduz  13013  fzoun  13058  fzind2  13139  swrdswrdlem  14046  swrdswrd  14047  pfxccatin12lem2a  14069  pfxccatin12lem1  14070  swrdccatin2  14071  pfxccatin12lem2  14073  pfxccat3  14076  2cshwcshw  14167  cshwcsh2id  14170  fprodntriv  15276  fprodeq0  15309  prmgaplem4  16368  chfacfscmulgsum  21444  chfacfpmmulgsum  21448  gausslemma2dlem3  25931  2lgslem1a1  25952  crctcshwlkn0lem3  27577  wwlksnextproplem2  27675  wrdt2ind  30614  lcmineqlem18  39198  monoords  41718  uzfissfz  41748  iuneqfzuzlem  41756  ssuzfz  41771  elfzd  41837  fmul01lt1lem1  42017  fmul01lt1lem2  42018  mccllem  42030  sumnnodd  42063  dvnmul  42376  dvnprodlem1  42379  dvnprodlem2  42380  itgspltprt  42412  stoweidlem3  42436  stoweidlem34  42467  stoweidlem51  42484  fourierdlem12  42552  fourierdlem14  42554  fourierdlem41  42581  fourierdlem48  42587  fourierdlem49  42588  fourierdlem50  42589  fourierdlem79  42618  fourierdlem92  42631  fourierdlem93  42632  elaa2lem  42666  etransclem3  42670  etransclem7  42674  etransclem10  42677  etransclem24  42691  etransclem27  42694  etransclem28  42695  etransclem35  42702  etransclem38  42705  etransclem44  42711  iundjiun  42890  caratheodorylem1  42956  elfzelfzlble  43669  iccpartiltu  43730  31prm  43906  nnsum4primeseven  44110  nnsum4primesevenALTV  44111
  Copyright terms: Public domain W3C validator