Theorem lt2addrd

Description: If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017)

	Ref	Expression
Hypotheses	lt2addrd.1	|- ( ph -> A e. RR )
	lt2addrd.2	|- ( ph -> B e. RR )
	lt2addrd.3	|- ( ph -> C e. RR )
	lt2addrd.4	|- ( ph -> A < ( B + C ) )
Assertion	lt2addrd	|- ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )

Proof

Step	Hyp	Ref	Expression
1		lt2addrd.1	|- ( ph -> A e. RR )
2		lt2addrd.2	|- ( ph -> B e. RR )
3		lt2addrd.3	|- ( ph -> C e. RR )
4		lt2addrd.4	|- ( ph -> A < ( B + C ) )
5	2 3	readdcld	|- ( ph -> ( B + C ) e. RR )
6	5 1	resubcld	|- ( ph -> ( ( B + C ) - A ) e. RR )
7	6	rehalfcld	|- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR )
8	2 7	resubcld	|- ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
9	3 7	resubcld	|- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
10	3	recnd	|- ( ph -> C e. CC )
11	2	recnd	|- ( ph -> B e. CC )
12	11 10	addcld	|- ( ph -> ( B + C ) e. CC )
13	1	recnd	|- ( ph -> A e. CC )
14	12 13	subcld	|- ( ph -> ( ( B + C ) - A ) e. CC )
15	14	halfcld	|- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. CC )
16	10 15 15	subsub4d	|- ( ph -> ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) = ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
17	16	oveq2d	|- ( ph -> ( B + ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) ) )
18	10 15	subcld	|- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. CC )
19	11 15 18	subadd23d	|- ( ph -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) ) )
20	14	2halvesd	|- ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) = ( ( B + C ) - A ) )
21	20 14	eqeltrd	|- ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) e. CC )
22	11 10 21	addsubassd	|- ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) ) )
23	17 19 22	3eqtr4d	|- ( ph -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
24	20	oveq2d	|- ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( B + C ) - A ) ) )
25	12 13	nncand	|- ( ph -> ( ( B + C ) - ( ( B + C ) - A ) ) = A )
26	23 24 25	3eqtrrd	|- ( ph -> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) )
27		difrp	|- ( ( A e. RR /\ ( B + C ) e. RR ) -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
28	1 5 27	syl2anc	|- ( ph -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
29	4 28	mpbid	|- ( ph -> ( ( B + C ) - A ) e. RR+ )
30	29	rphalfcld	|- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR+ )
31	2 30	ltsubrpd	|- ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B )
32	3 30	ltsubrpd	|- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C )
33		oveq1	|- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b + c ) = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) )
34	33	eqeq2d	|- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( A = ( b + c ) <-> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) ) )
35		breq1	|- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b < B <-> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B ) )
36	34 35	3anbi12d	|- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( ( A = ( b + c ) /\ b < B /\ c < C ) <-> ( A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) /\ ( B - ( ( ( B + C ) - A ) / 2 ) ) < B /\ c < C ) ) )
37		oveq2	|- ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) )
38	37	eqeq2d	|- ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) <-> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) ) )
39		breq1	|- ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( c < C <-> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C ) )
40	38 39	3anbi13d	|- ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( ( A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) /\ ( B - ( ( ( B + C ) - A ) / 2 ) ) < B /\ c < C ) <-> ( A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) /\ ( B - ( ( ( B + C ) - A ) / 2 ) ) < B /\ ( C - ( ( ( B + C ) - A ) / 2 ) ) < C ) ) )
41	36 40	rspc2ev	|- ( ( ( B - ( ( ( B + C ) - A ) / 2 ) ) e. RR /\ ( C - ( ( ( B + C ) - A ) / 2 ) ) e. RR /\ ( A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) /\ ( B - ( ( ( B + C ) - A ) / 2 ) ) < B /\ ( C - ( ( ( B + C ) - A ) / 2 ) ) < C ) ) -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )
42	8 9 26 31 32 41	syl113anc	|- ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )