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 | |
|
oddcomabszz.2 | |
||
oddcomabszz.3 | |
||
oddcomabszz.4 | |
||
oddcomabszz.5 | |
||
oddcomabszz.6 | |
||
oddcomabszz.7 | |
||
Assertion | oddcomabszz | |