Theorem avgle1

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

	Ref	Expression
Assertion	avgle1	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A <_ ( ( A + B ) / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		avglt2	|- ( ( B e. RR /\ A e. RR ) -> ( B < A <-> ( ( B + A ) / 2 ) < A ) )
2	1	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( B < A <-> ( ( B + A ) / 2 ) < A ) )
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	breq1d	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < A <-> ( ( B + A ) / 2 ) < A ) )
9	2 8	bitr4d	|- ( ( A e. RR /\ B e. RR ) -> ( B < A <-> ( ( A + B ) / 2 ) < A ) )
10	9	notbid	|- ( ( A e. RR /\ B e. RR ) -> ( -. B < A <-> -. ( ( A + B ) / 2 ) < A ) )
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 e. RR /\ ( ( A + B ) / 2 ) e. RR ) -> ( A <_ ( ( A + B ) / 2 ) <-> -. ( ( A + B ) / 2 ) < A ) )
16	14 15	syldan	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ ( ( A + B ) / 2 ) <-> -. ( ( A + B ) / 2 ) < A ) )
17	10 11 16	3bitr4d	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A <_ ( ( A + B ) / 2 ) ) )