Metamath Proof Explorer

Theorem absmax

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

Ref Expression
Assertion absmax ⊢ A ∈ ℝ ∧ B ∈ ℝ → if A ≤ B B A = A + B + A − B 2

Proof

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