Theorem lt2addrd 27713

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 9534	. . . . 5 |- ( ph -> ( B + C ) e. RR )
4		lt2addrd.1	. . . . 5 |- ( ph -> A e. RR )
5	3, 4	resubcld 9905	. . . 4 |- ( ph -> ( ( B + C ) - A ) e. RR )
6	5	rehalfcld 10702	. . 3 |- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR )
7	1, 6	resubcld 9905	. 2 |- ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
8	2, 6	resubcld 9905	. 2 |- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
9	2	recnd 9533	. . . . . 6 |- ( ph -> C e. CC )
10	1	recnd 9533	. . . . . . . . 9 |- ( ph -> B e. CC )
11	10, 9	addcld 9526	. . . . . . . 8 |- ( ph -> ( B + C ) e. CC )
12	4	recnd 9533	. . . . . . . 8 |- ( ph -> A e. CC )
13	11, 12	subcld 9844	. . . . . . 7 |- ( ph -> ( ( B + C ) - A ) e. CC )
14	13	halfcld 10700	. . . . . 6 |- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. CC )
15	9, 14, 14	subsub4d 9875	. . . . 5 |- ( ph -> ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) = ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
16	15	oveq2d 6212	. . . 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 9844	. . . . 5 |- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. CC )
18	10, 14, 17	subadd23d 9866	. . . 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 10701	. . . . . 6 |- ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) = ( ( B + C ) - A ) )
20	19, 13	eqeltrd 2470	. . . . 5 |- ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) e. CC )
21	10, 9, 20	addsubassd 9864	. . . 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 2433	. . 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 6212	. . 3 |- ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( B + C ) - A ) ) )
24	11, 12	nncand 9849	. . 3 |- ( ph -> ( ( B + C ) - ( ( B + C ) - A ) ) = A )
25	22, 23, 24	3eqtrrd 2428	. 2 |- ( ph -> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) )
26		lt2addrd.4	. . . . 5 |- ( ph -> A < ( B + C ) )
27		difrp 11173	. . . . . 6 |- ( ( A e. RR /\ ( B + C ) e. RR ) -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
28	4, 3, 27	syl2anc 659	. . . . 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 11189	. . 3 |- ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR+ )
31	1, 30	ltsubrpd 11205	. 2 |- ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B )
32	2, 30	ltsubrpd 11205	. 2 |- ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C )
33		oveq1 6203	. . . . 5 |- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b + c ) = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) )
34	33	eqeq2d 2396	. . . 4 |- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( A = ( b + c ) <-> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) ) )
35		breq1 4370	. . . 4 |- ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b < B <-> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B ) )
36	34, 35	3anbi12d 1298	. . 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 6204	. . . . 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 2396	. . . 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 4370	. . . 4 |- ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( c < C <-> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C ) )
40	38, 39	3anbi13d 1299	. . 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 3146	. 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 1238	1 |- ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 971   = wceq 1399   e. wcel 1826   E.wrex 2733   class class class wbr 4367  (class class class)co 6196   CCcc 9401   RRcr 9402   + caddc 9406   < clt 9539   - cmin 9718   / cdiv 10123   2c2 10502   RR+crp 11139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-po 4714  df-so 4715  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-2 10511  df-rp 11140

This theorem is referenced by:  xlt2addrd  27728