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	$$⊢\phi \to A\in ℝ$$
	lt2addrd.2	$$⊢\phi \to B\in ℝ$$
	lt2addrd.3	$$⊢\phi \to C\in ℝ$$
	lt2addrd.4	$$⊢\phi \to A<B+C$$
Assertion	lt2addrd	$$⊢\phi \to \exists b\in ℝ\exists c\in ℝ\left(A=b+c\wedge b<B\wedge c<C\right)$$

Proof

Step	Hyp	Ref	Expression
1		lt2addrd.1	$$⊢\phi \to A\in ℝ$$
2		lt2addrd.2	$$⊢\phi \to B\in ℝ$$
3		lt2addrd.3	$$⊢\phi \to C\in ℝ$$
4		lt2addrd.4	$$⊢\phi \to A<B+C$$
5	2 3	readdcld	$$⊢\phi \to B+C\in ℝ$$
6	5 1	resubcld	$$⊢\phi \to B+C-A\in ℝ$$
7	6	rehalfcld	$$⊢\phi \to \frac{B+C-A}{2}\in ℝ$$
8	2 7	resubcld	$$⊢\phi \to B-\left(\frac{B+C-A}{2}\right)\in ℝ$$
9	3 7	resubcld	$$⊢\phi \to C-\left(\frac{B+C-A}{2}\right)\in ℝ$$
10	3	recnd	$$⊢\phi \to C\in ℂ$$
11	2	recnd	$$⊢\phi \to B\in ℂ$$
12	11 10	addcld	$$⊢\phi \to B+C\in ℂ$$
13	1	recnd	$$⊢\phi \to A\in ℂ$$
14	12 13	subcld	$$⊢\phi \to B+C-A\in ℂ$$
15	14	halfcld	$$⊢\phi \to \frac{B+C-A}{2}\in ℂ$$
16	10 15 15	subsub4d	$$⊢\phi \to C-\left(\frac{B+C-A}{2}\right)-\left(\frac{B+C-A}{2}\right)=C-\left(\left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\right)$$
17	16	oveq2d	$$⊢\phi \to B+\left(C-\left(\frac{B+C-A}{2}\right)\right)-\left(\frac{B+C-A}{2}\right)=B+C-\left(\left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\right)$$
18	10 15	subcld	$$⊢\phi \to C-\left(\frac{B+C-A}{2}\right)\in ℂ$$
19	11 15 18	subadd23d	$$⊢\phi \to \left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)=B+\left(C-\left(\frac{B+C-A}{2}\right)\right)-\left(\frac{B+C-A}{2}\right)$$
20	14	2halvesd	$$⊢\phi \to \left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)=B+C-A$$
21	20 14	eqeltrd	$$⊢\phi \to \left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\in ℂ$$
22	11 10 21	addsubassd	$$⊢\phi \to B+C-\left(\left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\right)=B+C-\left(\left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\right)$$
23	17 19 22	3eqtr4d	$$⊢\phi \to \left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)=B+C-\left(\left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\right)$$
24	20	oveq2d	$$⊢\phi \to B+C-\left(\left(\frac{B+C-A}{2}\right)+\left(\frac{B+C-A}{2}\right)\right)=B+C-\left(B+C-A\right)$$
25	12 13	nncand	$$⊢\phi \to B+C-\left(B+C-A\right)=A$$
26	23 24 25	3eqtrrd	$$⊢\phi \to A=\left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)$$
27		difrp	$$⊢\left(A\in ℝ\wedge B+C\in ℝ\right)\to \left(A<B+C\leftrightarrow B+C-A\in {ℝ}^{+}\right)$$
28	1 5 27	syl2anc	$$⊢\phi \to \left(A<B+C\leftrightarrow B+C-A\in {ℝ}^{+}\right)$$
29	4 28	mpbid	$$⊢\phi \to B+C-A\in {ℝ}^{+}$$
30	29	rphalfcld	$$⊢\phi \to \frac{B+C-A}{2}\in {ℝ}^{+}$$
31	2 30	ltsubrpd	$$⊢\phi \to B-\left(\frac{B+C-A}{2}\right)<B$$
32	3 30	ltsubrpd	$$⊢\phi \to C-\left(\frac{B+C-A}{2}\right)<C$$
33		oveq1	$$⊢b=B-\left(\frac{B+C-A}{2}\right)\to b+c=B-\left(\frac{B+C-A}{2}\right)+c$$
34	33	eqeq2d	$$⊢b=B-\left(\frac{B+C-A}{2}\right)\to \left(A=b+c\leftrightarrow A=B-\left(\frac{B+C-A}{2}\right)+c\right)$$
35		breq1	$$⊢b=B-\left(\frac{B+C-A}{2}\right)\to \left(b<B\leftrightarrow B-\left(\frac{B+C-A}{2}\right)<B\right)$$
36	34 35	3anbi12d	$$⊢b=B-\left(\frac{B+C-A}{2}\right)\to \left(\left(A=b+c\wedge b<B\wedge c<C\right)\leftrightarrow \left(A=B-\left(\frac{B+C-A}{2}\right)+c\wedge B-\left(\frac{B+C-A}{2}\right)<B\wedge c<C\right)\right)$$
37		oveq2	$$⊢c=C-\left(\frac{B+C-A}{2}\right)\to B-\left(\frac{B+C-A}{2}\right)+c=\left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)$$
38	37	eqeq2d	$$⊢c=C-\left(\frac{B+C-A}{2}\right)\to \left(A=B-\left(\frac{B+C-A}{2}\right)+c\leftrightarrow A=\left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)\right)$$
39		breq1	$$⊢c=C-\left(\frac{B+C-A}{2}\right)\to \left(c<C\leftrightarrow C-\left(\frac{B+C-A}{2}\right)<C\right)$$
40	38 39	3anbi13d	$$⊢c=C-\left(\frac{B+C-A}{2}\right)\to \left(\left(A=B-\left(\frac{B+C-A}{2}\right)+c\wedge B-\left(\frac{B+C-A}{2}\right)<B\wedge c<C\right)\leftrightarrow \left(A=\left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)\wedge B-\left(\frac{B+C-A}{2}\right)<B\wedge C-\left(\frac{B+C-A}{2}\right)<C\right)\right)$$
41	36 40	rspc2ev	$$⊢\left(B-\left(\frac{B+C-A}{2}\right)\in ℝ\wedge C-\left(\frac{B+C-A}{2}\right)\in ℝ\wedge \left(A=\left(B-\left(\frac{B+C-A}{2}\right)\right)+C-\left(\frac{B+C-A}{2}\right)\wedge B-\left(\frac{B+C-A}{2}\right)<B\wedge C-\left(\frac{B+C-A}{2}\right)<C\right)\right)\to \exists b\in ℝ\exists c\in ℝ\left(A=b+c\wedge b<B\wedge c<C\right)$$
42	8 9 26 31 32 41	syl113anc	$$⊢\phi \to \exists b\in ℝ\exists c\in ℝ\left(A=b+c\wedge b<B\wedge c<C\right)$$