Metamath Proof Explorer

Theorem dnibndlem3

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem3.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnibndlem3.2 
 |-  ( ph -> A e. RR )
3 dnibndlem3.3 
 |-  ( ph -> B e. RR )
4 dnibndlem3.4 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
5 3 recnd 
 |-  ( ph -> B e. CC )
6 halfre 
 |-  ( 1 / 2 ) e. RR
7 6 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
8 3 7 jca 
 |-  ( ph -> ( B e. RR /\ ( 1 / 2 ) e. RR ) )
9 readdcl 
 |-  ( ( B e. RR /\ ( 1 / 2 ) e. RR ) -> ( B + ( 1 / 2 ) ) e. RR )
10 8 9 syl 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
11 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
12 10 11 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
13 12 recnd 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. CC )
14 halfcn 
 |-  ( 1 / 2 ) e. CC
15 14 a1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
16 13 15 subcld 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. CC )
17 2 recnd 
 |-  ( ph -> A e. CC )
18 5 16 17 3jca 
 |-  ( ph -> ( B e. CC /\ ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. CC /\ A e. CC ) )
19 npncan 
 |-  ( ( B e. CC /\ ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. CC /\ A e. CC ) -> ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - A ) ) = ( B - A ) )
20 18 19 syl 
 |-  ( ph -> ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - A ) ) = ( B - A ) )
21 20 eqcomd 
 |-  ( ph -> ( B - A ) = ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - A ) ) )
22 4 oveq1d 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) - ( 1 / 2 ) ) )
23 2 7 jca 
 |-  ( ph -> ( A e. RR /\ ( 1 / 2 ) e. RR ) )
24 readdcl 
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A + ( 1 / 2 ) ) e. RR )
25 23 24 syl 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. RR )
26 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
27 25 26 syl 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
28 27 recnd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
29 1cnd 
 |-  ( ph -> 1 e. CC )
30 28 29 15 3jca 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC /\ 1 e. CC /\ ( 1 / 2 ) e. CC ) )
31 addsubass 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC /\ 1 e. CC /\ ( 1 / 2 ) e. CC ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) - ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 - ( 1 / 2 ) ) ) )
32 30 31 syl 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) - ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 - ( 1 / 2 ) ) ) )
33 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
34 33 a1i 
 |-  ( ph -> ( 1 - ( 1 / 2 ) ) = ( 1 / 2 ) )
35 34 oveq2d 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 - ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
36 22 32 35 3eqtrd 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
37 36 oveq1d 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - A ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
38 37 oveq2d 
 |-  ( ph -> ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) - A ) ) = ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) )
39 21 38 eqtrd 
 |-  ( ph -> ( B - A ) = ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) )
40 39 fveq2d 
 |-  ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) )