Metamath Proof Explorer

Theorem sgnmulsgp

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

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

Proof

Step Hyp Ref Expression
1 0lt1 
 |-  0 < 1
2 breq2 
 |-  ( ( sgn ` ( A x. B ) ) = 1 -> ( 0 < ( sgn ` ( A x. B ) ) <-> 0 < 1 ) )
3 1 2 mpbiri 
 |-  ( ( sgn ` ( A x. B ) ) = 1 -> 0 < ( sgn ` ( A x. B ) ) )
4 3 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> 0 < ( sgn ` ( A x. B ) ) )
5 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> 0 < ( sgn ` ( A x. B ) ) )
6 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> ( sgn ` ( A x. B ) ) = -u 1 )
7 5 6 breqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> 0 < -u 1 )
8 1nn0 
 |-  1 e. NN0
9 nn0nlt0 
 |-  ( 1 e. NN0 -> -. 1 < 0 )
10 8 9 ax-mp 
 |-  -. 1 < 0
11 1re 
 |-  1 e. RR
12 lt0neg1 
 |-  ( 1 e. RR -> ( 1 < 0 <-> 0 < -u 1 ) )
13 11 12 ax-mp 
 |-  ( 1 < 0 <-> 0 < -u 1 )
14 10 13 mtbi 
 |-  -. 0 < -u 1
15 14 a1i 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> -. 0 < -u 1 )
16 7 15 pm2.21dd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = -u 1 ) -> ( sgn ` ( A x. B ) ) = 1 )
17 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) = 0 )
18 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> 0 < ( sgn ` ( A x. B ) ) )
19 18 gt0ne0d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) =/= 0 )
20 17 19 pm2.21ddne 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = 0 ) -> ( sgn ` ( A x. B ) ) = 1 )
21 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) /\ ( sgn ` ( A x. B ) ) = 1 ) -> ( sgn ` ( A x. B ) ) = 1 )
22 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
23 22 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR* )
24 23 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) -> ( A x. B ) e. RR* )
25 sgncl 
 |-  ( ( A x. B ) e. RR* -> ( sgn ` ( A x. B ) ) e. { -u 1 , 0 , 1 } )
26 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 ) )
27 24 25 26 3syl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) -> ( ( sgn ` ( A x. B ) ) = -u 1 \/ ( sgn ` ( A x. B ) ) = 0 \/ ( sgn ` ( A x. B ) ) = 1 ) )
28 16 20 21 27 mpjao3dan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 < ( sgn ` ( A x. B ) ) ) -> ( sgn ` ( A x. B ) ) = 1 )
29 4 28 impbida 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( sgn ` ( A x. B ) ) = 1 <-> 0 < ( sgn ` ( A x. B ) ) ) )
30 sgnpbi 
 |-  ( ( A x. B ) e. RR* -> ( ( sgn ` ( A x. B ) ) = 1 <-> 0 < ( A x. B ) ) )
31 23 30 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( sgn ` ( A x. B ) ) = 1 <-> 0 < ( A x. B ) ) )
32 sgnmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( sgn ` ( A x. B ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
33 32 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( sgn ` ( A x. B ) ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
34 29 31 33 3bitr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )