Theorem 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	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... 𝑃 ) ) → ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐼 + 𝑀 ) ∈ ( 0 ..^ 𝑃 ) ) )

Proof

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