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 φxA
oddcomabszz.2 φx0x0A
oddcomabszz.3 φyC=B
oddcomabszz.4 x=yA=B
oddcomabszz.5 x=yA=C
oddcomabszz.6 x=DA=E
oddcomabszz.7 x=DA=F
Assertion oddcomabszz φDE=F

Proof

Step Hyp Ref Expression
1 oddcomabszz.1 φxA
2 oddcomabszz.2 φx0x0A
3 oddcomabszz.3 φyC=B
4 oddcomabszz.4 x=yA=B
5 oddcomabszz.5 x=yA=C
6 oddcomabszz.6 x=DA=E
7 oddcomabszz.7 x=DA=F
8 eleq1 a=DaD
9 8 anbi2d a=DφaφD
10 csbeq1 a=Da/xA=D/xA
11 10 fveq2d a=Da/xA=D/xA
12 fveq2 a=Da=D
13 12 csbeq1d a=Da/xA=D/xA
14 11 13 eqeq12d a=Da/xA=a/xAD/xA=D/xA
15 9 14 imbi12d a=Dφaa/xA=a/xAφDD/xA=D/xA
16 nfv xφa
17 nfcsb1v _xa/xA
18 17 nfel1 xa/xA
19 16 18 nfim xφaa/xA
20 eleq1 x=axa
21 20 anbi2d x=aφxφa
22 csbeq1a x=aA=a/xA
23 22 eleq1d x=aAa/xA
24 21 23 imbi12d x=aφxAφaa/xA
25 19 24 1 chvarfv φaa/xA
26 25 adantr φa0aa/xA
27 nfv xφa0a
28 nfcv _x0
29 nfcv _x
30 28 29 17 nfbr x0a/xA
31 27 30 nfim xφa0a0a/xA
32 breq2 x=a0x0a
33 20 32 3anbi23d x=aφx0xφa0a
34 22 breq2d x=a0A0a/xA
35 33 34 imbi12d x=aφx0x0Aφa0a0a/xA
36 31 35 2 chvarfv φa0a0a/xA
37 36 3expa φa0a0a/xA
38 26 37 absidd φa0aa/xA=a/xA
39 zre aa
40 39 ad2antlr φa0aa
41 absid a0aa=a
42 40 41 sylancom φa0aa=a
43 42 csbeq1d φa0aa/xA=a/xA
44 38 43 eqtr4d φa0aa/xA=a/xA
45 nfv yφaa/xA=a/xA
46 eleq1 y=aya
47 46 anbi2d y=aφyφa
48 negex yV
49 48 5 csbie y/xA=C
50 negeq y=ay=a
51 50 csbeq1d y=ay/xA=a/xA
52 49 51 eqtr3id y=aC=a/xA
53 vex yV
54 53 4 csbie y/xA=B
55 csbeq1 y=ay/xA=a/xA
56 54 55 eqtr3id y=aB=a/xA
57 56 negeqd y=aB=a/xA
58 52 57 eqeq12d y=aC=Ba/xA=a/xA
59 47 58 imbi12d y=aφyC=Bφaa/xA=a/xA
60 45 59 3 chvarfv φaa/xA=a/xA
61 60 adantr φaa0a/xA=a/xA
62 39 ad2antlr φaa0a
63 absnid aa0a=a
64 62 63 sylancom φaa0a=a
65 64 csbeq1d φaa0a/xA=a/xA
66 25 adantr φaa0a/xA
67 znegcl aa
68 nfv xφa0a
69 nfcsb1v _xa/xA
70 28 29 69 nfbr x0a/xA
71 68 70 nfim xφa0a0a/xA
72 negex aV
73 eleq1 x=axa
74 breq2 x=a0x0a
75 73 74 3anbi23d x=aφx0xφa0a
76 csbeq1a x=aA=a/xA
77 76 breq2d x=a0A0a/xA
78 75 77 imbi12d x=aφx0x0Aφa0a0a/xA
79 71 72 78 2 vtoclf φa0a0a/xA
80 79 3expia φa0a0a/xA
81 67 80 sylan2 φa0a0a/xA
82 60 breq2d φa0a/xA0a/xA
83 81 82 sylibd φa0a0a/xA
84 39 adantl φaa
85 84 le0neg1d φaa00a
86 25 le0neg1d φaa/xA00a/xA
87 83 85 86 3imtr4d φaa0a/xA0
88 87 imp φaa0a/xA0
89 66 88 absnidd φaa0a/xA=a/xA
90 61 65 89 3eqtr4rd φaa0a/xA=a/xA
91 0re 0
92 letric 0a0aa0
93 91 39 92 sylancr a0aa0
94 93 adantl φa0aa0
95 44 90 94 mpjaodan φaa/xA=a/xA
96 15 95 vtoclg DφDD/xA=D/xA
97 96 anabsi7 φDD/xA=D/xA
98 nfcvd D_xE
99 98 6 csbiegf DD/xA=E
100 99 fveq2d DD/xA=E
101 100 adantl φDD/xA=E
102 fvex DV
103 102 7 csbie D/xA=F
104 103 a1i φDD/xA=F
105 97 101 104 3eqtr3d φDE=F