# Metamath Proof Explorer

## Theorem fzomaxdiflem

Description: Lemma for fzomaxdif . (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion fzomaxdiflem ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to \left|{B}-{A}\right|\in \left(0..^{D}-{C}\right)$

### Proof

Step Hyp Ref Expression
1 elfzoelz ${⊢}{B}\in \left({C}..^{D}\right)\to {B}\in ℤ$
2 1 adantl ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}\in ℤ$
3 elfzoelz ${⊢}{A}\in \left({C}..^{D}\right)\to {A}\in ℤ$
4 3 adantr ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {A}\in ℤ$
5 2 4 zsubcld ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}-{A}\in ℤ$
6 5 zred ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}-{A}\in ℝ$
7 2 zred ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}\in ℝ$
8 4 zred ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {A}\in ℝ$
9 7 8 subge0d ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to \left(0\le {B}-{A}↔{A}\le {B}\right)$
10 9 biimpar ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to 0\le {B}-{A}$
11 absid ${⊢}\left({B}-{A}\in ℝ\wedge 0\le {B}-{A}\right)\to \left|{B}-{A}\right|={B}-{A}$
12 6 10 11 syl2an2r ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to \left|{B}-{A}\right|={B}-{A}$
13 elfzoel1 ${⊢}{B}\in \left({C}..^{D}\right)\to {C}\in ℤ$
14 13 adantl ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {C}\in ℤ$
15 14 zred ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {C}\in ℝ$
16 7 15 resubcld ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}-{C}\in ℝ$
17 elfzoel2 ${⊢}{B}\in \left({C}..^{D}\right)\to {D}\in ℤ$
18 17 adantl ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {D}\in ℤ$
19 18 14 zsubcld ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {D}-{C}\in ℤ$
20 19 zred ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {D}-{C}\in ℝ$
21 elfzole1 ${⊢}{A}\in \left({C}..^{D}\right)\to {C}\le {A}$
22 21 adantr ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {C}\le {A}$
23 15 8 7 22 lesub2dd ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}-{A}\le {B}-{C}$
24 18 zred ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {D}\in ℝ$
25 elfzolt2 ${⊢}{B}\in \left({C}..^{D}\right)\to {B}<{D}$
26 25 adantl ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}<{D}$
27 7 24 15 26 ltsub1dd ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}-{C}<{D}-{C}$
28 6 16 20 23 27 lelttrd ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to {B}-{A}<{D}-{C}$
29 28 adantr ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to {B}-{A}<{D}-{C}$
30 0zd ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to 0\in ℤ$
31 elfzo ${⊢}\left({B}-{A}\in ℤ\wedge 0\in ℤ\wedge {D}-{C}\in ℤ\right)\to \left({B}-{A}\in \left(0..^{D}-{C}\right)↔\left(0\le {B}-{A}\wedge {B}-{A}<{D}-{C}\right)\right)$
32 5 30 19 31 syl3anc ${⊢}\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\to \left({B}-{A}\in \left(0..^{D}-{C}\right)↔\left(0\le {B}-{A}\wedge {B}-{A}<{D}-{C}\right)\right)$
33 32 adantr ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to \left({B}-{A}\in \left(0..^{D}-{C}\right)↔\left(0\le {B}-{A}\wedge {B}-{A}<{D}-{C}\right)\right)$
34 10 29 33 mpbir2and ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to {B}-{A}\in \left(0..^{D}-{C}\right)$
35 12 34 eqeltrd ${⊢}\left(\left({A}\in \left({C}..^{D}\right)\wedge {B}\in \left({C}..^{D}\right)\right)\wedge {A}\le {B}\right)\to \left|{B}-{A}\right|\in \left(0..^{D}-{C}\right)$