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 ⊢A∈ℝ→if0≤AA0+if0≤−A−A0=A

Proof

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