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 
|- ( ph -> A e. RR )
lt2addrd.2 
|- ( ph -> B e. RR )
lt2addrd.3 
|- ( ph -> C e. RR )
lt2addrd.4 
|- ( ph -> A < ( B + C ) )
Assertion lt2addrd 
|- ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )

Proof

Step Hyp Ref Expression
1 lt2addrd.1 
 |-  ( ph -> A e. RR )
2 lt2addrd.2 
 |-  ( ph -> B e. RR )
3 lt2addrd.3 
 |-  ( ph -> C e. RR )
4 lt2addrd.4 
 |-  ( ph -> A < ( B + C ) )
5 2 3 readdcld 
 |-  ( ph -> ( B + C ) e. RR )
6 5 1 resubcld 
 |-  ( ph -> ( ( B + C ) - A ) e. RR )
7 6 rehalfcld 
 |-  ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR )
8 2 7 resubcld 
 |-  ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
9 3 7 resubcld 
 |-  ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. RR )
10 3 recnd 
 |-  ( ph -> C e. CC )
11 2 recnd 
 |-  ( ph -> B e. CC )
12 11 10 addcld 
 |-  ( ph -> ( B + C ) e. CC )
13 1 recnd 
 |-  ( ph -> A e. CC )
14 12 13 subcld 
 |-  ( ph -> ( ( B + C ) - A ) e. CC )
15 14 halfcld 
 |-  ( ph -> ( ( ( B + C ) - A ) / 2 ) e. CC )
16 10 15 15 subsub4d 
 |-  ( ph -> ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) = ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
17 16 oveq2d 
 |-  ( ph -> ( B + ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) ) )
18 10 15 subcld 
 |-  ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) e. CC )
19 11 15 18 subadd23d 
 |-  ( ph -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( ( C - ( ( ( B + C ) - A ) / 2 ) ) - ( ( ( B + C ) - A ) / 2 ) ) ) )
20 14 2halvesd 
 |-  ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) = ( ( B + C ) - A ) )
21 20 14 eqeltrd 
 |-  ( ph -> ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) e. CC )
22 11 10 21 addsubassd 
 |-  ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( B + ( C - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) ) )
23 17 19 22 3eqtr4d 
 |-  ( ph -> ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) )
24 20 oveq2d 
 |-  ( ph -> ( ( B + C ) - ( ( ( ( B + C ) - A ) / 2 ) + ( ( ( B + C ) - A ) / 2 ) ) ) = ( ( B + C ) - ( ( B + C ) - A ) ) )
25 12 13 nncand 
 |-  ( ph -> ( ( B + C ) - ( ( B + C ) - A ) ) = A )
26 23 24 25 3eqtrrd 
 |-  ( ph -> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + ( C - ( ( ( B + C ) - A ) / 2 ) ) ) )
27 difrp 
 |-  ( ( A e. RR /\ ( B + C ) e. RR ) -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
28 1 5 27 syl2anc 
 |-  ( ph -> ( A < ( B + C ) <-> ( ( B + C ) - A ) e. RR+ ) )
29 4 28 mpbid 
 |-  ( ph -> ( ( B + C ) - A ) e. RR+ )
30 29 rphalfcld 
 |-  ( ph -> ( ( ( B + C ) - A ) / 2 ) e. RR+ )
31 2 30 ltsubrpd 
 |-  ( ph -> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B )
32 3 30 ltsubrpd 
 |-  ( ph -> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C )
33 oveq1 
 |-  ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b + c ) = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) )
34 33 eqeq2d 
 |-  ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( A = ( b + c ) <-> A = ( ( B - ( ( ( B + C ) - A ) / 2 ) ) + c ) ) )
35 breq1 
 |-  ( b = ( B - ( ( ( B + C ) - A ) / 2 ) ) -> ( b < B <-> ( B - ( ( ( B + C ) - A ) / 2 ) ) < B ) )
36 34 35 3anbi12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( c = ( C - ( ( ( B + C ) - A ) / 2 ) ) -> ( c < C <-> ( C - ( ( ( B + C ) - A ) / 2 ) ) < C ) )
40 38 39 3anbi13d 
 |-  ( 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 
 |-  ( ( ( 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 8 9 26 31 32 41 syl113anc 
 |-  ( ph -> E. b e. RR E. c e. RR ( A = ( b + c ) /\ b < B /\ c < C ) )