Step |
Hyp |
Ref |
Expression |
1 |
|
ditgpos.1 |
|- ( ph -> A <_ B ) |
2 |
|
ditgneg.2 |
|- ( ph -> A e. RR ) |
3 |
|
ditgneg.3 |
|- ( ph -> B e. RR ) |
4 |
1
|
biantrurd |
|- ( ph -> ( B <_ A <-> ( A <_ B /\ B <_ A ) ) ) |
5 |
2 3
|
letri3d |
|- ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) ) |
6 |
4 5
|
bitr4d |
|- ( ph -> ( B <_ A <-> A = B ) ) |
7 |
|
ditg0 |
|- S_ [ B -> B ] C _d x = 0 |
8 |
|
neg0 |
|- -u 0 = 0 |
9 |
7 8
|
eqtr4i |
|- S_ [ B -> B ] C _d x = -u 0 |
10 |
|
ditgeq2 |
|- ( A = B -> S_ [ B -> A ] C _d x = S_ [ B -> B ] C _d x ) |
11 |
|
oveq1 |
|- ( A = B -> ( A (,) B ) = ( B (,) B ) ) |
12 |
|
iooid |
|- ( B (,) B ) = (/) |
13 |
11 12
|
eqtrdi |
|- ( A = B -> ( A (,) B ) = (/) ) |
14 |
|
itgeq1 |
|- ( ( A (,) B ) = (/) -> S. ( A (,) B ) C _d x = S. (/) C _d x ) |
15 |
13 14
|
syl |
|- ( A = B -> S. ( A (,) B ) C _d x = S. (/) C _d x ) |
16 |
|
itg0 |
|- S. (/) C _d x = 0 |
17 |
15 16
|
eqtrdi |
|- ( A = B -> S. ( A (,) B ) C _d x = 0 ) |
18 |
17
|
negeqd |
|- ( A = B -> -u S. ( A (,) B ) C _d x = -u 0 ) |
19 |
9 10 18
|
3eqtr4a |
|- ( A = B -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x ) |
20 |
6 19
|
syl6bi |
|- ( ph -> ( B <_ A -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x ) ) |
21 |
|
df-ditg |
|- S_ [ B -> A ] C _d x = if ( B <_ A , S. ( B (,) A ) C _d x , -u S. ( A (,) B ) C _d x ) |
22 |
|
iffalse |
|- ( -. B <_ A -> if ( B <_ A , S. ( B (,) A ) C _d x , -u S. ( A (,) B ) C _d x ) = -u S. ( A (,) B ) C _d x ) |
23 |
21 22
|
syl5eq |
|- ( -. B <_ A -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x ) |
24 |
20 23
|
pm2.61d1 |
|- ( ph -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x ) |