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 ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( abs ‘ ( 𝐴 − 𝐷 ) ) ≤ ( 𝐹 − 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp2r ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐷 ∈ ( 𝐸 ... 𝐹 ) )
2 1 elfzelzd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐷 ∈ ℤ )
3 2 zred ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐷 ∈ ℝ )
4 simp2l ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐹 ∈ ℤ )
5 4 zred ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐹 ∈ ℝ )
6 simp1r ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐴 ∈ ( 𝐵 ... 𝐶 ) )
7 elfzel1 ⊢ ( 𝐴 ∈ ( 𝐵 ... 𝐶 ) → 𝐵 ∈ ℤ )
8 6 7 syl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐵 ∈ ℤ )
9 8 zred ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐵 ∈ ℝ )
10 5 9 resubcld ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐹 − 𝐵 ) ∈ ℝ )
11 3 10 resubcld ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐷 − ( 𝐹 − 𝐵 ) ) ∈ ℝ )
12 6 elfzelzd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐴 ∈ ℤ )
13 12 zred ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐴 ∈ ℝ )
14 elfzle2 ⊢ ( 𝐷 ∈ ( 𝐸 ... 𝐹 ) → 𝐷 ≤ 𝐹 )
15 1 14 syl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐷 ≤ 𝐹 )
16 3 5 10 15 lesub1dd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐷 − ( 𝐹 − 𝐵 ) ) ≤ ( 𝐹 − ( 𝐹 − 𝐵 ) ) )
17 5 recnd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐹 ∈ ℂ )
18 9 recnd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐵 ∈ ℂ )
19 17 18 nncand ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐹 − ( 𝐹 − 𝐵 ) ) = 𝐵 )
20 16 19 breqtrd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐷 − ( 𝐹 − 𝐵 ) ) ≤ 𝐵 )
21 elfzle1 ⊢ ( 𝐴 ∈ ( 𝐵 ... 𝐶 ) → 𝐵 ≤ 𝐴 )
22 6 21 syl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐵 ≤ 𝐴 )
23 11 9 13 20 22 letrd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐷 − ( 𝐹 − 𝐵 ) ) ≤ 𝐴 )
24 simp1l ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐶 ∈ ℤ )
25 24 zred ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐶 ∈ ℝ )
26 3 10 readdcld ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐷 + ( 𝐹 − 𝐵 ) ) ∈ ℝ )
27 elfzle2 ⊢ ( 𝐴 ∈ ( 𝐵 ... 𝐶 ) → 𝐴 ≤ 𝐶 )
28 6 27 syl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐴 ≤ 𝐶 )
29 25 3 resubcld ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐶 − 𝐷 ) ∈ ℝ )
30 elfzel1 ⊢ ( 𝐷 ∈ ( 𝐸 ... 𝐹 ) → 𝐸 ∈ ℤ )
31 1 30 syl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐸 ∈ ℤ )
32 31 zred ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐸 ∈ ℝ )
33 25 32 resubcld ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐶 − 𝐸 ) ∈ ℝ )
34 elfzle1 ⊢ ( 𝐷 ∈ ( 𝐸 ... 𝐹 ) → 𝐸 ≤ 𝐷 )
35 1 34 syl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐸 ≤ 𝐷 )
36 32 3 25 35 lesub2dd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐶 − 𝐷 ) ≤ ( 𝐶 − 𝐸 ) )
37 simp3 ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) )
38 29 33 10 36 37 letrd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐶 − 𝐷 ) ≤ ( 𝐹 − 𝐵 ) )
39 25 3 10 lesubaddd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( ( 𝐶 − 𝐷 ) ≤ ( 𝐹 − 𝐵 ) ↔ 𝐶 ≤ ( ( 𝐹 − 𝐵 ) + 𝐷 ) ) )
40 38 39 mpbid ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐶 ≤ ( ( 𝐹 − 𝐵 ) + 𝐷 ) )
41 10 recnd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( 𝐹 − 𝐵 ) ∈ ℂ )
42 3 recnd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐷 ∈ ℂ )
43 41 42 addcomd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( ( 𝐹 − 𝐵 ) + 𝐷 ) = ( 𝐷 + ( 𝐹 − 𝐵 ) ) )
44 40 43 breqtrd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐶 ≤ ( 𝐷 + ( 𝐹 − 𝐵 ) ) )
45 13 25 26 28 44 letrd ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → 𝐴 ≤ ( 𝐷 + ( 𝐹 − 𝐵 ) ) )
46 13 3 10 absdifled ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( ( abs ‘ ( 𝐴 − 𝐷 ) ) ≤ ( 𝐹 − 𝐵 ) ↔ ( ( 𝐷 − ( 𝐹 − 𝐵 ) ) ≤ 𝐴 ∧ 𝐴 ≤ ( 𝐷 + ( 𝐹 − 𝐵 ) ) ) ) )
47 23 45 46 mpbir2and ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ( 𝐵 ... 𝐶 ) ) ∧ ( 𝐹 ∈ ℤ ∧ 𝐷 ∈ ( 𝐸 ... 𝐹 ) ) ∧ ( 𝐶 − 𝐸 ) ≤ ( 𝐹 − 𝐵 ) ) → ( abs ‘ ( 𝐴 − 𝐷 ) ) ≤ ( 𝐹 − 𝐵 ) )