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 addridd ⊢ ( ( 𝐴 ∈ ℝ ∧ 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 addlidd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 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 ‘ 𝐴 ) )