Theorem elfzuzb 13232

Description: Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuzb	⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))

Proof of Theorem elfzuzb

Step	Hyp	Ref	Expression
1		df-3an 1087	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
2		an6 1443	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
3		df-3an 1087	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ))
4		anandir 673	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)))
5		an43 654	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6	3, 4, 5	3bitri 296	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
7	6	anbi1i 623	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
8	1, 2, 7	3bitr4ri 303	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁)))
9		elfz2 13228	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
10		eluz2 12570	. . 3 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾))
11		eluz2 12570	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁))
12	10, 11	anbi12i 626	. 2 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁)))
13	8, 9, 12	3bitr4i 302	1 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2109   class class class wbr 5078  ‘cfv 6430  (class class class)co 7268   ≤ cle 10994  ℤcz 12302  ℤ_≥cuz 12564  ...cfz 13221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-cnex 10911  ax-resscn 10912

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-fv 6438  df-ov 7271  df-oprab 7272  df-mpo 7273  df-1st 7817  df-2nd 7818  df-neg 11191  df-z 12303  df-uz 12565  df-fz 13222

This theorem is referenced by:  eluzfz  13233  elfzuz  13234  elfzuz3  13235  elfzuz2  13243  peano2fzr  13251  fzsplit2  13263  fzass4  13276  fzss1  13277  fzss2  13278  fzp1elp1  13291  fznn  13306  elfz2nn0  13329  elfzofz  13384  fzosplitsnm1  13443  fzofzp1b  13466  fzosplitsn  13476  seqcl2  13722  seqfveq2  13726  monoord  13734  seqid2  13750  bcn1  14008  fz1isolem  14156  seqcoll  14159  ccatrn  14275  swrds1  14360  swrdccat2  14363  spllen  14448  splfv2a  14450  splval2  14451  caubnd  15051  isercolllem2  15358  isercolllem3  15359  summolem2a  15408  fsum0diag2  15476  climcndslem1  15542  mertenslem1  15577  prodmolem2a  15625  vdwlem2  16664  vdwlem8  16670  gexcl3  19173  efginvrel2  19314  efgredleme  19330  efgcpbllemb  19342  1stckgenlem  22685  imasdsf1olem  23507  iscmet3lem1  24436  dvtaylp  25510  mtest  25544  ppisval  26234  ppisval2  26235  chtdif  26288  ppidif  26293  logfaclbnd  26351  bposlem4  26416  dchrisumlem2  26619  pntpbnd1  26715  fzsplit3  31094  mettrifi  35894  monoordxrv  42976  smonoord  44775