This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℝ → ( if ( 0 ≤ 𝐴 , 𝐴 , 0 ) − if ( 0 ≤ - 𝐴 , - 𝐴 , 0 ) ) = 𝐴 )

Proof

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