| Step |
Hyp |
Ref |
Expression |
| 1 |
|
iblrelem.1 |
|- ( ( ph /\ x e. A ) -> B e. RR ) |
| 2 |
|
iblpos.2 |
|- ( ( ph /\ x e. A ) -> 0 <_ B ) |
| 3 |
1
|
le0neg2d |
|- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> -u B <_ 0 ) ) |
| 4 |
2 3
|
mpbid |
|- ( ( ph /\ x e. A ) -> -u B <_ 0 ) |
| 5 |
4
|
adantrr |
|- ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B <_ 0 ) |
| 6 |
|
simprr |
|- ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> 0 <_ -u B ) |
| 7 |
1
|
adantrr |
|- ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> B e. RR ) |
| 8 |
7
|
renegcld |
|- ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B e. RR ) |
| 9 |
|
0re |
|- 0 e. RR |
| 10 |
|
letri3 |
|- ( ( -u B e. RR /\ 0 e. RR ) -> ( -u B = 0 <-> ( -u B <_ 0 /\ 0 <_ -u B ) ) ) |
| 11 |
8 9 10
|
sylancl |
|- ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> ( -u B = 0 <-> ( -u B <_ 0 /\ 0 <_ -u B ) ) ) |
| 12 |
5 6 11
|
mpbir2and |
|- ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B = 0 ) |
| 13 |
12
|
ifeq1da |
|- ( ph -> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = if ( ( x e. A /\ 0 <_ -u B ) , 0 , 0 ) ) |
| 14 |
|
ifid |
|- if ( ( x e. A /\ 0 <_ -u B ) , 0 , 0 ) = 0 |
| 15 |
13 14
|
eqtrdi |
|- ( ph -> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = 0 ) |
| 16 |
15
|
mpteq2dv |
|- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) = ( x e. RR |-> 0 ) ) |
| 17 |
|
fconstmpt |
|- ( RR X. { 0 } ) = ( x e. RR |-> 0 ) |
| 18 |
16 17
|
eqtr4di |
|- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) = ( RR X. { 0 } ) ) |
| 19 |
18
|
fveq2d |
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = ( S.2 ` ( RR X. { 0 } ) ) ) |
| 20 |
|
itg20 |
|- ( S.2 ` ( RR X. { 0 } ) ) = 0 |
| 21 |
19 20
|
eqtrdi |
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = 0 ) |