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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	lt2addrd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	lt2addrd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	lt2addrd.4	⊢ ( 𝜑 → 𝐴 < ( 𝐵 + 𝐶 ) )
Assertion	lt2addrd	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ( 𝐴 = ( 𝑏 + 𝑐 ) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		lt2addrd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		lt2addrd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		lt2addrd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		lt2addrd.4	⊢ ( 𝜑 → 𝐴 < ( 𝐵 + 𝐶 ) )
5	2 3	readdcld	⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) ∈ ℝ )
6	5 1	resubcld	⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − 𝐴 ) ∈ ℝ )
7	6	rehalfcld	⊢ ( 𝜑 → ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ∈ ℝ )
8	2 7	resubcld	⊢ ( 𝜑 → ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ∈ ℝ )
9	3 7	resubcld	⊢ ( 𝜑 → ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ∈ ℝ )
10	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
11	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
12	11 10	addcld	⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) ∈ ℂ )
13	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
14	12 13	subcld	⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − 𝐴 ) ∈ ℂ )
15	14	halfcld	⊢ ( 𝜑 → ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ∈ ℂ )
16	10 15 15	subsub4d	⊢ ( 𝜑 → ( ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) = ( 𝐶 − ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) )
17	16	oveq2d	⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) = ( 𝐵 + ( 𝐶 − ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) ) )
18	10 15	subcld	⊢ ( 𝜑 → ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ∈ ℂ )
19	11 15 18	subadd23d	⊢ ( 𝜑 → ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) = ( 𝐵 + ( ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) )
20	14	2halvesd	⊢ ( 𝜑 → ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) = ( ( 𝐵 + 𝐶 ) − 𝐴 ) )
21	20 14	eqeltrd	⊢ ( 𝜑 → ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ∈ ℂ )
22	11 10 21	addsubassd	⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) = ( 𝐵 + ( 𝐶 − ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) ) )
23	17 19 22	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) = ( ( 𝐵 + 𝐶 ) − ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) )
24	20	oveq2d	⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − ( ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) + ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) = ( ( 𝐵 + 𝐶 ) − ( ( 𝐵 + 𝐶 ) − 𝐴 ) ) )
25	12 13	nncand	⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − ( ( 𝐵 + 𝐶 ) − 𝐴 ) ) = 𝐴 )
26	23 24 25	3eqtrrd	⊢ ( 𝜑 → 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) )
27		difrp	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ) → ( 𝐴 < ( 𝐵 + 𝐶 ) ↔ ( ( 𝐵 + 𝐶 ) − 𝐴 ) ∈ ℝ+ ) )
28	1 5 27	syl2anc	⊢ ( 𝜑 → ( 𝐴 < ( 𝐵 + 𝐶 ) ↔ ( ( 𝐵 + 𝐶 ) − 𝐴 ) ∈ ℝ+ ) )
29	4 28	mpbid	⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − 𝐴 ) ∈ ℝ+ )
30	29	rphalfcld	⊢ ( 𝜑 → ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ∈ ℝ+ )
31	2 30	ltsubrpd	⊢ ( 𝜑 → ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐵 )
32	3 30	ltsubrpd	⊢ ( 𝜑 → ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐶 )
33		oveq1	⊢ ( 𝑏 = ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( 𝑏 + 𝑐 ) = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + 𝑐 ) )
34	33	eqeq2d	⊢ ( 𝑏 = ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( 𝐴 = ( 𝑏 + 𝑐 ) ↔ 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + 𝑐 ) ) )
35		breq1	⊢ ( 𝑏 = ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( 𝑏 < 𝐵 ↔ ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐵 ) )
36	34 35	3anbi12d	⊢ ( 𝑏 = ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( ( 𝐴 = ( 𝑏 + 𝑐 ) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶 ) ↔ ( 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + 𝑐 ) ∧ ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐵 ∧ 𝑐 < 𝐶 ) ) )
37		oveq2	⊢ ( 𝑐 = ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + 𝑐 ) = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) )
38	37	eqeq2d	⊢ ( 𝑐 = ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + 𝑐 ) ↔ 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) ) )
39		breq1	⊢ ( 𝑐 = ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( 𝑐 < 𝐶 ↔ ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐶 ) )
40	38 39	3anbi13d	⊢ ( 𝑐 = ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) → ( ( 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + 𝑐 ) ∧ ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐵 ∧ 𝑐 < 𝐶 ) ↔ ( 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) ∧ ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐵 ∧ ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐶 ) ) )
41	36 40	rspc2ev	⊢ ( ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ∈ ℝ ∧ ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ∈ ℝ ∧ ( 𝐴 = ( ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) + ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) ) ∧ ( 𝐵 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐵 ∧ ( 𝐶 − ( ( ( 𝐵 + 𝐶 ) − 𝐴 ) / 2 ) ) < 𝐶 ) ) → ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ( 𝐴 = ( 𝑏 + 𝑐 ) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶 ) )
42	8 9 26 31 32 41	syl113anc	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ( 𝐴 = ( 𝑏 + 𝑐 ) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶 ) )