Metamath Proof Explorer

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 the 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 ..^ 𝑃 ) ) )