Metamath Proof Explorer

Theorem 2elfz2melfz

Description: If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018) (Revised by Alexander van der Vekens, 31-May-2018)

Ref Expression
Assertion 2elfz2melfz 
|- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( N < ( A + B ) -> ( B - ( N - A ) ) e. ( 0 ... A ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( A e. ( 0 ... N ) -> A e. ZZ )
2 elfzel2 
 |-  ( B e. ( 0 ... N ) -> N e. ZZ )
3 elfzelz 
 |-  ( B e. ( 0 ... N ) -> B e. ZZ )
4 simplr 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> B e. ZZ )
5 zsubcl 
 |-  ( ( N e. ZZ /\ A e. ZZ ) -> ( N - A ) e. ZZ )
6 5 adantlr 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( N - A ) e. ZZ )
7 4 6 zsubcld 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( B - ( N - A ) ) e. ZZ )
8 7 adantr 
 |-  ( ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) /\ N < ( A + B ) ) -> ( B - ( N - A ) ) e. ZZ )
9 zre 
 |-  ( N e. ZZ -> N e. RR )
10 9 ad2antrr 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> N e. RR )
11 zaddcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
12 11 zred 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. RR )
13 12 expcom 
 |-  ( B e. ZZ -> ( A e. ZZ -> ( A + B ) e. RR ) )
14 13 adantl 
 |-  ( ( N e. ZZ /\ B e. ZZ ) -> ( A e. ZZ -> ( A + B ) e. RR ) )
15 14 imp 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( A + B ) e. RR )
16 10 15 10 ltsub1d 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( N < ( A + B ) <-> ( N - N ) < ( ( A + B ) - N ) ) )
17 zre 
 |-  ( B e. ZZ -> B e. RR )
18 9 17 anim12i 
 |-  ( ( N e. ZZ /\ B e. ZZ ) -> ( N e. RR /\ B e. RR ) )
19 zre 
 |-  ( A e. ZZ -> A e. RR )
20 18 19 anim12i 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( ( N e. RR /\ B e. RR ) /\ A e. RR ) )
21 id 
 |-  ( N e. RR -> N e. RR )
22 21 21 resubcld 
 |-  ( N e. RR -> ( N - N ) e. RR )
23 22 ad2antrr 
 |-  ( ( ( N e. RR /\ B e. RR ) /\ A e. RR ) -> ( N - N ) e. RR )
24 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
25 24 expcom 
 |-  ( B e. RR -> ( A e. RR -> ( A + B ) e. RR ) )
26 25 adantl 
 |-  ( ( N e. RR /\ B e. RR ) -> ( A e. RR -> ( A + B ) e. RR ) )
27 26 imp 
 |-  ( ( ( N e. RR /\ B e. RR ) /\ A e. RR ) -> ( A + B ) e. RR )
28 simpll 
 |-  ( ( ( N e. RR /\ B e. RR ) /\ A e. RR ) -> N e. RR )
29 27 28 resubcld 
 |-  ( ( ( N e. RR /\ B e. RR ) /\ A e. RR ) -> ( ( A + B ) - N ) e. RR )
30 23 29 jca 
 |-  ( ( ( N e. RR /\ B e. RR ) /\ A e. RR ) -> ( ( N - N ) e. RR /\ ( ( A + B ) - N ) e. RR ) )
31 ltle 
 |-  ( ( ( N - N ) e. RR /\ ( ( A + B ) - N ) e. RR ) -> ( ( N - N ) < ( ( A + B ) - N ) -> ( N - N ) <_ ( ( A + B ) - N ) ) )
32 20 30 31 3syl 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( ( N - N ) < ( ( A + B ) - N ) -> ( N - N ) <_ ( ( A + B ) - N ) ) )
33 zcn 
 |-  ( N e. ZZ -> N e. CC )
34 33 subidd 
 |-  ( N e. ZZ -> ( N - N ) = 0 )
35 34 ad2antrr 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( N - N ) = 0 )
36 zcn 
 |-  ( B e. ZZ -> B e. CC )
37 36 adantl 
 |-  ( ( N e. ZZ /\ B e. ZZ ) -> B e. CC )
38 37 adantr 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> B e. CC )
39 33 ad2antrr 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> N e. CC )
40 zcn 
 |-  ( A e. ZZ -> A e. CC )
41 40 adantl 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> A e. CC )
42 simp3 
 |-  ( ( B e. CC /\ N e. CC /\ A e. CC ) -> A e. CC )
43 simp1 
 |-  ( ( B e. CC /\ N e. CC /\ A e. CC ) -> B e. CC )
44 42 43 addcomd 
 |-  ( ( B e. CC /\ N e. CC /\ A e. CC ) -> ( A + B ) = ( B + A ) )
45 44 oveq1d 
 |-  ( ( B e. CC /\ N e. CC /\ A e. CC ) -> ( ( A + B ) - N ) = ( ( B + A ) - N ) )
