Metamath Proof Explorer

Theorem fzrev

Description: Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

Ref Expression
Assertion fzrev 
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( K e. ( ( J - N ) ... ( J - M ) ) <-> ( J - K ) e. ( M ... N ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( J e. ZZ -> J e. RR )
2 zre 
 |-  ( K e. ZZ -> K e. RR )
3 zre 
 |-  ( N e. ZZ -> N e. RR )
4 suble 
 |-  ( ( J e. RR /\ K e. RR /\ N e. RR ) -> ( ( J - K ) <_ N <-> ( J - N ) <_ K ) )
5 1 2 3 4 syl3an 
 |-  ( ( J e. ZZ /\ K e. ZZ /\ N e. ZZ ) -> ( ( J - K ) <_ N <-> ( J - N ) <_ K ) )
6 5 3comr 
 |-  ( ( N e. ZZ /\ J e. ZZ /\ K e. ZZ ) -> ( ( J - K ) <_ N <-> ( J - N ) <_ K ) )
7 6 3expb 
 |-  ( ( N e. ZZ /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J - K ) <_ N <-> ( J - N ) <_ K ) )
8 7 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J - K ) <_ N <-> ( J - N ) <_ K ) )
9 zre 
 |-  ( M e. ZZ -> M e. RR )
10 lesub 
 |-  ( ( M e. RR /\ J e. RR /\ K e. RR ) -> ( M <_ ( J - K ) <-> K <_ ( J - M ) ) )
11 9 1 2 10 syl3an 
 |-  ( ( M e. ZZ /\ J e. ZZ /\ K e. ZZ ) -> ( M <_ ( J - K ) <-> K <_ ( J - M ) ) )
12 11 3expb 
 |-  ( ( M e. ZZ /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( M <_ ( J - K ) <-> K <_ ( J - M ) ) )
13 12 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( M <_ ( J - K ) <-> K <_ ( J - M ) ) )
14 8 13 anbi12d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( ( J - K ) <_ N /\ M <_ ( J - K ) ) <-> ( ( J - N ) <_ K /\ K <_ ( J - M ) ) ) )
15 ancom 
 |-  ( ( ( J - K ) <_ N /\ M <_ ( J - K ) ) <-> ( M <_ ( J - K ) /\ ( J - K ) <_ N ) )
16 14 15 bitr3di 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( ( J - N ) <_ K /\ K <_ ( J - M ) ) <-> ( M <_ ( J - K ) /\ ( J - K ) <_ N ) ) )
17 simprr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> K e. ZZ )
18 zsubcl 
 |-  ( ( J e. ZZ /\ N e. ZZ ) -> ( J - N ) e. ZZ )
19 18 ancoms 
 |-  ( ( N e. ZZ /\ J e. ZZ ) -> ( J - N ) e. ZZ )
20 19 ad2ant2lr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J - N ) e. ZZ )
21 zsubcl 
 |-  ( ( J e. ZZ /\ M e. ZZ ) -> ( J - M ) e. ZZ )
22 21 ancoms 
 |-  ( ( M e. ZZ /\ J e. ZZ ) -> ( J - M ) e. ZZ )
23 22 ad2ant2r 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J - M ) e. ZZ )
24 elfz 
 |-  ( ( K e. ZZ /\ ( J - N ) e. ZZ /\ ( J - M ) e. ZZ ) -> ( K e. ( ( J - N ) ... ( J - M ) ) <-> ( ( J - N ) <_ K /\ K <_ ( J - M ) ) ) )
25 17 20 23 24 syl3anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( K e. ( ( J - N ) ... ( J - M ) ) <-> ( ( J - N ) <_ K /\ K <_ ( J - M ) ) ) )
26 zsubcl 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J - K ) e. ZZ )
27 26 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J - K ) e. ZZ )
28 simpll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> M e. ZZ )
29 simplr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> N e. ZZ )
30 elfz 
 |-  ( ( ( J - K ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( J - K ) e. ( M ... N ) <-> ( M <_ ( J - K ) /\ ( J - K ) <_ N ) ) )
31 27 28 29 30 syl3anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J - K ) e. ( M ... N ) <-> ( M <_ ( J - K ) /\ ( J - K ) <_ N ) ) )
32 16 25 31 3bitr4d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( K e. ( ( J - N ) ... ( J - M ) ) <-> ( J - K ) e. ( M ... N ) ) )