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 ) )