46 subsub3 
 |-  ( ( B e. CC /\ N e. CC /\ A e. CC ) -> ( B - ( N - A ) ) = ( ( B + A ) - N ) )
47 45 46 eqtr4d 
 |-  ( ( B e. CC /\ N e. CC /\ A e. CC ) -> ( ( A + B ) - N ) = ( B - ( N - A ) ) )
48 38 39 41 47 syl3anc 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( ( A + B ) - N ) = ( B - ( N - A ) ) )
49 35 48 breq12d 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( ( N - N ) <_ ( ( A + B ) - N ) <-> 0 <_ ( B - ( N - A ) ) ) )
50 32 49 sylibd 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( ( N - N ) < ( ( A + B ) - N ) -> 0 <_ ( B - ( N - A ) ) ) )
51 16 50 sylbid 
 |-  ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) -> ( N < ( A + B ) -> 0 <_ ( B - ( N - A ) ) ) )
52 51 imp 
 |-  ( ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) /\ N < ( A + B ) ) -> 0 <_ ( B - ( N - A ) ) )
53 elnn0z 
 |-  ( ( B - ( N - A ) ) e. NN0 <-> ( ( B - ( N - A ) ) e. ZZ /\ 0 <_ ( B - ( N - A ) ) ) )
54 8 52 53 sylanbrc 
 |-  ( ( ( ( N e. ZZ /\ B e. ZZ ) /\ A e. ZZ ) /\ N < ( A + B ) ) -> ( B - ( N - A ) ) e. NN0 )
55 54 exp31 
 |-  ( ( N e. ZZ /\ B e. ZZ ) -> ( A e. ZZ -> ( N < ( A + B ) -> ( B - ( N - A ) ) e. NN0 ) ) )
56 2 3 55 syl2anc 
 |-  ( B e. ( 0 ... N ) -> ( A e. ZZ -> ( N < ( A + B ) -> ( B - ( N - A ) ) e. NN0 ) ) )
57 1 56 mpan9 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( N < ( A + B ) -> ( B - ( N - A ) ) e. NN0 ) )
58 57 imp 
 |-  ( ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) /\ N < ( A + B ) ) -> ( B - ( N - A ) ) e. NN0 )
59 elfznn0 
 |-  ( A e. ( 0 ... N ) -> A e. NN0 )
60 59 ad2antrr 
 |-  ( ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) /\ N < ( A + B ) ) -> A e. NN0 )
61 elfzle2 
 |-  ( B e. ( 0 ... N ) -> B <_ N )
62 61 adantl 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> B <_ N )
63 elfzel2 
 |-  ( A e. ( 0 ... N ) -> N e. ZZ )
64 63 zcnd 
 |-  ( A e. ( 0 ... N ) -> N e. CC )
65 1 zcnd 
 |-  ( A e. ( 0 ... N ) -> A e. CC )
66 64 65 jca 
 |-  ( A e. ( 0 ... N ) -> ( N e. CC /\ A e. CC ) )
67 66 adantr 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( N e. CC /\ A e. CC ) )
68 npcan 
 |-  ( ( N e. CC /\ A e. CC ) -> ( ( N - A ) + A ) = N )
69 67 68 syl 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( ( N - A ) + A ) = N )
70 62 69 breqtrrd 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> B <_ ( ( N - A ) + A ) )
71 3 zred 
 |-  ( B e. ( 0 ... N ) -> B e. RR )
72 71 adantl 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> B e. RR )
73 63 zred 
 |-  ( A e. ( 0 ... N ) -> N e. RR )
74 1 zred 
 |-  ( A e. ( 0 ... N ) -> A e. RR )
75 73 74 resubcld 
 |-  ( A e. ( 0 ... N ) -> ( N - A ) e. RR )
76 75 adantr 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( N - A ) e. RR )
77 74 adantr 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> A e. RR )
78 72 76 77 lesubadd2d 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( ( B - ( N - A ) ) <_ A <-> B <_ ( ( N - A ) + A ) ) )
79 70 78 mpbird 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( B - ( N - A ) ) <_ A )
80 79 adantr 
 |-  ( ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) /\ N < ( A + B ) ) -> ( B - ( N - A ) ) <_ A )
81 elfz2nn0 
 |-  ( ( B - ( N - A ) ) e. ( 0 ... A ) <-> ( ( B - ( N - A ) ) e. NN0 /\ A e. NN0 /\ ( B - ( N - A ) ) <_ A ) )
82 58 60 80 81 syl3anbrc 
 |-  ( ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) /\ N < ( A + B ) ) -> ( B - ( N - A ) ) e. ( 0 ... A ) )
83 82 ex 
 |-  ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( N < ( A + B ) -> ( B - ( N - A ) ) e. ( 0 ... A ) ) )