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 ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 + 𝐷 ) ∈ ( ( 𝐵 + 𝐷 ) ..^ ( 𝐶 + 𝐷 ) ) )

Proof

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