elfzodifsumelfzo

Description: If an integer is in a half-open range of nonnegative integers with a difference as upper bound, the sum of the integer with the subtrahend of the difference is in a half-open range of nonnegative integers containing the minuend of the difference. (Contributed by AV, 13-Nov-2018)

		Ref	Expression
	Assertion	elfzodifsumelfzo	$⊢ (M \in (0 \dots N) \land N \in (0 \dots P)) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P))$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
2		elfz2nn0	$⊢ N \in (0 \dots P) \leftrightarrow (N \in ℕ_{0} \land P \in ℕ_{0} \land N \leq P)$
3		elfzo0	$⊢ I \in (0 ..^N - M) \leftrightarrow (I \in ℕ_{0} \land N - M \in ℕ \land I < N - M)$
4		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
5		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
6		znnsub	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N - M \in ℕ)$
7	4 5 6	syl2an	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \leftrightarrow N - M \in ℕ)$
8		simpr	$⊢ (I < N - M \land I \in ℕ_{0}) \to I \in ℕ_{0}$
9		simpll	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to M \in ℕ_{0}$
10		nn0addcl	$⊢ (I \in ℕ_{0} \land M \in ℕ_{0}) \to I + M \in ℕ_{0}$
11	8 9 10	syl2anr	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \to I + M \in ℕ_{0}$
12	11	adantr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land (P \in ℕ_{0} \land N \leq P)) \to I + M \in ℕ_{0}$
13		0red	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \in ℝ$
14		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
15	14	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℝ$
16		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
17	16	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℝ$
18	13 15 17	3jca	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 \in ℝ \land M \in ℝ \land N \in ℝ)$
19	18	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to (0 \in ℝ \land M \in ℝ \land N \in ℝ)$
20		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
21	20	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \leq M$
22	21	anim1i	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to (0 \leq M \land M < N)$
23		lelttr	$⊢ (0 \in ℝ \land M \in ℝ \land N \in ℝ) \to ((0 \leq M \land M < N) \to 0 < N)$
24	19 22 23	sylc	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to 0 < N$
25	24	ex	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \to 0 < N)$
26		0red	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \in ℝ$
27	16	adantl	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℝ$
28		nn0re	$⊢ P \in ℕ_{0} \to P \in ℝ$
29	28	adantr	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to P \in ℝ$
30		ltletr	$⊢ (0 \in ℝ \land N \in ℝ \land P \in ℝ) \to ((0 < N \land N \leq P) \to 0 < P)$
31	26 27 29 30	syl3anc	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to ((0 < N \land N \leq P) \to 0 < P)$
32		nn0z	$⊢ P \in ℕ_{0} \to P \in ℤ$
33		elnnz	$⊢ P \in ℕ \leftrightarrow (P \in ℤ \land 0 < P)$
34	33	simplbi2	$⊢ P \in ℤ \to (0 < P \to P \in ℕ)$
35	32 34	syl	$⊢ P \in ℕ_{0} \to (0 < P \to P \in ℕ)$
36	35	adantr	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to (0 < P \to P \in ℕ)$
37	31 36	syld	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to ((0 < N \land N \leq P) \to P \in ℕ)$
38	37	exp4b	$⊢ P \in ℕ_{0} \to (N \in ℕ_{0} \to (0 < N \to (N \leq P \to P \in ℕ)))$
39	38	com24	$⊢ P \in ℕ_{0} \to (N \leq P \to (0 < N \to (N \in ℕ_{0} \to P \in ℕ)))$
40	39	imp	$⊢ (P \in ℕ_{0} \land N \leq P) \to (0 < N \to (N \in ℕ_{0} \to P \in ℕ))$
41	40	com13	$⊢ N \in ℕ_{0} \to (0 < N \to ((P \in ℕ_{0} \land N \leq P) \to P \in ℕ))$
42	41	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 < N \to ((P \in ℕ_{0} \land N \leq P) \to P \in ℕ))$
43	25 42	syld	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \to ((P \in ℕ_{0} \land N \leq P) \to P \in ℕ))$
44	43	imp	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to ((P \in ℕ_{0} \land N \leq P) \to P \in ℕ)$
45	44	adantr	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \to ((P \in ℕ_{0} \land N \leq P) \to P \in ℕ)$
46	45	imp	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land (P \in ℕ_{0} \land N \leq P)) \to P \in ℕ$
47		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
48	47	adantl	$⊢ (I < N - M \land I \in ℕ_{0}) \to I \in ℝ$
49	15	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to M \in ℝ$
50		readdcl	$⊢ (I \in ℝ \land M \in ℝ) \to I + M \in ℝ$
51	48 49 50	syl2anr	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \to I + M \in ℝ$
52	51	adantr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \to I + M \in ℝ$
53	17	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to N \in ℝ$
54	53	adantr	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \to N \in ℝ$
55	54	adantr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \to N \in ℝ$
56	28	adantl	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \to P \in ℝ$
57	52 55 56	3jca	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \to (I + M \in ℝ \land N \in ℝ \land P \in ℝ)$
58	57	adantr	$⊢ (((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \land N \leq P) \to (I + M \in ℝ \land N \in ℝ \land P \in ℝ)$
59	47	adantl	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land I \in ℕ_{0}) \to I \in ℝ$
60	15	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land I \in ℕ_{0}) \to M \in ℝ$
61	17	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land I \in ℕ_{0}) \to N \in ℝ$
62	59 60 61	ltaddsubd	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land I \in ℕ_{0}) \to (I + M < N \leftrightarrow I < N - M)$
63	62	exbiri	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (I \in ℕ_{0} \to (I < N - M \to I + M < N))$
64	63	impcomd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((I < N - M \land I \in ℕ_{0}) \to I + M < N)$
65	64	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \to ((I < N - M \land I \in ℕ_{0}) \to I + M < N)$
66	65	imp	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \to I + M < N$
67	66	adantr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \to I + M < N$
68	67	anim1i	$⊢ (((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \land N \leq P) \to (I + M < N \land N \leq P)$
69		ltletr	$⊢ (I + M \in ℝ \land N \in ℝ \land P \in ℝ) \to ((I + M < N \land N \leq P) \to I + M < P)$
70	58 68 69	sylc	$⊢ (((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land P \in ℕ_{0}) \land N \leq P) \to I + M < P$
71	70	anasss	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land (P \in ℕ_{0} \land N \leq P)) \to I + M < P$
72		elfzo0	$⊢ I + M \in (0 ..^P) \leftrightarrow (I + M \in ℕ_{0} \land P \in ℕ \land I + M < P)$
73	12 46 71 72	syl3anbrc	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land M < N) \land (I < N - M \land I \in ℕ_{0})) \land (P \in ℕ_{0} \land N \leq P)) \to I + M \in (0 ..^P)$
74	73	exp53	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \to (I < N - M \to (I \in ℕ_{0} \to ((P \in ℕ_{0} \land N \leq P) \to I + M \in (0 ..^P)))))$
75	7 74	sylbird	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N - M \in ℕ \to (I < N - M \to (I \in ℕ_{0} \to ((P \in ℕ_{0} \land N \leq P) \to I + M \in (0 ..^P)))))$
76	75	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (N - M \in ℕ \to (I < N - M \to (I \in ℕ_{0} \to ((P \in ℕ_{0} \land N \leq P) \to I + M \in (0 ..^P)))))$
77	76	com14	$⊢ I \in ℕ_{0} \to (N - M \in ℕ \to (I < N - M \to ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to ((P \in ℕ_{0} \land N \leq P) \to I + M \in (0 ..^P)))))$
78	77	3imp	$⊢ (I \in ℕ_{0} \land N - M \in ℕ \land I < N - M) \to ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to ((P \in ℕ_{0} \land N \leq P) \to I + M \in (0 ..^P)))$
79	3 78	sylbi	$⊢ I \in (0 ..^N - M) \to ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to ((P \in ℕ_{0} \land N \leq P) \to I + M \in (0 ..^P)))$
80	79	com13	$⊢ (P \in ℕ_{0} \land N \leq P) \to ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P)))$
81	80	3adant1	$⊢ (N \in ℕ_{0} \land P \in ℕ_{0} \land N \leq P) \to ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P)))$
82	2 81	sylbi	$⊢ N \in (0 \dots P) \to ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P)))$
83	82	com12	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (N \in (0 \dots P) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P)))$
84	1 83	sylbi	$⊢ M \in (0 \dots N) \to (N \in (0 \dots P) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P)))$
85	84	imp	$⊢ (M \in (0 \dots N) \land N \in (0 \dots P)) \to (I \in (0 ..^N - M) \to I + M \in (0 ..^P))$

Metamath Proof Explorer

Theorem elfzodifsumelfzo

Proof