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 ∈ ℝ → if 0 ≤ A A 0 − if 0 ≤ − A − A 0 = A

Proof

Step Hyp Ref Expression
1 0red ⊢ A ∈ ℝ → 0 ∈ ℝ
2 id ⊢ A ∈ ℝ → A ∈ ℝ
3 iftrue ⊢ 0 ≤ A → if 0 ≤ A A 0 = A
4 3 adantl ⊢ A ∈ ℝ ∧ 0 ≤ A → if 0 ≤ A A 0 = 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 → if 0 ≤ − A − A 0 = 0
12 5 8 10 11 mp3an2i ⊢ A ∈ ℝ ∧ 0 ≤ A → if 0 ≤ − A − A 0 = 0
13 4 12 oveq12d ⊢ A ∈ ℝ ∧ 0 ≤ A → if 0 ≤ A A 0 − if 0 ≤ − A − A 0 = 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 → if 0 ≤ A A 0 − if 0 ≤ − A − A 0 = 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 → if 0 ≤ A A 0 = 0
22 5 19 20 21 mp3an2i ⊢ A ∈ ℝ ∧ A ≤ 0 → if 0 ≤ A A 0 = 0
23 le0neg1 ⊢ A ∈ ℝ → A ≤ 0 ↔ 0 ≤ − A
24 23 biimpa ⊢ A ∈ ℝ ∧ A ≤ 0 → 0 ≤ − A
25 24 iftrued ⊢ A ∈ ℝ ∧ A ≤ 0 → if 0 ≤ − A − A 0 = − A
26 22 25 oveq12d ⊢ A ∈ ℝ ∧ A ≤ 0 → if 0 ≤ A A 0 − if 0 ≤ − A − A 0 = 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 → if 0 ≤ A A 0 − if 0 ≤ − A − A 0 = A
32 1 2 17 31 lecasei ⊢ A ∈ ℝ → if 0 ≤ A A 0 − if 0 ≤ − A − A 0 = A