Theorem elincfzoext

Description: Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020)

	Ref	Expression
Assertion	elincfzoext	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzole1	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑍 )
2		elfzoelz	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 ∈ ℤ )
3	2	zred	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 ∈ ℝ )
4	3	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) → 𝑍 ∈ ℝ )
5		nn0addge1	⊢ ( ( 𝑍 ∈ ℝ ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ≤ ( 𝑍 + 𝐼 ) )
6	4 5	sylan	⊢ ( ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ≤ ( 𝑍 + 𝐼 ) )
7		elfzoel1	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ )
8	7	zred	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℝ )
9	8	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
10	3	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ℝ )
11		nn0re	⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
12	11	adantl	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℝ )
13	10 12	readdcld	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ℝ )
14		letr	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ ( 𝑍 + 𝐼 ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝑍 ∧ 𝑍 ≤ ( 𝑍 + 𝐼 ) ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
15	9 10 13 14	syl3anc	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝑀 ≤ 𝑍 ∧ 𝑍 ≤ ( 𝑍 + 𝐼 ) ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
16	15	exp4b	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐼 ∈ ℕ0 → ( 𝑀 ≤ 𝑍 → ( 𝑍 ≤ ( 𝑍 + 𝐼 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) ) ) )
17	16	com23	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝑍 → ( 𝐼 ∈ ℕ0 → ( 𝑍 ≤ ( 𝑍 + 𝐼 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) ) ) )
18	17	imp31	⊢ ( ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 ≤ ( 𝑍 + 𝐼 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
19	6 18	mpd	⊢ ( ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) )
20	19	exp31	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝑍 → ( 𝐼 ∈ ℕ0 → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) ) )
21	1 20	mpd	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐼 ∈ ℕ0 → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
22	21	imp	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) )
23		elfzoel2	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
24	23	zred	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℝ )
25	24	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
26		elfzolt2	⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 < 𝑁 )
27	26	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 < 𝑁 )
28	10 25 12 27	ltadd1dd	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) < ( 𝑁 + 𝐼 ) )
29	2	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ℤ )
30		nn0z	⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
31	30	adantl	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℤ )
32	29 31	zaddcld	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ℤ )
33	7	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
34	23	adantr	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
35	34 31	zaddcld	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑁 + 𝐼 ) ∈ ℤ )
36		elfzo	⊢ ( ( ( 𝑍 + 𝐼 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 + 𝐼 ) ∈ ℤ ) → ( ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) ↔ ( 𝑀 ≤ ( 𝑍 + 𝐼 ) ∧ ( 𝑍 + 𝐼 ) < ( 𝑁 + 𝐼 ) ) ) )
37	32 33 35 36	syl3anc	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) ↔ ( 𝑀 ≤ ( 𝑍 + 𝐼 ) ∧ ( 𝑍 + 𝐼 ) < ( 𝑁 + 𝐼 ) ) ) )
38	22 28 37	mpbir2and	⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) )