Theorem avglt1

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

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

Proof

Step	Hyp	Ref	Expression
1		ltadd2	|- ( ( A e. RR /\ B e. RR /\ A e. RR ) -> ( A < B <-> ( A + A ) < ( A + B ) ) )
2	1	3anidm13	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A + A ) < ( A + B ) ) )
3		simpl	|- ( ( A e. RR /\ B e. RR ) -> A e. RR )
4	3	recnd	|- ( ( A e. RR /\ B e. RR ) -> A e. CC )
5		times2	|- ( A e. CC -> ( A x. 2 ) = ( A + A ) )
6	4 5	syl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. 2 ) = ( A + A ) )
7	6	breq1d	|- ( ( A e. RR /\ B e. RR ) -> ( ( A x. 2 ) < ( A + B ) <-> ( A + A ) < ( A + B ) ) )
8		readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
9		2re	|- 2 e. RR
10		2pos	|- 0 < 2
11	9 10	pm3.2i	|- ( 2 e. RR /\ 0 < 2 )
12	11	a1i	|- ( ( A e. RR /\ B e. RR ) -> ( 2 e. RR /\ 0 < 2 ) )
13		ltmuldiv	|- ( ( A e. RR /\ ( A + B ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( A x. 2 ) < ( A + B ) <-> A < ( ( A + B ) / 2 ) ) )
14	3 8 12 13	syl3anc	|- ( ( A e. RR /\ B e. RR ) -> ( ( A x. 2 ) < ( A + B ) <-> A < ( ( A + B ) / 2 ) ) )
15	2 7 14	3bitr2d	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )