Theorem elfz2 11781

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 M e. ZZ and N e. ZZ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfz2	|- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )

Proof of Theorem elfz2

Step	Hyp	Ref	Expression
1		anass 659	. 2 |- ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) )
2		df-3an 988	. . 3 |- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) )
3	2	anbi1i 706	. 2 |- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) <-> ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
4		elfz1 11779	. . . 4 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( K e. ZZ /\ M <_ K /\ K <_ N ) ) )
5		3anass 990	. . . . 5 |- ( ( K e. ZZ /\ M <_ K /\ K <_ N ) <-> ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) )
6		ibar 511	. . . . 5 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) ) )
7	5, 6	syl5bb 265	. . . 4 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K e. ZZ /\ M <_ K /\ K <_ N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) ) )
8	4, 7	bitrd 261	. . 3 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) ) )
9		fzf 11778	. . . . . . 7 |- ... : ( ZZ X. ZZ ) --> ~P ZZ
10	9	fdmi 5716	. . . . . 6 |- dom ... = ( ZZ X. ZZ )
11	10	ndmov 6440	. . . . 5 |- ( -. ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = (/) )
12	11	eleq2d 2514	. . . 4 |- ( -. ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> K e. (/) ) )
13		noel 3702	. . . . . 6 |- -. K e. (/)
14	13	pm2.21i 136	. . . . 5 |- ( K e. (/) -> ( M e. ZZ /\ N e. ZZ ) )
15		simpl 463	. . . . 5 |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
16	14, 15	pm5.21ni 358	. . . 4 |- ( -. ( M e. ZZ /\ N e. ZZ ) -> ( K e. (/) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) ) )
17	12, 16	bitrd 261	. . 3 |- ( -. ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) ) )
18	8, 17	pm2.61i 169	. 2 |- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) )
19	1, 3, 18	3bitr4ri 286	1 |- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )

Syntax hints:   -. wn 3   <-> wb 189   /\ wa 375   /\ w3a 986   e. wcel 1890   (/)c0 3698   ~Pcpw 3918   class class class wbr 4373   X. cxp 4809  (class class class)co 6275   <_ cle 9662   ZZcz 10926   ...cfz 11774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-fv 5568  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6780  df-2nd 6781  df-neg 9849  df-z 10927  df-fz 11775

This theorem is referenced by:  elfz4  11783  elfzuzb  11784  0nelfz1  11808  uzsubsubfz  11811  fzmmmeqm  11822  fzpreddisj  11835  elfz1b  11854  fzp1nel  11868  elfz0ubfz0  11885  elfz0fzfz0  11886  fz0fzelfz0  11887  fz0fzdiffz0  11890  elfzmlbmOLD  11892  elfzmlbp  11893  preduz  11903  fzind2  12015  swrdswrdlem  12813  swrdswrd  12814  swrdccatin12lem2a  12839  swrdccatin12lem2b  12840  swrdccatin2  12841  swrdccatin12lem2  12843  swrdccat3  12846  2cshwcshw  12922  cshwcsh2id  12925  fprodntriv  14006  fprodeq0  14039  prmgaplem4  15034  chfacfscmulgsum  19894  chfacfpmmulgsum  19898  wwlkextproplem1  25480  wwlkextproplem2  25481  clwlkfclwwlk  25583  monoords  37544  uzfissfz  37579  iuneqfzuzlem  37587  ssuzfz  37602  fmul01lt1lem1  37703  fmul01lt1lem2  37704  mccllem  37718  sumnnodd  37751  dvnmul  37859  dvnprodlem1  37862  dvnprodlem2  37863  itgspltprt  37897  stoweidlem3  37919  stoweidlem34  37951  stoweidlem51  37968  fourierdlem12  38037  fourierdlem14  38039  fourierdlem41  38067  fourierdlem48  38074  fourierdlem49  38075  fourierdlem50  38076  fourierdlem79  38105  fourierdlem92  38118  fourierdlem93  38119  elaa2lem  38153  elaa2lemOLD  38154  etransclem3  38158  etransclem7  38162  etransclem10  38165  etransclem24  38179  etransclem27  38182  etransclem28  38183  etransclem35  38190  etransclem38  38193  etransclem44  38199  iundjiun  38358  caratheodorylem1  38410  iccpartiltu  38826  nnsum4primeseven  38985  nnsum4primesevenALTV  38986  pfxccatin12lem1  39056  pfxccatin12lem2  39057  pfxccat3  39059  elfzelfzlble  39154