Metamath Proof Explorer

Theorem fzomaxdiflem

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

Ref Expression
Assertion fzomaxdiflem 
|- ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( abs ` ( B - A ) ) e. ( 0 ..^ ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( B e. ( C ..^ D ) -> B e. ZZ )
2 1 adantl 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> B e. ZZ )
3 elfzoelz 
 |-  ( A e. ( C ..^ D ) -> A e. ZZ )
4 3 adantr 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> A e. ZZ )
5 2 4 zsubcld 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( B - A ) e. ZZ )
6 5 zred 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( B - A ) e. RR )
7 2 zred 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> B e. RR )
8 4 zred 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> A e. RR )
9 7 8 subge0d 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( 0 <_ ( B - A ) <-> A <_ B ) )
10 9 biimpar 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> 0 <_ ( B - A ) )
11 absid 
 |-  ( ( ( B - A ) e. RR /\ 0 <_ ( B - A ) ) -> ( abs ` ( B - A ) ) = ( B - A ) )
12 6 10 11 syl2an2r 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( abs ` ( B - A ) ) = ( B - A ) )
13 elfzoel1 
 |-  ( B e. ( C ..^ D ) -> C e. ZZ )
14 13 adantl 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> C e. ZZ )
15 14 zred 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> C e. RR )
16 7 15 resubcld 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( B - C ) e. RR )
17 elfzoel2 
 |-  ( B e. ( C ..^ D ) -> D e. ZZ )
18 17 adantl 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> D e. ZZ )
19 18 14 zsubcld 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( D - C ) e. ZZ )
20 19 zred 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( D - C ) e. RR )
21 elfzole1 
 |-  ( A e. ( C ..^ D ) -> C <_ A )
22 21 adantr 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> C <_ A )
23 15 8 7 22 lesub2dd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( B - A ) <_ ( B - C ) )
24 18 zred 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> D e. RR )
25 elfzolt2 
 |-  ( B e. ( C ..^ D ) -> B < D )
26 25 adantl 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> B < D )
27 7 24 15 26 ltsub1dd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( B - C ) < ( D - C ) )
28 6 16 20 23 27 lelttrd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( B - A ) < ( D - C ) )
29 28 adantr 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( B - A ) < ( D - C ) )
30 0zd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> 0 e. ZZ )
31 elfzo 
 |-  ( ( ( B - A ) e. ZZ /\ 0 e. ZZ /\ ( D - C ) e. ZZ ) -> ( ( B - A ) e. ( 0 ..^ ( D - C ) ) <-> ( 0 <_ ( B - A ) /\ ( B - A ) < ( D - C ) ) ) )
32 5 30 19 31 syl3anc 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( B - A ) e. ( 0 ..^ ( D - C ) ) <-> ( 0 <_ ( B - A ) /\ ( B - A ) < ( D - C ) ) ) )
33 32 adantr 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( ( B - A ) e. ( 0 ..^ ( D - C ) ) <-> ( 0 <_ ( B - A ) /\ ( B - A ) < ( D - C ) ) ) )
34 10 29 33 mpbir2and 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( B - A ) e. ( 0 ..^ ( D - C ) ) )
35 12 34 eqeltrd 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( abs ` ( B - A ) ) e. ( 0 ..^ ( D - C ) ) )