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\in ℝ\to if\left(0\le A,A,0\right)+if\left(0\le -A,-A,0\right)=\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		0red	$$⊢A\in ℝ\to 0\in ℝ$$
2		id	$$⊢A\in ℝ\to A\in ℝ$$
3		recn	$$⊢A\in ℝ\to A\in ℂ$$
4	3	adantr	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A\in ℂ$$
5	4	addridd	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A+0=A$$
6		iftrue	$$⊢0\le A\to if\left(0\le A,A,0\right)=A$$
7	6	adantl	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to if\left(0\le A,A,0\right)=A$$
8		le0neg2	$$⊢A\in ℝ\to \left(0\le A\leftrightarrow -A\le 0\right)$$
9	8	biimpa	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to -A\le 0$$
10	9	adantr	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge 0\le -A\right)\to -A\le 0$$
11		simpr	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge 0\le -A\right)\to 0\le -A$$
12		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
13	12	ad2antrr	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge 0\le -A\right)\to -A\in ℝ$$
14		0re	$$⊢0\in ℝ$$
15		letri3	$$⊢\left(-A\in ℝ\wedge 0\in ℝ\right)\to \left(-A=0\leftrightarrow \left(-A\le 0\wedge 0\le -A\right)\right)$$
16	13 14 15	sylancl	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge 0\le -A\right)\to \left(-A=0\leftrightarrow \left(-A\le 0\wedge 0\le -A\right)\right)$$
17	10 11 16	mpbir2and	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge 0\le -A\right)\to -A=0$$
18	17	ifeq1da	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to if\left(0\le -A,-A,0\right)=if\left(0\le -A,0,0\right)$$
19		ifid	$$⊢if\left(0\le -A,0,0\right)=0$$
20	18 19	eqtrdi	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to if\left(0\le -A,-A,0\right)=0$$
21	7 20	oveq12d	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to if\left(0\le A,A,0\right)+if\left(0\le -A,-A,0\right)=A+0$$
22		absid	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left|A\right|=A$$
23	5 21 22	3eqtr4d	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to if\left(0\le A,A,0\right)+if\left(0\le -A,-A,0\right)=\left|A\right|$$
24	3	adantr	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to A\in ℂ$$
25	24	negcld	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to -A\in ℂ$$
26	25	addlidd	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to 0+\left(-A\right)=-A$$
27		letri3	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to \left(A=0\leftrightarrow \left(A\le 0\wedge 0\le A\right)\right)$$
28	14 27	mpan2	$$⊢A\in ℝ\to \left(A=0\leftrightarrow \left(A\le 0\wedge 0\le A\right)\right)$$
29	28	biimprd	$$⊢A\in ℝ\to \left(\left(A\le 0\wedge 0\le A\right)\to A=0\right)$$
30	29	impl	$$⊢\left(\left(A\in ℝ\wedge A\le 0\right)\wedge 0\le A\right)\to A=0$$
31	30	ifeq1da	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to if\left(0\le A,A,0\right)=if\left(0\le A,0,0\right)$$
32		ifid	$$⊢if\left(0\le A,0,0\right)=0$$
33	31 32	eqtrdi	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to if\left(0\le A,A,0\right)=0$$
34		le0neg1	$$⊢A\in ℝ\to \left(A\le 0\leftrightarrow 0\le -A\right)$$
35	34	biimpa	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to 0\le -A$$
36	35	iftrued	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to if\left(0\le -A,-A,0\right)=-A$$
37	33 36	oveq12d	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to if\left(0\le A,A,0\right)+if\left(0\le -A,-A,0\right)=0+\left(-A\right)$$
38		absnid	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to \left|A\right|=-A$$
39	26 37 38	3eqtr4d	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to if\left(0\le A,A,0\right)+if\left(0\le -A,-A,0\right)=\left|A\right|$$
40	1 2 23 39	lecasei	$$⊢A\in ℝ\to if\left(0\le A,A,0\right)+if\left(0\le -A,-A,0\right)=\left|A\right|$$