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

Metamath Proof Explorer

Theorem fzoaddel

Proof