Metamath Proof Explorer

Theorem absmax

Description: The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008)

Ref Expression
Assertion absmax ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 2cn ⊢ 2 ∈ ℂ
3 2ne0 ⊢ 2 ≠ 0
4 divcan3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
5 2 3 4 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
6 1 5 syl ⊢ ( 𝐴 ∈ ℝ → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
7 6 ad2antlr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
8 ltle ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 → 𝐵 ≤ 𝐴 ) )
9 8 imp ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → 𝐵 ≤ 𝐴 )
10 abssubge0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ≤ 𝐴 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
11 10 3expa ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
12 9 11 syldan ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
13 12 oveq2d ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) = ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) )
14 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
15 simpr ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ℂ )
16 simpl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → 𝐵 ∈ ℂ )
17 15 16 15 ppncand ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( 𝐴 + 𝐴 ) )
18 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
19 18 adantl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
20 17 19 eqtr4d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( 2 · 𝐴 ) )
21 14 1 20 syl2an ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( 2 · 𝐴 ) )
22 21 adantr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( 2 · 𝐴 ) )
23 13 22 eqtrd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) = ( 2 · 𝐴 ) )
24 23 oveq1d ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) = ( ( 2 · 𝐴 ) / 2 ) )
25 ltnle ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵 ) )
26 25 biimpa ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ¬ 𝐴 ≤ 𝐵 )
27 26 iffalsed ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 )
28 7 24 27 3eqtr4rd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) )
29 28 ancom1s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) )
30 divcan3 ⊢ ( ( 𝐵 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
31 2 3 30 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
32 14 31 syl ⊢ ( 𝐵 ∈ ℝ → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
33 32 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
34 abssuble0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
35 34 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
36 35 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) = ( ( 𝐴 + 𝐵 ) + ( 𝐵 − 𝐴 ) ) )
37 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
38 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
39 37 38 37 ppncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐵 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐵 + 𝐵 ) )
40 addcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
41 40 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + ( 𝐵 − 𝐴 ) ) = ( ( 𝐵 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) )
42 2times ⊢ ( 𝐵 ∈ ℂ → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
43 42 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
44 39 41 43 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + ( 𝐵 − 𝐴 ) ) = ( 2 · 𝐵 ) )
45 1 14 44 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) + ( 𝐵 − 𝐴 ) ) = ( 2 · 𝐵 ) )
46 45 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 + 𝐵 ) + ( 𝐵 − 𝐴 ) ) = ( 2 · 𝐵 ) )
47 36 46 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) = ( 2 · 𝐵 ) )
48 47 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) = ( ( 2 · 𝐵 ) / 2 ) )
49 iftrue ⊢ ( 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
50 49 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
51 33 48 50 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) )
52 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
53 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
54 29 51 52 53 ltlecasei ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = ( ( ( 𝐴 + 𝐵 ) + ( abs ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) )