Metamath Proof Explorer

Theorem sgnsub

Description: Subtraction of a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018)

Ref Expression
Assertion sgnsub 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> ( sgn ` ( A - B ) ) = ( sgn ` A ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> A e. RR )
2 1 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> A e. RR* )
3 eqeq2 
 |-  ( ( sgn ` A ) = 0 -> ( ( sgn ` ( A - B ) ) = ( sgn ` A ) <-> ( sgn ` ( A - B ) ) = 0 ) )
4 eqeq2 
 |-  ( ( sgn ` A ) = 1 -> ( ( sgn ` ( A - B ) ) = ( sgn ` A ) <-> ( sgn ` ( A - B ) ) = 1 ) )
5 eqeq2 
 |-  ( ( sgn ` A ) = -u 1 -> ( ( sgn ` ( A - B ) ) = ( sgn ` A ) <-> ( sgn ` ( A - B ) ) = -u 1 ) )
6 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> A = 0 )
7 1 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> A e. CC )
8 7 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> A e. CC )
9 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> B e. RR )
10 9 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> B e. CC )
11 10 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> B e. CC )
12 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> ( A x. B ) < 0 )
13 12 lt0ne0d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> ( A x. B ) =/= 0 )
14 8 11 13 mulne0bad 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> A =/= 0 )
15 6 14 pm2.21ddne 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A = 0 ) -> ( sgn ` ( A - B ) ) = 0 )
16 simplll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> A e. RR )
17 simpllr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> B e. RR )
18 16 17 resubcld 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> ( A - B ) e. RR )
19 18 rexrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> ( A - B ) e. RR* )
20 0red 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> 0 e. RR )
21 simpr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> ( A x. B ) < 0 )
22 1 9 21 mul2lt0lgt0 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> B < 0 )
23 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> 0 < A )
24 17 20 16 22 23 lttrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> B < A )
25 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
26 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
27 25 26 posdifd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A <-> 0 < ( A - B ) ) )
28 27 biimpa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> 0 < ( A - B ) )
29 16 17 24 28 syl21anc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> 0 < ( A - B ) )
30 sgnp 
 |-  ( ( ( A - B ) e. RR* /\ 0 < ( A - B ) ) -> ( sgn ` ( A - B ) ) = 1 )
31 19 29 30 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ 0 < A ) -> ( sgn ` ( A - B ) ) = 1 )
32 simplll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A e. RR )
33 simpllr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> B e. RR )
34 32 33 resubcld 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A - B ) e. RR )
35 34 rexrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A - B ) e. RR* )
36 0red 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> 0 e. RR )
37 7 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A e. CC )
38 37 subid1d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A - 0 ) = A )
39 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A < 0 )
40 1 9 21 mul2lt0llt0 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> 0 < B )
41 32 36 33 39 40 lttrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A < B )
42 38 41 eqbrtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A - 0 ) < B )
43 32 36 33 42 ltsub23d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A - B ) < 0 )
44 sgnn 
 |-  ( ( ( A - B ) e. RR* /\ ( A - B ) < 0 ) -> ( sgn ` ( A - B ) ) = -u 1 )
45 35 43 44 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( sgn ` ( A - B ) ) = -u 1 )
46 2 3 4 5 15 31 45 sgn3da 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A x. B ) < 0 ) -> ( sgn ` ( A - B ) ) = ( sgn ` A ) )