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
|- ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... P ) ) -> ( I e. ( 0 ..^ ( N - M ) ) -> ( I + M ) e. ( 0 ..^ P ) ) )

Proof

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