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