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 ) )