# 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 ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to \left|{A}-{D}\right|\le {F}-{B}$

### Proof

Step Hyp Ref Expression
1 simp2r ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}\in \left({E}\dots {F}\right)$
2 elfzelz ${⊢}{D}\in \left({E}\dots {F}\right)\to {D}\in ℤ$
3 1 2 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}\in ℤ$
4 3 zred ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}\in ℝ$
5 simp2l ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}\in ℤ$
6 5 zred ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}\in ℝ$
7 simp1r ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {A}\in \left({B}\dots {C}\right)$
8 elfzel1 ${⊢}{A}\in \left({B}\dots {C}\right)\to {B}\in ℤ$
9 7 8 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {B}\in ℤ$
10 9 zred ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {B}\in ℝ$
11 6 10 resubcld ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}-{B}\in ℝ$
12 4 11 resubcld ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}-\left({F}-{B}\right)\in ℝ$
13 elfzelz ${⊢}{A}\in \left({B}\dots {C}\right)\to {A}\in ℤ$
14 7 13 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {A}\in ℤ$
15 14 zred ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {A}\in ℝ$
16 elfzle2 ${⊢}{D}\in \left({E}\dots {F}\right)\to {D}\le {F}$
17 1 16 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}\le {F}$
18 4 6 11 17 lesub1dd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}-\left({F}-{B}\right)\le {F}-\left({F}-{B}\right)$
19 6 recnd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}\in ℂ$
20 10 recnd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {B}\in ℂ$
21 19 20 nncand ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}-\left({F}-{B}\right)={B}$
22 18 21 breqtrd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}-\left({F}-{B}\right)\le {B}$
23 elfzle1 ${⊢}{A}\in \left({B}\dots {C}\right)\to {B}\le {A}$
24 7 23 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {B}\le {A}$
25 12 10 15 22 24 letrd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}-\left({F}-{B}\right)\le {A}$
26 simp1l ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}\in ℤ$
27 26 zred ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}\in ℝ$
28 4 11 readdcld ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}+{F}-{B}\in ℝ$
29 elfzle2 ${⊢}{A}\in \left({B}\dots {C}\right)\to {A}\le {C}$
30 7 29 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {A}\le {C}$
31 27 4 resubcld ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}-{D}\in ℝ$
32 elfzel1 ${⊢}{D}\in \left({E}\dots {F}\right)\to {E}\in ℤ$
33 1 32 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {E}\in ℤ$
34 33 zred ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {E}\in ℝ$
35 27 34 resubcld ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}-{E}\in ℝ$
36 elfzle1 ${⊢}{D}\in \left({E}\dots {F}\right)\to {E}\le {D}$
37 1 36 syl ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {E}\le {D}$
38 34 4 27 37 lesub2dd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}-{D}\le {C}-{E}$
39 simp3 ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}-{E}\le {F}-{B}$
40 31 35 11 38 39 letrd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}-{D}\le {F}-{B}$
41 27 4 11 lesubaddd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to \left({C}-{D}\le {F}-{B}↔{C}\le {F}-{B}+{D}\right)$
42 40 41 mpbid ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}\le {F}-{B}+{D}$
43 11 recnd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}-{B}\in ℂ$
44 4 recnd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {D}\in ℂ$
45 43 44 addcomd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {F}-{B}+{D}={D}+{F}-{B}$
46 42 45 breqtrd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {C}\le {D}+{F}-{B}$
47 15 27 28 30 46 letrd ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to {A}\le {D}+{F}-{B}$
48 15 4 11 absdifled ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to \left(\left|{A}-{D}\right|\le {F}-{B}↔\left({D}-\left({F}-{B}\right)\le {A}\wedge {A}\le {D}+{F}-{B}\right)\right)$
49 25 47 48 mpbir2and ${⊢}\left(\left({C}\in ℤ\wedge {A}\in \left({B}\dots {C}\right)\right)\wedge \left({F}\in ℤ\wedge {D}\in \left({E}\dots {F}\right)\right)\wedge {C}-{E}\le {F}-{B}\right)\to \left|{A}-{D}\right|\le {F}-{B}$