Metamath Proof Explorer

Theorem fzoaddel

Description: Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzoaddel ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A + D ∈ B + D ..^ C + D

Proof

Step Hyp Ref Expression
1 elfzoel1 ⊢ A ∈ B ..^ C → B ∈ ℤ
2 1 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B ∈ ℤ
3 2 zred ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B ∈ ℝ
4 elfzoelz ⊢ A ∈ B ..^ C → A ∈ ℤ
5 4 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ ℤ
6 5 zred ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ ℝ
7 simpr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → D ∈ ℤ
8 7 zred ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → D ∈ ℝ
9 elfzole1 ⊢ A ∈ B ..^ C → B ≤ A
10 9 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B ≤ A
11 3 6 8 10 leadd1dd ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B + D ≤ A + D
12 elfzoel2 ⊢ A ∈ B ..^ C → C ∈ ℤ
13 12 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → C ∈ ℤ
14 13 zred ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → C ∈ ℝ
15 elfzolt2 ⊢ A ∈ B ..^ C → A < C
16 15 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A < C
17 6 14 8 16 ltadd1dd ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A + D < C + D
18 zaddcl ⊢ A ∈ ℤ ∧ D ∈ ℤ → A + D ∈ ℤ
19 4 18 sylan ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A + D ∈ ℤ
20 zaddcl ⊢ B ∈ ℤ ∧ D ∈ ℤ → B + D ∈ ℤ
21 1 20 sylan ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B + D ∈ ℤ
22 zaddcl ⊢ C ∈ ℤ ∧ D ∈ ℤ → C + D ∈ ℤ
23 12 22 sylan ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → C + D ∈ ℤ
24 elfzo ⊢ A + D ∈ ℤ ∧ B + D ∈ ℤ ∧ C + D ∈ ℤ → A + D ∈ B + D ..^ C + D ↔ B + D ≤ A + D ∧ A + D < C + D
25 19 21 23 24 syl3anc ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A + D ∈ B + D ..^ C + D ↔ B + D ≤ A + D ∧ A + D < C + D
26 11 17 25 mpbir2and ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A + D ∈ B + D ..^ C + D