This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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