Metamath Proof Explorer

Theorem sgnmulsgn

Description: If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 neg1lt0 
 |-  -u 1 < 0
2 breq1 
 |-  ( ( sgn ` ( A x. B ) ) = -u 1 -> ( ( sgn ` ( A x. B ) ) < 0 <-> -u 1 < 0 ) )
3 1 2 mpbiri 
 |-  ( ( sgn ` ( A x. B ) ) = -u 1 -> ( sgn ` ( A x. B ) ) < 0 )
4 3 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> ( sgn ` ( A x. B ) ) < 0 )
5 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> ( sgn ` ( A x. B ) ) = -u 1 )
6 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) = 0 )
7 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) < 0 )
8 7 lt0ne0d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) =/= 0 )
9 6 8 pm2.21ddne 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) = -u 1 )
10 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> ( sgn ` ( A x. B ) ) = 1 )
11 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> ( sgn ` ( A x. B ) ) < 0 )
12 10 11 eqbrtrrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> 1 < 0 )
13 1nn0 
 |-  1 e. NN0
14 nn0nlt0 
 |-  ( 1 e. NN0 -> -. 1 < 0 )
15 13 14 mp1i 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> -. 1 < 0 )
16 12 15 pm2.21dd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> ( sgn ` ( A x. B ) ) = -u 1 )
17 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
18 17 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR* )
19 18 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) -> ( A x. B ) e. RR* )
20 sgncl 
 |-  ( ( A x. B ) e. RR* -> ( sgn ` ( A x. B ) ) e. { -u 1 , 0 , 1 } )
21 eltpi 
 |-  ( ( sgn ` ( A x. B ) ) e. { -u 1 , 0 , 1 } -> ( ( sgn ` ( A x. B ) ) = -u 1 \/ ( sgn ` ( A x. B ) ) = 0 \/ ( sgn ` ( A x. B ) ) = 1 ) )
22 19 20 21 3syl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) -> ( ( sgn ` ( A x. B ) ) = -u 1 \/ ( sgn ` ( A x. B ) ) = 0 \/ ( sgn ` ( A x. B ) ) = 1 ) )
23 5 9 16 22 mpjao3dan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) < 0 ) -> ( sgn ` ( A x. B ) ) = -u 1 )
24 4 23 impbida 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( sgn ` ( A x. B ) ) = -u 1 <-> ( sgn ` ( A x. B ) ) < 0 ) )
25 sgnnbi 
 |-  ( ( A x. B ) e. RR* -> ( ( sgn ` ( A x. B ) ) = -u 1 <-> ( A x. B ) < 0 ) )
26 18 25 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( sgn ` ( A x. B ) ) = -u 1 <-> ( A x. B ) < 0 ) )
27 sgnmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( sgn ` ( A x. B ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
28 27 breq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( sgn ` ( A x. B ) ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` B ) ) < 0 ) )
29 24 26 28 3bitr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) < 0 <-> ( ( sgn ` A ) x. ( sgn ` B ) ) < 0 ) )