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	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( ( A + B ) / 2 ) <_ B ) )

Proof

Step	Hyp	Ref	Expression
1		avglt1	|- ( ( B e. RR /\ A e. RR ) -> ( B < A <-> B < ( ( B + A ) / 2 ) ) )
2	1	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( B < A <-> B < ( ( B + A ) / 2 ) ) )
3		recn	|- ( A e. RR -> A e. CC )
4		recn	|- ( B e. RR -> B e. CC )
5		addcom	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
6	3 4 5	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
7	6	oveq1d	|- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) = ( ( B + A ) / 2 ) )
8	7	breq2d	|- ( ( A e. RR /\ B e. RR ) -> ( B < ( ( A + B ) / 2 ) <-> B < ( ( B + A ) / 2 ) ) )
9	2 8	bitr4d	|- ( ( A e. RR /\ B e. RR ) -> ( B < A <-> B < ( ( A + B ) / 2 ) ) )
10	9	notbid	|- ( ( A e. RR /\ B e. RR ) -> ( -. B < A <-> -. B < ( ( A + B ) / 2 ) ) )
11		lenlt	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
12		readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
13		rehalfcl	|- ( ( A + B ) e. RR -> ( ( A + B ) / 2 ) e. RR )
14	12 13	syl	|- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) e. RR )
15		lenlt	|- ( ( ( ( A + B ) / 2 ) e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) <_ B <-> -. B < ( ( A + B ) / 2 ) ) )
16	14 15	sylancom	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) <_ B <-> -. B < ( ( A + B ) / 2 ) ) )
17	10 11 16	3bitr4d	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( ( A + B ) / 2 ) <_ B ) )