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 
|- ( ( 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 ) ) )