Metamath Proof Explorer

Theorem subfzo0

Description: The difference between two elements in a half-open range of nonnegative integers is greater than the negation of the upper bound and less than the upper bound of the range. (Contributed by AV, 20-Mar-2021)

Ref Expression
Assertion subfzo0 
|- ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( I e. ( 0 ..^ N ) <-> ( I e. NN0 /\ N e. NN /\ I < N ) )
2 elfzo0 
 |-  ( J e. ( 0 ..^ N ) <-> ( J e. NN0 /\ N e. NN /\ J < N ) )
3 nn0re 
 |-  ( I e. NN0 -> I e. RR )
4 3 adantr 
 |-  ( ( I e. NN0 /\ I < N ) -> I e. RR )
5 nnre 
 |-  ( N e. NN -> N e. RR )
6 nn0re 
 |-  ( J e. NN0 -> J e. RR )
7 resubcl 
 |-  ( ( N e. RR /\ J e. RR ) -> ( N - J ) e. RR )
8 5 6 7 syl2an 
 |-  ( ( N e. NN /\ J e. NN0 ) -> ( N - J ) e. RR )
9 8 ancoms 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( N - J ) e. RR )
10 9 3adant3 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( N - J ) e. RR )
11 4 10 anim12i 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( I e. RR /\ ( N - J ) e. RR ) )
12 nn0ge0 
 |-  ( I e. NN0 -> 0 <_ I )
13 12 adantr 
 |-  ( ( I e. NN0 /\ I < N ) -> 0 <_ I )
14 posdif 
 |-  ( ( J e. RR /\ N e. RR ) -> ( J < N <-> 0 < ( N - J ) ) )
15 6 5 14 syl2an 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( J < N <-> 0 < ( N - J ) ) )
16 15 biimp3a 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> 0 < ( N - J ) )
17 13 16 anim12i 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( 0 <_ I /\ 0 < ( N - J ) ) )
18 addgegt0 
 |-  ( ( ( I e. RR /\ ( N - J ) e. RR ) /\ ( 0 <_ I /\ 0 < ( N - J ) ) ) -> 0 < ( I + ( N - J ) ) )
19 11 17 18 syl2anc 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> 0 < ( I + ( N - J ) ) )
20 nn0cn 
 |-  ( I e. NN0 -> I e. CC )
21 20 adantr 
 |-  ( ( I e. NN0 /\ I < N ) -> I e. CC )
22 21 adantr 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> I e. CC )
23 nn0cn 
 |-  ( J e. NN0 -> J e. CC )
24 23 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. CC )
25 24 adantl 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> J e. CC )
26 nncn 
 |-  ( N e. NN -> N e. CC )
27 26 3ad2ant2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. CC )
28 27 adantl 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> N e. CC )
29 22 25 28 subadd23d 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( ( I - J ) + N ) = ( I + ( N - J ) ) )
30 19 29 breqtrrd 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> 0 < ( ( I - J ) + N ) )
31 6 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. RR )
32 resubcl 
 |-  ( ( I e. RR /\ J e. RR ) -> ( I - J ) e. RR )
33 4 31 32 syl2an 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( I - J ) e. RR )
34 5 3ad2ant2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. RR )
35 34 adantl 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> N e. RR )
36 33 35 possumd 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( 0 < ( ( I - J ) + N ) <-> -u N < ( I - J ) ) )
37 30 36 mpbid 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> -u N < ( I - J ) )
38 3 adantr 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> I e. RR )
39 34 adantl 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> N e. RR )
40 readdcl 
 |-  ( ( J e. RR /\ N e. RR ) -> ( J + N ) e. RR )
41 6 5 40 syl2an 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( J + N ) e. RR )
42 41 3adant3 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J + N ) e. RR )
43 42 adantl 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( J + N ) e. RR )
44 38 39 43 3jca 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( I e. RR /\ N e. RR /\ ( J + N ) e. RR ) )
45 nn0ge0 
 |-  ( J e. NN0 -> 0 <_ J )
46 45 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> 0 <_ J )
47 46 adantl 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> 0 <_ J )
48 5 6 anim12i 
 |-  ( ( N e. NN /\ J e. NN0 ) -> ( N e. RR /\ J e. RR ) )
49 48 ancoms 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( N e. RR /\ J e. RR ) )
50 49 3adant3 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( N e. RR /\ J e. RR ) )
51 50 adantl 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( N e. RR /\ J e. RR ) )
52 addge02 
 |-  ( ( N e. RR /\ J e. RR ) -> ( 0 <_ J <-> N <_ ( J + N ) ) )
53 51 52 syl 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( 0 <_ J <-> N <_ ( J + N ) ) )
54 47 53 mpbid 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> N <_ ( J + N ) )
55 44 54 lelttrdi 
 |-  ( ( I e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( I < N -> I < ( J + N ) ) )
56 55 impancom 
 |-  ( ( I e. NN0 /\ I < N ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> I < ( J + N ) ) )
57 56 imp 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> I < ( J + N ) )
58 4 adantr 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> I e. RR )
59 31 adantl 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> J e. RR )
60 58 59 35 ltsubadd2d 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( ( I - J ) < N <-> I < ( J + N ) ) )
61 57 60 mpbird 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( I - J ) < N )
62 37 61 jca 
 |-  ( ( ( I e. NN0 /\ I < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
63 62 ex 
 |-  ( ( I e. NN0 /\ I < N ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) ) )
64 2 63 biimtrid 
 |-  ( ( I e. NN0 /\ I < N ) -> ( J e. ( 0 ..^ N ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) ) )
65 64 3adant2 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( J e. ( 0 ..^ N ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) ) )
66 1 65 sylbi 
 |-  ( I e. ( 0 ..^ N ) -> ( J e. ( 0 ..^ N ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) ) )
67 66 imp 
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )