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