Metamath Proof Explorer

Theorem max0sub

Description: Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion max0sub ⊢A∈ℝ→if0≤AA0−if0≤−A−A0=A

Proof

Step Hyp Ref Expression
1 0red ⊢A∈ℝ→0∈ℝ
2 id ⊢A∈ℝ→A∈ℝ
3 iftrue ⊢0≤A→if0≤AA0=A
4 3 adantl ⊢A∈ℝ∧0≤A→if0≤AA0=A
5 0xr ⊢0∈ℝ*
6 renegcl ⊢A∈ℝ→−A∈ℝ
7 6 adantr ⊢A∈ℝ∧0≤A→−A∈ℝ
8 7 rexrd ⊢A∈ℝ∧0≤A→−A∈ℝ*
9 le0neg2 ⊢A∈ℝ→0≤A↔−A≤0
10 9 biimpa ⊢A∈ℝ∧0≤A→−A≤0
11 xrmaxeq ⊢0∈ℝ*∧−A∈ℝ*∧−A≤0→if0≤−A−A0=0
12 5 8 10 11 mp3an2i ⊢A∈ℝ∧0≤A→if0≤−A−A0=0
13 4 12 oveq12d ⊢A∈ℝ∧0≤A→if0≤AA0−if0≤−A−A0=A−0
14 recn ⊢A∈ℝ→A∈ℂ
15 14 adantr ⊢A∈ℝ∧0≤A→A∈ℂ
16 15 subid1d ⊢A∈ℝ∧0≤A→A−0=A
17 13 16 eqtrd ⊢A∈ℝ∧0≤A→if0≤AA0−if0≤−A−A0=A
18 rexr ⊢A∈ℝ→A∈ℝ*
19 18 adantr ⊢A∈ℝ∧A≤0→A∈ℝ*
20 simpr ⊢A∈ℝ∧A≤0→A≤0
21 xrmaxeq ⊢0∈ℝ*∧A∈ℝ*∧A≤0→if0≤AA0=0
22 5 19 20 21 mp3an2i ⊢A∈ℝ∧A≤0→if0≤AA0=0
23 le0neg1 ⊢A∈ℝ→A≤0↔0≤−A
24 23 biimpa ⊢A∈ℝ∧A≤0→0≤−A
25 24 iftrued ⊢A∈ℝ∧A≤0→if0≤−A−A0=−A
26 22 25 oveq12d ⊢A∈ℝ∧A≤0→if0≤AA0−if0≤−A−A0=0−−A
27 df-neg ⊢−−A=0−−A
28 14 adantr ⊢A∈ℝ∧A≤0→A∈ℂ
29 28 negnegd ⊢A∈ℝ∧A≤0→−−A=A
30 27 29 eqtr3id ⊢A∈ℝ∧A≤0→0−−A=A
31 26 30 eqtrd ⊢A∈ℝ∧A≤0→if0≤AA0−if0≤−A−A0=A
32 1 2 17 31 lecasei ⊢A∈ℝ→if0≤AA0−if0≤−A−A0=A