Theorem avgle2

Description: Ordering property for average. (Contributed by Jeff Hankins, 15-Sep-2013) (Revised by Mario Carneiro, 28-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		avglt1	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B<A\leftrightarrow B<\frac{B+A}{2}\right)$$
2	1	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B<A\leftrightarrow B<\frac{B+A}{2}\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	breq2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B<\frac{A+B}{2}\leftrightarrow B<\frac{B+A}{2}\right)$$
9	2 8	bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B<A\leftrightarrow B<\frac{A+B}{2}\right)$$
10	9	notbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\neg B<A\leftrightarrow \neg B<\frac{A+B}{2}\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(\frac{A+B}{2}\in ℝ\wedge B\in ℝ\right)\to \left(\frac{A+B}{2}\le B\leftrightarrow \neg B<\frac{A+B}{2}\right)$$
16	14 15	sylancom	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\frac{A+B}{2}\le B\leftrightarrow \neg B<\frac{A+B}{2}\right)$$
17	10 11 16	3bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \frac{A+B}{2}\le B\right)$$