Theorem lt2addrd 27432

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
lt2addrd	|- ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )

Distinct variable groups:   b, c, A   B, b, c   C, b, c

Allowed substitution hints:   ph( b, c)

Proof of Theorem lt2addrd

Step	Hyp	Ref	Expression
1		lt2addrd.2	. . 3 |- ( ph -> B e. RR )
2		lt2addrd.3	. . . . . 6 |- ( ph -> C e. RR )
3	1, 2	readdcld 9623	. . . . 5 |- ( ph -> ( B + C ) e. RR )
4		lt2addrd.1	. . . . 5 |- ( ph -> A e. RR )
5	3, 4	resubcld 9990	. . . 4 |- ( ph -> ( ( B + C ) - A ) e. RR )
6	5	rehalfcld 10788	. . 3 |- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR )
7	1, 6	resubcld 9990	. 2 |- ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
8	2, 6	resubcld 9990	. 2 |- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
9	2	recnd 9622	. . . . . 6 |- ( ph -> C e. CC )
10	1	recnd 9622	. . . . . . . . 9 |- ( ph -> B e. CC )
11	10, 9	addcld 9615	. . . . . . . 8 |- ( ph -> ( B + C ) e. CC )
12	4	recnd 9622	. . . . . . . 8 |- ( ph -> A e. CC )
13	11, 12	subcld 9933	. . . . . . 7 |- ( ph -> ( ( B + C ) - A ) e. CC )
14	13	halfcld 10786	. . . . . 6 |- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. CC )
15	9, 14, 14	subsub4d 9964	. . . . 5 |- ( ph -> ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) = ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
16	15	oveq2d 6294	. . . 4 |- ( ph -> ( B + ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) ) )
17	9, 14	subcld 9933	. . . . 5 |- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. CC )
18	10, 14, 17	subadd23d 9955	. . . 4 |- ( ph -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) ) )
19	13	2halvesd 10787	. . . . . 6 |- ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) = ( ( B + C ) - A ) )
20	19, 13	eqeltrd 2529	. . . . 5 |- ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) e. CC )
21	10, 9, 20	addsubassd 9953	. . . 4 |- ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) ) )
22	16, 18, 21	3eqtr4d 2492	. . 3 |- ( ph -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
23	19	oveq2d 6294	. . 3 |- ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( B + C ) - A ) ) )
24	11, 12	nncand 9938	. . 3 |- ( ph -> ( ( B + C ) - ( ( B + C ) - A ) ) = A )
25	22, 23, 24	3eqtrrd 2487	. 2 |- ( ph -> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) )
26		lt2addrd.4	. . . . 5 |- ( ph -> A < ( B + C ) )
27		difrp 11259	. . . . . 6 |- ( ( A e. RR /\ ( B + C ) e. RR ) -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
28	4, 3, 27	syl2anc 661	. . . . 5 |- ( ph -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
29	26, 28	mpbid 210	. . . 4 |- ( ph -> ( ( B + C ) - A ) e. RR+ )
30	29	rphalfcld 11274	. . 3 |- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR+ )
31	1, 30	ltsubrpd 11290	. 2 |- ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B )
32	2, 30	ltsubrpd 11290	. 2 |- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C )
33		oveq1 6285	. . . . 5 |- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b + c ) = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) )
34	33	eqeq2d 2455	. . . 4 |- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( A = ( b + c ) <-> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) ) )
35		breq1 4437	. . . 4 |- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b < B <-> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B ) )
36	34, 35	3anbi12d 1299	. . 3 |- ( 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 6286	. . . . 5 |- ( 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 2455	. . . 4 |- ( 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 4437	. . . 4 |- ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( c < C <-> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C ) )
40	38, 39	3anbi13d 1300	. . 3 |- ( 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 3205	. 2 |- ( ( ( 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	7, 8, 25, 31, 32, 41	syl113anc 1239	1 |- ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 972   = wceq 1381   e. wcel 1802   E.wrex 2792   class class class wbr 4434  (class class class)co 6278   CCcc 9490   RRcr 9491   + caddc 9495   < clt 9628   - cmin 9807   / cdiv 10209   2c2 10588   RR+crp 11226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-po 4787  df-so 4788  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-er 7310  df-en 7516  df-dom 7517  df-sdom 7518  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9809  df-neg 9810  df-div 10210  df-2 10597  df-rp 11227

This theorem is referenced by:  xlt2addrd  27447