Theorem elfzuzb 13486

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 1088	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
2		an6 1447	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
3		df-3an 1088	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ))
4		anandir 677	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)))
5		an43 658	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6	3, 4, 5	3bitri 297	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
7	6	anbi1i 624	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
8	1, 2, 7	3bitr4ri 304	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁)))
9		elfz2 13482	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
10		eluz2 12806	. . 3 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾))
11		eluz2 12806	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁))
12	10, 11	anbi12i 628	. 2 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) ∧ (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁)))
13	8, 9, 12	3bitr4i 303	1 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5110  ‘cfv 6514  (class class class)co 7390   ≤ cle 11216  ℤcz 12536  ℤ_≥cuz 12800  ...cfz 13475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-neg 11415  df-z 12537  df-uz 12801  df-fz 13476

This theorem is referenced by:  eluzfz  13487  elfzuz  13488  elfzuz3  13489  elfzuz2  13497  peano2fzr  13505  fzsplit2  13517  fzass4  13530  fzss1  13531  fzss2  13532  fzp1elp1  13545  fznn  13560  elfz2nn0  13586  elfzofz  13643  fzosplitsnm1  13708  fzofzp1b  13733  fzosplitsn  13743  seqcl2  13992  seqfveq2  13996  monoord  14004  seqid2  14020  bcn1  14285  fz1isolem  14433  seqcoll  14436  ccatrn  14561  swrds1  14638  swrdccat2  14641  spllen  14726  splfv2a  14728  splval2  14729  caubnd  15332  isercolllem2  15639  isercolllem3  15640  summolem2a  15688  fsum0diag2  15756  climcndslem1  15822  mertenslem1  15857  prodmolem2a  15907  vdwlem2  16960  vdwlem8  16966  gexcl3  19524  efginvrel2  19664  efgredleme  19680  efgcpbllemb  19692  1stckgenlem  23447  imasdsf1olem  24268  iscmet3lem1  25198  dvtaylp  26285  mtest  26320  ppisval  27021  ppisval2  27022  chtdif  27075  ppidif  27080  logfaclbnd  27140  bposlem4  27205  dchrisumlem2  27408  pntpbnd1  27504  fzsplit3  32723  mettrifi  37758  monoordxrv  45484  smonoord  47376