Metamath Proof Explorer


Theorem max0add

Description: The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Mario Carneiro, 24-Aug-2014)

Ref Expression
Assertion max0add ( 𝐴 ∈ ℝ → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) + if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 0red ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
2 id ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
3 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4 3 adantr ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
5 4 addid1d ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 + 0 ) = 𝐴 )
6 iftrue ( 0 ≤ 𝐴 → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) = 𝐴 )
7 6 adantl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) = 𝐴 )
8 le0neg2 ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ 0 ) )
9 8 biimpa ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → - 𝐴 ≤ 0 )
10 9 adantr ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ - 𝐴 ) → - 𝐴 ≤ 0 )
11 simpr ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ - 𝐴 ) → 0 ≤ - 𝐴 )
12 renegcl ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
13 12 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ - 𝐴 ) → - 𝐴 ∈ ℝ )
14 0re 0 ∈ ℝ
15 letri3 ( ( - 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝐴 = 0 ↔ ( - 𝐴 ≤ 0 ∧ 0 ≤ - 𝐴 ) ) )
16 13 14 15 sylancl ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ - 𝐴 ) → ( - 𝐴 = 0 ↔ ( - 𝐴 ≤ 0 ∧ 0 ≤ - 𝐴 ) ) )
17 10 11 16 mpbir2and ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ - 𝐴 ) → - 𝐴 = 0 )
18 17 ifeq1da ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) = if ( 0 ≤ - 𝐴 , 0 , 0 ) )
19 ifid if ( 0 ≤ - 𝐴 , 0 , 0 ) = 0
20 18 19 eqtrdi ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) = 0 )
21 7 20 oveq12d ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) + if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = ( 𝐴 + 0 ) )
22 absid ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
23 5 21 22 3eqtr4d ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) + if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = ( abs ‘ 𝐴 ) )
24 3 adantr ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℂ )
25 24 negcld ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → - 𝐴 ∈ ℂ )
26 25 addid2d ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( 0 + - 𝐴 ) = - 𝐴 )
27 letri3 ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 = 0 ↔ ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ) )
28 14 27 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 = 0 ↔ ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ) )
29 28 biimprd ( 𝐴 ∈ ℝ → ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) → 𝐴 = 0 ) )
30 29 impl ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 = 0 )
31 30 ifeq1da ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) = if ( 0 ≤ 𝐴 , 0 , 0 ) )
32 ifid if ( 0 ≤ 𝐴 , 0 , 0 ) = 0
33 31 32 eqtrdi ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) = 0 )
34 le0neg1 ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 0 ↔ 0 ≤ - 𝐴 ) )
35 34 biimpa ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → 0 ≤ - 𝐴 )
36 35 iftrued ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) = - 𝐴 )
37 33 36 oveq12d ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) + if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = ( 0 + - 𝐴 ) )
38 absnid ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
39 26 37 38 3eqtr4d ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) + if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = ( abs ‘ 𝐴 ) )
40 1 2 23 39 lecasei ( 𝐴 ∈ ℝ → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) + if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = ( abs ‘ 𝐴 ) )