Metamath Proof Explorer

Theorem oddcomabszz

Description: An odd function which takes nonnegative values on nonnegative arguments commutes with abs . (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Hypotheses oddcomabszz.1 
|- ( ( ph /\ x e. ZZ ) -> A e. RR )
oddcomabszz.2 
|- ( ( ph /\ x e. ZZ /\ 0 <_ x ) -> 0 <_ A )
oddcomabszz.3 
|- ( ( ph /\ y e. ZZ ) -> C = -u B )
oddcomabszz.4 
|- ( x = y -> A = B )
oddcomabszz.5 
|- ( x = -u y -> A = C )
oddcomabszz.6 
|- ( x = D -> A = E )
oddcomabszz.7 
|- ( x = ( abs ` D ) -> A = F )
Assertion oddcomabszz 
|- ( ( ph /\ D e. ZZ ) -> ( abs ` E ) = F )

Proof

Step Hyp Ref Expression
1 oddcomabszz.1 
 |-  ( ( ph /\ x e. ZZ ) -> A e. RR )
2 oddcomabszz.2 
 |-  ( ( ph /\ x e. ZZ /\ 0 <_ x ) -> 0 <_ A )
3 oddcomabszz.3 
 |-  ( ( ph /\ y e. ZZ ) -> C = -u B )
4 oddcomabszz.4 
 |-  ( x = y -> A = B )
5 oddcomabszz.5 
 |-  ( x = -u y -> A = C )
6 oddcomabszz.6 
 |-  ( x = D -> A = E )
7 oddcomabszz.7 
 |-  ( x = ( abs ` D ) -> A = F )
8 eleq1 
 |-  ( a = D -> ( a e. ZZ <-> D e. ZZ ) )
9 8 anbi2d 
 |-  ( a = D -> ( ( ph /\ a e. ZZ ) <-> ( ph /\ D e. ZZ ) ) )
10 csbeq1 
 |-  ( a = D -> [_ a / x ]_ A = [_ D / x ]_ A )
11 10 fveq2d 
 |-  ( a = D -> ( abs ` [_ a / x ]_ A ) = ( abs ` [_ D / x ]_ A ) )
12 fveq2 
 |-  ( a = D -> ( abs ` a ) = ( abs ` D ) )
13 12 csbeq1d 
 |-  ( a = D -> [_ ( abs ` a ) / x ]_ A = [_ ( abs ` D ) / x ]_ A )
14 11 13 eqeq12d 
 |-  ( a = D -> ( ( abs ` [_ a / x ]_ A ) = [_ ( abs ` a ) / x ]_ A <-> ( abs ` [_ D / x ]_ A ) = [_ ( abs ` D ) / x ]_ A ) )
15 9 14 imbi12d 
 |-  ( a = D -> ( ( ( ph /\ a e. ZZ ) -> ( abs ` [_ a / x ]_ A ) = [_ ( abs ` a ) / x ]_ A ) <-> ( ( ph /\ D e. ZZ ) -> ( abs ` [_ D / x ]_ A ) = [_ ( abs ` D ) / x ]_ A ) ) )
16 nfv 
 |-  F/ x ( ph /\ a e. ZZ )
17 nfcsb1v 
 |-  F/_ x [_ a / x ]_ A
18 17 nfel1 
 |-  F/ x [_ a / x ]_ A e. RR
19 16 18 nfim 
 |-  F/ x ( ( ph /\ a e. ZZ ) -> [_ a / x ]_ A e. RR )
20 eleq1 
 |-  ( x = a -> ( x e. ZZ <-> a e. ZZ ) )
21 20 anbi2d 
 |-  ( x = a -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ a e. ZZ ) ) )
22 csbeq1a 
 |-  ( x = a -> A = [_ a / x ]_ A )
23 22 eleq1d 
 |-  ( x = a -> ( A e. RR <-> [_ a / x ]_ A e. RR ) )
24 21 23 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. ZZ ) -> A e. RR ) <-> ( ( ph /\ a e. ZZ ) -> [_ a / x ]_ A e. RR ) ) )
25 19 24 1 chvarfv 
 |-  ( ( ph /\ a e. ZZ ) -> [_ a / x ]_ A e. RR )
26 25 adantr 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> [_ a / x ]_ A e. RR )
27 nfv 
 |-  F/ x ( ph /\ a e. ZZ /\ 0 <_ a )
28 nfcv 
 |-  F/_ x 0
29 nfcv 
 |-  F/_ x <_
30 28 29 17 nfbr 
 |-  F/ x 0 <_ [_ a / x ]_ A
31 27 30 nfim 
 |-  F/ x ( ( ph /\ a e. ZZ /\ 0 <_ a ) -> 0 <_ [_ a / x ]_ A )
32 breq2 
 |-  ( x = a -> ( 0 <_ x <-> 0 <_ a ) )
33 20 32 3anbi23d 
 |-  ( x = a -> ( ( ph /\ x e. ZZ /\ 0 <_ x ) <-> ( ph /\ a e. ZZ /\ 0 <_ a ) ) )
34 22 breq2d 
 |-  ( x = a -> ( 0 <_ A <-> 0 <_ [_ a / x ]_ A ) )
35 33 34 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. ZZ /\ 0 <_ x ) -> 0 <_ A ) <-> ( ( ph /\ a e. ZZ /\ 0 <_ a ) -> 0 <_ [_ a / x ]_ A ) ) )
36 31 35 2 chvarfv 
 |-  ( ( ph /\ a e. ZZ /\ 0 <_ a ) -> 0 <_ [_ a / x ]_ A )
37 36 3expa 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> 0 <_ [_ a / x ]_ A )
38 26 37 absidd 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> ( abs ` [_ a / x ]_ A ) = [_ a / x ]_ A )
39 zre 
 |-  ( a e. ZZ -> a e. RR )
40 39 ad2antlr 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> a e. RR )
41 absid 
 |-  ( ( a e. RR /\ 0 <_ a ) -> ( abs ` a ) = a )
42 40 41 sylancom 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> ( abs ` a ) = a )
43 42 csbeq1d 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> [_ ( abs ` a ) / x ]_ A = [_ a / x ]_ A )
44 38 43 eqtr4d 
 |-  ( ( ( ph /\ a e. ZZ ) /\ 0 <_ a ) -> ( abs ` [_ a / x ]_ A ) = [_ ( abs ` a ) / x ]_ A )
45 nfv 
 |-  F/ y ( ( ph /\ a e. ZZ ) -> [_ -u a / x ]_ A = -u [_ a / x ]_ A )
46 eleq1 
 |-  ( y = a -> ( y e. ZZ <-> a e. ZZ ) )
47 46 anbi2d 
 |-  ( y = a -> ( ( ph /\ y e. ZZ ) <-> ( ph /\ a e. ZZ ) ) )
48 negex 
 |-  -u y e. _V
49 48 5 csbie 
 |-  [_ -u y / x ]_ A = C
50 negeq 
 |-  ( y = a -> -u y = -u a )
51 50 csbeq1d 
 |-  ( y = a -> [_ -u y / x ]_ A = [_ -u a / x ]_ A )
52 49 51 eqtr3id 
 |-  ( y = a -> C = [_ -u a / x ]_ A )
53 vex 
 |-  y e. _V
54 53 4 csbie 
 |-  [_ y / x ]_ A = B
55 csbeq1 
 |-  ( y = a -> [_ y / x ]_ A = [_ a / x ]_ A )
56 54 55 eqtr3id 
 |-  ( y = a -> B = [_ a / x ]_ A )
57 56 negeqd 
 |-  ( y = a -> -u B = -u [_ a / x ]_ A )
58 52 57 eqeq12d 
 |-  ( y = a -> ( C = -u B <-> [_ -u a / x ]_ A = -u [_ a / x ]_ A ) )
59 47 58 imbi12d 
 |-  ( y = a -> ( ( ( ph /\ y e. ZZ ) -> C = -u B ) <-> ( ( ph /\ a e. ZZ ) -> [_ -u a / x ]_ A = -u [_ a / x ]_ A ) ) )
60 45 59 3 chvarfv 
 |-  ( ( ph /\ a e. ZZ ) -> [_ -u a / x ]_ A = -u [_ a / x ]_ A )
61 60 adantr 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> [_ -u a / x ]_ A = -u [_ a / x ]_ A )
62 39 ad2antlr 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> a e. RR )
63 absnid 
 |-  ( ( a e. RR /\ a <_ 0 ) -> ( abs ` a ) = -u a )
64 62 63 sylancom 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> ( abs ` a ) = -u a )
65 64 csbeq1d 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> [_ ( abs ` a ) / x ]_ A = [_ -u a / x ]_ A )
66 25 adantr 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> [_ a / x ]_ A e. RR )
67 znegcl 
 |-  ( a e. ZZ -> -u a e. ZZ )
68 nfv 
 |-  F/ x ( ph /\ -u a e. ZZ /\ 0 <_ -u a )
69 nfcsb1v 
 |-  F/_ x [_ -u a / x ]_ A
70 28 29 69 nfbr 
 |-  F/ x 0 <_ [_ -u a / x ]_ A
71 68 70 nfim 
 |-  F/ x ( ( ph /\ -u a e. ZZ /\ 0 <_ -u a ) -> 0 <_ [_ -u a / x ]_ A )
72 negex 
 |-  -u a e. _V
73 eleq1 
 |-  ( x = -u a -> ( x e. ZZ <-> -u a e. ZZ ) )
74 breq2 
 |-  ( x = -u a -> ( 0 <_ x <-> 0 <_ -u a ) )
75 73 74 3anbi23d 
 |-  ( x = -u a -> ( ( ph /\ x e. ZZ /\ 0 <_ x ) <-> ( ph /\ -u a e. ZZ /\ 0 <_ -u a ) ) )
76 csbeq1a 
 |-  ( x = -u a -> A = [_ -u a / x ]_ A )
77 76 breq2d 
 |-  ( x = -u a -> ( 0 <_ A <-> 0 <_ [_ -u a / x ]_ A ) )
78 75 77 imbi12d 
 |-  ( x = -u a -> ( ( ( ph /\ x e. ZZ /\ 0 <_ x ) -> 0 <_ A ) <-> ( ( ph /\ -u a e. ZZ /\ 0 <_ -u a ) -> 0 <_ [_ -u a / x ]_ A ) ) )
79 71 72 78 2 vtoclf 
 |-  ( ( ph /\ -u a e. ZZ /\ 0 <_ -u a ) -> 0 <_ [_ -u a / x ]_ A )
80 79 3expia 
 |-  ( ( ph /\ -u a e. ZZ ) -> ( 0 <_ -u a -> 0 <_ [_ -u a / x ]_ A ) )
81 67 80 sylan2 
 |-  ( ( ph /\ a e. ZZ ) -> ( 0 <_ -u a -> 0 <_ [_ -u a / x ]_ A ) )
82 60 breq2d 
 |-  ( ( ph /\ a e. ZZ ) -> ( 0 <_ [_ -u a / x ]_ A <-> 0 <_ -u [_ a / x ]_ A ) )
83 81 82 sylibd 
 |-  ( ( ph /\ a e. ZZ ) -> ( 0 <_ -u a -> 0 <_ -u [_ a / x ]_ A ) )
84 39 adantl 
 |-  ( ( ph /\ a e. ZZ ) -> a e. RR )
85 84 le0neg1d 
 |-  ( ( ph /\ a e. ZZ ) -> ( a <_ 0 <-> 0 <_ -u a ) )
86 25 le0neg1d 
 |-  ( ( ph /\ a e. ZZ ) -> ( [_ a / x ]_ A <_ 0 <-> 0 <_ -u [_ a / x ]_ A ) )
87 83 85 86 3imtr4d 
 |-  ( ( ph /\ a e. ZZ ) -> ( a <_ 0 -> [_ a / x ]_ A <_ 0 ) )
88 87 imp 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> [_ a / x ]_ A <_ 0 )
89 66 88 absnidd 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> ( abs ` [_ a / x ]_ A ) = -u [_ a / x ]_ A )
90 61 65 89 3eqtr4rd 
 |-  ( ( ( ph /\ a e. ZZ ) /\ a <_ 0 ) -> ( abs ` [_ a / x ]_ A ) = [_ ( abs ` a ) / x ]_ A )
91 0re 
 |-  0 e. RR
92 letric 
 |-  ( ( 0 e. RR /\ a e. RR ) -> ( 0 <_ a \/ a <_ 0 ) )
93 91 39 92 sylancr 
 |-  ( a e. ZZ -> ( 0 <_ a \/ a <_ 0 ) )
94 93 adantl 
 |-  ( ( ph /\ a e. ZZ ) -> ( 0 <_ a \/ a <_ 0 ) )
95 44 90 94 mpjaodan 
 |-  ( ( ph /\ a e. ZZ ) -> ( abs ` [_ a / x ]_ A ) = [_ ( abs ` a ) / x ]_ A )
96 15 95 vtoclg 
 |-  ( D e. ZZ -> ( ( ph /\ D e. ZZ ) -> ( abs ` [_ D / x ]_ A ) = [_ ( abs ` D ) / x ]_ A ) )
97 96 anabsi7 
 |-  ( ( ph /\ D e. ZZ ) -> ( abs ` [_ D / x ]_ A ) = [_ ( abs ` D ) / x ]_ A )
98 nfcvd 
 |-  ( D e. ZZ -> F/_ x E )
99 98 6 csbiegf 
 |-  ( D e. ZZ -> [_ D / x ]_ A = E )
100 99 fveq2d 
 |-  ( D e. ZZ -> ( abs ` [_ D / x ]_ A ) = ( abs ` E ) )
101 100 adantl 
 |-  ( ( ph /\ D e. ZZ ) -> ( abs ` [_ D / x ]_ A ) = ( abs ` E ) )
102 fvex 
 |-  ( abs ` D ) e. _V
103 102 7 csbie 
 |-  [_ ( abs ` D ) / x ]_ A = F
104 103 a1i 
 |-  ( ( ph /\ D e. ZZ ) -> [_ ( abs ` D ) / x ]_ A = F )
105 97 101 104 3eqtr3d 
 |-  ( ( ph /\ D e. ZZ ) -> ( abs ` E ) = F )