Metamath Proof Explorer

Theorem fzadd2

Description: Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion fzadd2 
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) -> ( ( J e. ( M ... N ) /\ K e. ( O ... P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )

Proof

Step Hyp Ref Expression
1 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( J e. ( M ... N ) <-> ( J e. ZZ /\ M <_ J /\ J <_ N ) ) )
2 elfz1 
 |-  ( ( O e. ZZ /\ P e. ZZ ) -> ( K e. ( O ... P ) <-> ( K e. ZZ /\ O <_ K /\ K <_ P ) ) )
3 1 2 bi2anan9 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) -> ( ( J e. ( M ... N ) /\ K e. ( O ... P ) ) <-> ( ( J e. ZZ /\ M <_ J /\ J <_ N ) /\ ( K e. ZZ /\ O <_ K /\ K <_ P ) ) ) )
4 an6 
 |-  ( ( ( J e. ZZ /\ M <_ J /\ J <_ N ) /\ ( K e. ZZ /\ O <_ K /\ K <_ P ) ) <-> ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) )
5 zre 
 |-  ( M e. ZZ -> M e. RR )
6 zre 
 |-  ( O e. ZZ -> O e. RR )
7 5 6 anim12i 
 |-  ( ( M e. ZZ /\ O e. ZZ ) -> ( M e. RR /\ O e. RR ) )
8 zre 
 |-  ( J e. ZZ -> J e. RR )
9 zre 
 |-  ( K e. ZZ -> K e. RR )
10 8 9 anim12i 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J e. RR /\ K e. RR ) )
11 le2add 
 |-  ( ( ( M e. RR /\ O e. RR ) /\ ( J e. RR /\ K e. RR ) ) -> ( ( M <_ J /\ O <_ K ) -> ( M + O ) <_ ( J + K ) ) )
12 7 10 11 syl2an 
 |-  ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( M <_ J /\ O <_ K ) -> ( M + O ) <_ ( J + K ) ) )
13 12 impr 
 |-  ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) ) ) -> ( M + O ) <_ ( J + K ) )
14 13 3adantr3 
 |-  ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( M + O ) <_ ( J + K ) )
15 14 adantlr 
 |-  ( ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( M + O ) <_ ( J + K ) )
16 zre 
 |-  ( N e. ZZ -> N e. RR )
17 zre 
 |-  ( P e. ZZ -> P e. RR )
18 16 17 anim12i 
 |-  ( ( N e. ZZ /\ P e. ZZ ) -> ( N e. RR /\ P e. RR ) )
19 le2add 
 |-  ( ( ( J e. RR /\ K e. RR ) /\ ( N e. RR /\ P e. RR ) ) -> ( ( J <_ N /\ K <_ P ) -> ( J + K ) <_ ( N + P ) ) )
20 10 18 19 syl2anr 
 |-  ( ( ( N e. ZZ /\ P e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J <_ N /\ K <_ P ) -> ( J + K ) <_ ( N + P ) ) )
21 20 impr 
 |-  ( ( ( N e. ZZ /\ P e. ZZ ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( J + K ) <_ ( N + P ) )
22 21 3adantr2 
 |-  ( ( ( N e. ZZ /\ P e. ZZ ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( J + K ) <_ ( N + P ) )
23 22 adantll 
 |-  ( ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( J + K ) <_ ( N + P ) )
24 zaddcl 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J + K ) e. ZZ )
25 zaddcl 
 |-  ( ( M e. ZZ /\ O e. ZZ ) -> ( M + O ) e. ZZ )
26 zaddcl 
 |-  ( ( N e. ZZ /\ P e. ZZ ) -> ( N + P ) e. ZZ )
27 elfz 
 |-  ( ( ( J + K ) e. ZZ /\ ( M + O ) e. ZZ /\ ( N + P ) e. ZZ ) -> ( ( J + K ) e. ( ( M + O ) ... ( N + P ) ) <-> ( ( M + O ) <_ ( J + K ) /\ ( J + K ) <_ ( N + P ) ) ) )
28 24 25 26 27 syl3an 
 |-  ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) -> ( ( J + K ) e. ( ( M + O ) ... ( N + P ) ) <-> ( ( M + O ) <_ ( J + K ) /\ ( J + K ) <_ ( N + P ) ) ) )
29 28 3expb 
 |-  ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) ) -> ( ( J + K ) e. ( ( M + O ) ... ( N + P ) ) <-> ( ( M + O ) <_ ( J + K ) /\ ( J + K ) <_ ( N + P ) ) ) )
30 29 ancoms 
 |-  ( ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J + K ) e. ( ( M + O ) ... ( N + P ) ) <-> ( ( M + O ) <_ ( J + K ) /\ ( J + K ) <_ ( N + P ) ) ) )
31 30 3ad2antr1 
 |-  ( ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( ( J + K ) e. ( ( M + O ) ... ( N + P ) ) <-> ( ( M + O ) <_ ( J + K ) /\ ( J + K ) <_ ( N + P ) ) ) )
32 15 23 31 mpbir2and 
 |-  ( ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) /\ ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) )
33 32 ex 
 |-  ( ( ( M e. ZZ /\ O e. ZZ ) /\ ( N e. ZZ /\ P e. ZZ ) ) -> ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )
34 33 an4s 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) -> ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( M <_ J /\ O <_ K ) /\ ( J <_ N /\ K <_ P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )
35 4 34 biimtrid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) -> ( ( ( J e. ZZ /\ M <_ J /\ J <_ N ) /\ ( K e. ZZ /\ O <_ K /\ K <_ P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )
36 3 35 sylbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) -> ( ( J e. ( M ... N ) /\ K e. ( O ... P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )