Theorem avgle1

Description: Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		avglt2	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B<A\leftrightarrow \frac{B+A}{2}<A\right)$$
2	1	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B<A\leftrightarrow \frac{B+A}{2}<A\right)$$
3		recn	$$⊢A\in ℝ\to A\in ℂ$$
4		recn	$$⊢B\in ℝ\to B\in ℂ$$
5		addcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B=B+A$$
6	3 4 5	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B=B+A$$
7	6	oveq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \frac{A+B}{2}=\frac{B+A}{2}$$
8	7	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\frac{A+B}{2}<A\leftrightarrow \frac{B+A}{2}<A\right)$$
9	2 8	bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B<A\leftrightarrow \frac{A+B}{2}<A\right)$$
10	9	notbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\neg B<A\leftrightarrow \neg \frac{A+B}{2}<A\right)$$
11		lenlt	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \neg B<A\right)$$
12		readdcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B\in ℝ$$
13		rehalfcl	$$⊢A+B\in ℝ\to \frac{A+B}{2}\in ℝ$$
14	12 13	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \frac{A+B}{2}\in ℝ$$
15		lenlt	$$⊢\left(A\in ℝ\wedge \frac{A+B}{2}\in ℝ\right)\to \left(A\le \frac{A+B}{2}\leftrightarrow \neg \frac{A+B}{2}<A\right)$$
16	14 15	syldan	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le \frac{A+B}{2}\leftrightarrow \neg \frac{A+B}{2}<A\right)$$
17	10 11 16	3bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow A\le \frac{A+B}{2}\right)$$