Metamath Proof Explorer

Theorem dnibndlem13

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses dnibndlem13.1 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
dnibndlem13.2 
|- ( ph -> A e. RR )
dnibndlem13.3 
|- ( ph -> B e. RR )
dnibndlem13.4 
|- ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
Assertion dnibndlem13 
|- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem13.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnibndlem13.2 
 |-  ( ph -> A e. RR )
3 dnibndlem13.3 
 |-  ( ph -> B e. RR )
4 dnibndlem13.4 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
5 2 ad2antrr 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> A e. RR )
6 3 ad2antrr 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> B e. RR )
7 simpr 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
8 1 5 6 7 dnibndlem12 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
9 2 ad2antrr 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> A e. RR )
10 3 ad2antrr 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> B e. RR )
11 simpr 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) )
12 11 eqcomd 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
13 1 9 10 12 dnibndlem9 
 |-  ( ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
14 simpr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) )
15 halfre 
 |-  ( 1 / 2 ) e. RR
16 15 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
17 2 16 readdcld 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. RR )
18 17 flcld 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. ZZ )
19 3 16 readdcld 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
20 19 flcld 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. ZZ )
21 18 20 jca 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. ZZ /\ ( |_ ` ( B + ( 1 / 2 ) ) ) e. ZZ ) )
22 21 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. ZZ /\ ( |_ ` ( B + ( 1 / 2 ) ) ) e. ZZ ) )
23 zltp1le 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. ZZ /\ ( |_ ` ( B + ( 1 / 2 ) ) ) e. ZZ ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
24 22 23 syl 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
25 14 24 mpbid 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
26 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
27 17 26 syl 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
28 peano2re 
 |-  ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) e. RR )
29 27 28 syl 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) e. RR )
30 29 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) e. RR )
31 20 zred 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
32 31 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
33 30 32 leloed 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) ) )
34 25 33 mpbid 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
35 18 peano2zd 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) e. ZZ )
36 35 20 jca 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) e. ZZ /\ ( |_ ` ( B + ( 1 / 2 ) ) ) e. ZZ ) )
37 zltp1le 
 |-  ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) e. ZZ /\ ( |_ ` ( B + ( 1 / 2 ) ) ) e. ZZ ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
38 36 37 syl 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
39 27 recnd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
40 1cnd 
 |-  ( ph -> 1 e. CC )
41 39 40 40 addassd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) + 1 ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 + 1 ) ) )
42 1p1e2 
 |-  ( 1 + 1 ) = 2
43 42 a1i 
 |-  ( ph -> ( 1 + 1 ) = 2 )
44 43 oveq2d 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 + 1 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) )
45 41 44 eqtrd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) + 1 ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) )
46 45 breq1d 
 |-  ( ph -> ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) + 1 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
47 38 46 bitrd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
48 47 biimpd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
49 48 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
50 49 orim1d 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) < ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) ) )
51 34 50 mpd 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
52 8 13 51 mpjaodan 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
53 2 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> A e. RR )
54 3 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> B e. RR )
55 simpr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) )
56 55 eqcomd 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( |_ ` ( A + ( 1 / 2 ) ) ) )
57 1 53 54 56 dnibndlem2 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
58 27 31 leloed 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) <-> ( ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) ) )
59 4 58 mpbid 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) < ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( |_ ` ( A + ( 1 / 2 ) ) ) = ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
60 52 57 59 mpjaodan 
 |-  ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )