Metamath Proof Explorer

Theorem fzaddel

Description: Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> J e. ZZ )
2 zaddcl 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J + K ) e. ZZ )
3 1 2 2thd 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J e. ZZ <-> ( J + K ) e. ZZ ) )
4 3 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ZZ <-> ( J + K ) e. ZZ ) )
5 zre 
 |-  ( M e. ZZ -> M e. RR )
6 zre 
 |-  ( J e. ZZ -> J e. RR )
7 zre 
 |-  ( K e. ZZ -> K e. RR )
8 leadd1 
 |-  ( ( M e. RR /\ J e. RR /\ K e. RR ) -> ( M <_ J <-> ( M + K ) <_ ( J + K ) ) )
9 5 6 7 8 syl3an 
 |-  ( ( M e. ZZ /\ J e. ZZ /\ K e. ZZ ) -> ( M <_ J <-> ( M + K ) <_ ( J + K ) ) )
10 9 3expb 
 |-  ( ( M e. ZZ /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( M <_ J <-> ( M + K ) <_ ( J + K ) ) )
11 10 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( M <_ J <-> ( M + K ) <_ ( J + K ) ) )
12 zre 
 |-  ( N e. ZZ -> N e. RR )
13 leadd1 
 |-  ( ( J e. RR /\ N e. RR /\ K e. RR ) -> ( J <_ N <-> ( J + K ) <_ ( N + K ) ) )
14 6 12 7 13 syl3an 
 |-  ( ( J e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( J <_ N <-> ( J + K ) <_ ( N + K ) ) )
15 14 3com12 
 |-  ( ( N e. ZZ /\ J e. ZZ /\ K e. ZZ ) -> ( J <_ N <-> ( J + K ) <_ ( N + K ) ) )
16 15 3expb 
 |-  ( ( N e. ZZ /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J <_ N <-> ( J + K ) <_ ( N + K ) ) )
17 16 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J <_ N <-> ( J + K ) <_ ( N + K ) ) )
18 4 11 17 3anbi123d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J e. ZZ /\ M <_ J /\ J <_ N ) <-> ( ( J + K ) e. ZZ /\ ( M + K ) <_ ( J + K ) /\ ( J + K ) <_ ( N + K ) ) ) )
19 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( J e. ( M ... N ) <-> ( J e. ZZ /\ M <_ J /\ J <_ N ) ) )
20 19 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J e. ZZ /\ M <_ J /\ J <_ N ) ) )
21 zaddcl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M + K ) e. ZZ )
22 zaddcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ZZ )
23 elfz1 
 |-  ( ( ( M + K ) e. ZZ /\ ( N + K ) e. ZZ ) -> ( ( J + K ) e. ( ( M + K ) ... ( N + K ) ) <-> ( ( J + K ) e. ZZ /\ ( M + K ) <_ ( J + K ) /\ ( J + K ) <_ ( N + K ) ) ) )
24 21 22 23 syl2an 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( ( J + K ) e. ( ( M + K ) ... ( N + K ) ) <-> ( ( J + K ) e. ZZ /\ ( M + K ) <_ ( J + K ) /\ ( J + K ) <_ ( N + K ) ) ) )
25 24 anandirs 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( J + K ) e. ( ( M + K ) ... ( N + K ) ) <-> ( ( J + K ) e. ZZ /\ ( M + K ) <_ ( J + K ) /\ ( J + K ) <_ ( N + K ) ) ) )
26 25 adantrl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J + K ) e. ( ( M + K ) ... ( N + K ) ) <-> ( ( J + K ) e. ZZ /\ ( M + K ) <_ ( J + K ) /\ ( J + K ) <_ ( N + K ) ) ) )
27 18 20 26 3bitr4d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J + K ) e. ( ( M + K ) ... ( N + K ) ) ) )