Theorem avgle

Description: The average of two numbers is less than or equal to at least one of them. (Contributed by NM, 9-Dec-2005) (Revised by Mario Carneiro, 28-May-2014)

	Ref	Expression
Assertion	avgle	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\frac{A+B}{2}\le A\vee \frac{A+B}{2}\le B\right)$$

Proof

Step	Hyp	Ref	Expression
1		letric	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\vee B\le A\right)$$
2	1	orcomd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B\le A\vee A\le B\right)$$
3		avgle2	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B\le A\leftrightarrow \frac{B+A}{2}\le A\right)$$
4	3	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B\le A\leftrightarrow \frac{B+A}{2}\le A\right)$$
5		recn	$$⊢A\in ℝ\to A\in ℂ$$
6		recn	$$⊢B\in ℝ\to B\in ℂ$$
7		addcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B=B+A$$
8	5 6 7	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B=B+A$$
9	8	oveq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \frac{A+B}{2}=\frac{B+A}{2}$$
10	9	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\frac{A+B}{2}\le A\leftrightarrow \frac{B+A}{2}\le A\right)$$
11	4 10	bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B\le A\leftrightarrow \frac{A+B}{2}\le A\right)$$
12		avgle2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \frac{A+B}{2}\le B\right)$$
13	11 12	orbi12d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(B\le A\vee A\le B\right)\leftrightarrow \left(\frac{A+B}{2}\le A\vee \frac{A+B}{2}\le B\right)\right)$$
14	2 13	mpbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\frac{A+B}{2}\le A\vee \frac{A+B}{2}\le B\right)$$