Step |
Hyp |
Ref |
Expression |
1 |
|
0red |
|- ( A e. RR -> 0 e. RR ) |
2 |
|
id |
|- ( A e. RR -> A e. RR ) |
3 |
|
recn |
|- ( A e. RR -> A e. CC ) |
4 |
3
|
adantr |
|- ( ( A e. RR /\ 0 <_ A ) -> A e. CC ) |
5 |
4
|
addid1d |
|- ( ( A e. RR /\ 0 <_ A ) -> ( A + 0 ) = A ) |
6 |
|
iftrue |
|- ( 0 <_ A -> if ( 0 <_ A , A , 0 ) = A ) |
7 |
6
|
adantl |
|- ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ A , A , 0 ) = A ) |
8 |
|
le0neg2 |
|- ( A e. RR -> ( 0 <_ A <-> -u A <_ 0 ) ) |
9 |
8
|
biimpa |
|- ( ( A e. RR /\ 0 <_ A ) -> -u A <_ 0 ) |
10 |
9
|
adantr |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> -u A <_ 0 ) |
11 |
|
simpr |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> 0 <_ -u A ) |
12 |
|
renegcl |
|- ( A e. RR -> -u A e. RR ) |
13 |
12
|
ad2antrr |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> -u A e. RR ) |
14 |
|
0re |
|- 0 e. RR |
15 |
|
letri3 |
|- ( ( -u A e. RR /\ 0 e. RR ) -> ( -u A = 0 <-> ( -u A <_ 0 /\ 0 <_ -u A ) ) ) |
16 |
13 14 15
|
sylancl |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> ( -u A = 0 <-> ( -u A <_ 0 /\ 0 <_ -u A ) ) ) |
17 |
10 11 16
|
mpbir2and |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> -u A = 0 ) |
18 |
17
|
ifeq1da |
|- ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ -u A , -u A , 0 ) = if ( 0 <_ -u A , 0 , 0 ) ) |
19 |
|
ifid |
|- if ( 0 <_ -u A , 0 , 0 ) = 0 |
20 |
18 19
|
eqtrdi |
|- ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ -u A , -u A , 0 ) = 0 ) |
21 |
7 20
|
oveq12d |
|- ( ( A e. RR /\ 0 <_ A ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( A + 0 ) ) |
22 |
|
absid |
|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A ) |
23 |
5 21 22
|
3eqtr4d |
|- ( ( A e. RR /\ 0 <_ A ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) ) |
24 |
3
|
adantr |
|- ( ( A e. RR /\ A <_ 0 ) -> A e. CC ) |
25 |
24
|
negcld |
|- ( ( A e. RR /\ A <_ 0 ) -> -u A e. CC ) |
26 |
25
|
addid2d |
|- ( ( A e. RR /\ A <_ 0 ) -> ( 0 + -u A ) = -u A ) |
27 |
|
letri3 |
|- ( ( A e. RR /\ 0 e. RR ) -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) ) |
28 |
14 27
|
mpan2 |
|- ( A e. RR -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) ) |
29 |
28
|
biimprd |
|- ( A e. RR -> ( ( A <_ 0 /\ 0 <_ A ) -> A = 0 ) ) |
30 |
29
|
impl |
|- ( ( ( A e. RR /\ A <_ 0 ) /\ 0 <_ A ) -> A = 0 ) |
31 |
30
|
ifeq1da |
|- ( ( A e. RR /\ A <_ 0 ) -> if ( 0 <_ A , A , 0 ) = if ( 0 <_ A , 0 , 0 ) ) |
32 |
|
ifid |
|- if ( 0 <_ A , 0 , 0 ) = 0 |
33 |
31 32
|
eqtrdi |
|- ( ( A e. RR /\ A <_ 0 ) -> if ( 0 <_ A , A , 0 ) = 0 ) |
34 |
|
le0neg1 |
|- ( A e. RR -> ( A <_ 0 <-> 0 <_ -u A ) ) |
35 |
34
|
biimpa |
|- ( ( A e. RR /\ A <_ 0 ) -> 0 <_ -u A ) |
36 |
35
|
iftrued |
|- ( ( A e. RR /\ A <_ 0 ) -> if ( 0 <_ -u A , -u A , 0 ) = -u A ) |
37 |
33 36
|
oveq12d |
|- ( ( A e. RR /\ A <_ 0 ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( 0 + -u A ) ) |
38 |
|
absnid |
|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A ) |
39 |
26 37 38
|
3eqtr4d |
|- ( ( A e. RR /\ A <_ 0 ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) ) |
40 |
1 2 23 39
|
lecasei |
|- ( A e. RR -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) ) |