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	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z + I \in (M ..^N + I)$

Proof

Step	Hyp	Ref	Expression
1		elfzole1	$⊢ Z \in (M ..^N) \to M \leq Z$
2		elfzoelz	$⊢ Z \in (M ..^N) \to Z \in ℤ$
3	2	zred	$⊢ Z \in (M ..^N) \to Z \in ℝ$
4	3	adantr	$⊢ (Z \in (M ..^N) \land M \leq Z) \to Z \in ℝ$
5		nn0addge1	$⊢ (Z \in ℝ \land I \in ℕ_{0}) \to Z \leq Z + I$
6	4 5	sylan	$⊢ ((Z \in (M ..^N) \land M \leq Z) \land I \in ℕ_{0}) \to Z \leq Z + I$
7		elfzoel1	$⊢ Z \in (M ..^N) \to M \in ℤ$
8	7	zred	$⊢ Z \in (M ..^N) \to M \in ℝ$
9	8	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to M \in ℝ$
10	3	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in ℝ$
11		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
12	11	adantl	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to I \in ℝ$
13	10 12	readdcld	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z + I \in ℝ$
14		letr	$⊢ (M \in ℝ \land Z \in ℝ \land Z + I \in ℝ) \to ((M \leq Z \land Z \leq Z + I) \to M \leq Z + I)$
15	9 10 13 14	syl3anc	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to ((M \leq Z \land Z \leq Z + I) \to M \leq Z + I)$
16	15	exp4b	$⊢ Z \in (M ..^N) \to (I \in ℕ_{0} \to (M \leq Z \to (Z \leq Z + I \to M \leq Z + I)))$
17	16	com23	$⊢ Z \in (M ..^N) \to (M \leq Z \to (I \in ℕ_{0} \to (Z \leq Z + I \to M \leq Z + I)))$
18	17	imp31	$⊢ ((Z \in (M ..^N) \land M \leq Z) \land I \in ℕ_{0}) \to (Z \leq Z + I \to M \leq Z + I)$
19	6 18	mpd	$⊢ ((Z \in (M ..^N) \land M \leq Z) \land I \in ℕ_{0}) \to M \leq Z + I$
20	19	exp31	$⊢ Z \in (M ..^N) \to (M \leq Z \to (I \in ℕ_{0} \to M \leq Z + I))$
21	1 20	mpd	$⊢ Z \in (M ..^N) \to (I \in ℕ_{0} \to M \leq Z + I)$
22	21	imp	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to M \leq Z + I$
23		elfzoel2	$⊢ Z \in (M ..^N) \to N \in ℤ$
24	23	zred	$⊢ Z \in (M ..^N) \to N \in ℝ$
25	24	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to N \in ℝ$
26		elfzolt2	$⊢ Z \in (M ..^N) \to Z < N$
27	26	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z < N$
28	10 25 12 27	ltadd1dd	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z + I < N + I$
29	2	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in ℤ$
30		nn0z	$⊢ I \in ℕ_{0} \to I \in ℤ$
31	30	adantl	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to I \in ℤ$
32	29 31	zaddcld	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z + I \in ℤ$
33	7	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to M \in ℤ$
34	23	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to N \in ℤ$
35	34 31	zaddcld	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to N + I \in ℤ$
36		elfzo	$⊢ (Z + I \in ℤ \land M \in ℤ \land N + I \in ℤ) \to (Z + I \in (M ..^N + I) \leftrightarrow (M \leq Z + I \land Z + I < N + I))$
37	32 33 35 36	syl3anc	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to (Z + I \in (M ..^N + I) \leftrightarrow (M \leq Z + I \land Z + I < N + I))$
38	22 28 37	mpbir2and	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z + I \in (M ..^N + I)$

Metamath Proof Explorer

Theorem elincfzoext

Proof