Metamath Proof Explorer

Theorem dnibndlem10

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

Ref Expression
Hypotheses dnibndlem10.1 
|- ( ph -> A e. RR )
dnibndlem10.2 
|- ( ph -> B e. RR )
dnibndlem10.3 
|- ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
Assertion dnibndlem10 
|- ( ph -> 1 <_ ( B - A ) )

Proof

Step Hyp Ref Expression
1 dnibndlem10.1 
 |-  ( ph -> A e. RR )
2 dnibndlem10.2 
 |-  ( ph -> B e. RR )
3 dnibndlem10.3 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
4 1red 
 |-  ( ph -> 1 e. RR )
5 halfre 
 |-  ( 1 / 2 ) e. RR
6 5 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
7 2 6 readdcld 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
8 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
9 7 8 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
10 9 6 jca 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) )
11 resubcl 
 |-  ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR )
12 10 11 syl 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR )
13 1 6 readdcld 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. RR )
14 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
15 13 14 syl 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
16 15 6 readdcld 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR )
17 12 16 jca 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR ) )
18 resubcl 
 |-  ( ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR /\ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR ) -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) e. RR )
19 17 18 syl 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) e. RR )
20 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
21 15 recnd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
22 2cnd 
 |-  ( ph -> 2 e. CC )
23 6 recnd 
 |-  ( ph -> ( 1 / 2 ) e. CC )
24 21 22 23 addsubassd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 2 - ( 1 / 2 ) ) ) )
25 24 oveq1d 
 |-  ( ph -> ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 2 - ( 1 / 2 ) ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
26 22 23 subcld 
 |-  ( ph -> ( 2 - ( 1 / 2 ) ) e. CC )
27 21 26 23 pnpcand 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 2 - ( 1 / 2 ) ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) = ( ( 2 - ( 1 / 2 ) ) - ( 1 / 2 ) ) )
28 22 23 23 subsub4d 
 |-  ( ph -> ( ( 2 - ( 1 / 2 ) ) - ( 1 / 2 ) ) = ( 2 - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
29 ax-1cn 
 |-  1 e. CC
30 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
31 29 30 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
32 31 a1i 
 |-  ( ph -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
33 32 oveq2d 
 |-  ( ph -> ( 2 - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( 2 - 1 ) )
34 2m1e1 
 |-  ( 2 - 1 ) = 1
35 34 a1i 
 |-  ( ph -> ( 2 - 1 ) = 1 )
36 28 33 35 3eqtrd 
 |-  ( ph -> ( ( 2 - ( 1 / 2 ) ) - ( 1 / 2 ) ) = 1 )
37 25 27 36 3eqtrd 
 |-  ( ph -> ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) = 1 )
38 37 eqcomd 
 |-  ( ph -> 1 = ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
39 2re 
 |-  2 e. RR
40 39 a1i 
 |-  ( ph -> 2 e. RR )
41 15 40 readdcld 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) e. RR )
42 41 6 jca 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) e. RR /\ ( 1 / 2 ) e. RR ) )
43 resubcl 
 |-  ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) e. RR )
44 42 43 syl 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) e. RR )
45 41 9 6 3 lesub1dd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) <_ ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) )
46 44 12 16 45 lesub1dd 
 |-  ( ph -> ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) <_ ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
47 38 46 eqbrtrd 
 |-  ( ph -> 1 <_ ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
48 flle 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( B + ( 1 / 2 ) ) )
49 7 48 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( B + ( 1 / 2 ) ) )
50 9 6 2 lesubaddd 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) <_ B <-> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( B + ( 1 / 2 ) ) ) )
51 49 50 mpbird 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) <_ B )
52 fllep1 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( A + ( 1 / 2 ) ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
53 13 52 syl 
 |-  ( ph -> ( A + ( 1 / 2 ) ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
54 21 23 23 addassd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
55 32 oveq2d 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
56 54 55 eqtrd 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
57 56 eqcomd 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
58 53 57 breqtrd 
 |-  ( ph -> ( A + ( 1 / 2 ) ) <_ ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
59 1 16 6 leadd1d 
 |-  ( ph -> ( A <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) <-> ( A + ( 1 / 2 ) ) <_ ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) )
60 58 59 mpbird 
 |-  ( ph -> A <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
61 12 1 2 16 51 60 le2subd 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) <_ ( B - A ) )
62 4 19 20 47 61 letrd 
 |-  ( ph -> 1 <_ ( B - A ) )