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 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑂 ... 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )

Proof

Step Hyp Ref Expression
1 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
2 elfz1 ⊢ ( ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑂 ... 𝑃 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑂 ≤ 𝐾 ∧ 𝐾 ≤ 𝑃 ) ) )
3 1 2 bi2anan9 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑂 ... 𝑃 ) ) ↔ ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑂 ≤ 𝐾 ∧ 𝐾 ≤ 𝑃 ) ) ) )
4 an6 ⊢ ( ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑂 ≤ 𝐾 ∧ 𝐾 ≤ 𝑃 ) ) ↔ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) )
5 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
6 zre ⊢ ( 𝑂 ∈ ℤ → 𝑂 ∈ ℝ )
7 5 6 anim12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝑂 ∈ ℝ ) )
8 zre ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
9 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
10 8 9 anim12i ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
11 le2add ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑂 ∈ ℝ ) ∧ ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ) → ( ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) → ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ) )
12 7 10 11 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) → ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ) )
13 12 impr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ) ) → ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) )
14 13 3adantr3 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) )
15 14 adantlr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) )
16 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
17 zre ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∈ ℝ )
18 16 17 anim12i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝑃 ∈ ℝ ) )
19 le2add ⊢ ( ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) → ( ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) → ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) )
20 10 18 19 syl2anr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) → ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) )
21 20 impr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) )
22 21 3adantr2 ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) )
23 22 adantll ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) )
24 zaddcl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 + 𝐾 ) ∈ ℤ )
25 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) → ( 𝑀 + 𝑂 ) ∈ ℤ )
26 zaddcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 + 𝑃 ) ∈ ℤ )
27 elfz ⊢ ( ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝑂 ) ∈ ℤ ∧ ( 𝑁 + 𝑃 ) ∈ ℤ ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ↔ ( ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) ) )
28 24 25 26 27 syl3an ⊢ ( ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ↔ ( ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) ) )
29 28 3expb ⊢ ( ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ↔ ( ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) ) )
30 29 ancoms ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ↔ ( ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) ) )
31 30 3ad2antr1 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ↔ ( ( 𝑀 + 𝑂 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝑃 ) ) ) )
32 15 23 31 mpbir2and ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) ∧ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) )
33 32 ex ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑂 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )
34 33 an4s ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐽 ∧ 𝑂 ≤ 𝐾 ) ∧ ( 𝐽 ≤ 𝑁 ∧ 𝐾 ≤ 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )
35 4 34 biimtrid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑂 ≤ 𝐾 ∧ 𝐾 ≤ 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )
36 3 35 sylbid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑂 ... 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )