This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐽 ∈ ℤ )
2 zaddcl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 + 𝐾 ) ∈ ℤ )
3 1 2 2thd ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ∈ ℤ ↔ ( 𝐽 + 𝐾 ) ∈ ℤ ) )
4 3 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ℤ ↔ ( 𝐽 + 𝐾 ) ∈ ℤ ) )
5 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
6 zre ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
7 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
8 leadd1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
9 5 6 7 8 syl3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
10 9 3expb ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
11 10 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
12 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
13 leadd1 ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
14 6 12 7 13 syl3an ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
15 14 3com12 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
16 15 3expb ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
17 16 adantll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
18 4 11 17 3anbi123d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
19 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
20 19 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
21 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
22 zaddcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
23 elfz1 ⊢ ( ( ( 𝑀 + 𝐾 ) ∈ ℤ ∧ ( 𝑁 + 𝐾 ) ∈ ℤ ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
24 21 22 23 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
25 24 anandirs ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
26 25 adantrl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
27 18 20 26 3bitr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )