Metamath Proof Explorer

Theorem fzmaxdif

Description: Bound on the difference between two integers constrained to two possibly overlapping finite ranges. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion fzmaxdif 
|- ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( abs ` ( A - D ) ) <_ ( F - B ) )

Proof

Step Hyp Ref Expression
1 simp2r 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> D e. ( E ... F ) )
2 1 elfzelzd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> D e. ZZ )
3 2 zred 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> D e. RR )
4 simp2l 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> F e. ZZ )
5 4 zred 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> F e. RR )
6 simp1r 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> A e. ( B ... C ) )
7 elfzel1 
 |-  ( A e. ( B ... C ) -> B e. ZZ )
8 6 7 syl 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> B e. ZZ )
9 8 zred 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> B e. RR )
10 5 9 resubcld 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( F - B ) e. RR )
11 3 10 resubcld 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( D - ( F - B ) ) e. RR )
12 6 elfzelzd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> A e. ZZ )
13 12 zred 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> A e. RR )
14 elfzle2 
 |-  ( D e. ( E ... F ) -> D <_ F )
15 1 14 syl 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> D <_ F )
16 3 5 10 15 lesub1dd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( D - ( F - B ) ) <_ ( F - ( F - B ) ) )
17 5 recnd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> F e. CC )
18 9 recnd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> B e. CC )
19 17 18 nncand 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( F - ( F - B ) ) = B )
20 16 19 breqtrd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( D - ( F - B ) ) <_ B )
21 elfzle1 
 |-  ( A e. ( B ... C ) -> B <_ A )
22 6 21 syl 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> B <_ A )
23 11 9 13 20 22 letrd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( D - ( F - B ) ) <_ A )
24 simp1l 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> C e. ZZ )
25 24 zred 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> C e. RR )
26 3 10 readdcld 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( D + ( F - B ) ) e. RR )
27 elfzle2 
 |-  ( A e. ( B ... C ) -> A <_ C )
28 6 27 syl 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> A <_ C )
29 25 3 resubcld 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( C - D ) e. RR )
30 elfzel1 
 |-  ( D e. ( E ... F ) -> E e. ZZ )
31 1 30 syl 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> E e. ZZ )
32 31 zred 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> E e. RR )
33 25 32 resubcld 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( C - E ) e. RR )
34 elfzle1 
 |-  ( D e. ( E ... F ) -> E <_ D )
35 1 34 syl 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> E <_ D )
36 32 3 25 35 lesub2dd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( C - D ) <_ ( C - E ) )
37 simp3 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( C - E ) <_ ( F - B ) )
38 29 33 10 36 37 letrd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( C - D ) <_ ( F - B ) )
39 25 3 10 lesubaddd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( ( C - D ) <_ ( F - B ) <-> C <_ ( ( F - B ) + D ) ) )
40 38 39 mpbid 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> C <_ ( ( F - B ) + D ) )
41 10 recnd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( F - B ) e. CC )
42 3 recnd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> D e. CC )
43 41 42 addcomd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( ( F - B ) + D ) = ( D + ( F - B ) ) )
44 40 43 breqtrd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> C <_ ( D + ( F - B ) ) )
45 13 25 26 28 44 letrd 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> A <_ ( D + ( F - B ) ) )
46 13 3 10 absdifled 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( ( abs ` ( A - D ) ) <_ ( F - B ) <-> ( ( D - ( F - B ) ) <_ A /\ A <_ ( D + ( F - B ) ) ) ) )
47 23 45 46 mpbir2and 
 |-  ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( abs ` ( A - D ) ) <_ ( F - B ) )