Metamath Proof Explorer

Theorem sgnmulrp2

Description: Multiplication by a positive number does not affect signum. (Contributed by Thierry Arnoux, 2-Oct-2018)

Ref Expression
Assertion sgnmulrp2 
|- ( ( A e. RR /\ B e. RR+ ) -> ( sgn ` ( A x. B ) ) = ( sgn ` A ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR+ )
2 1 rpred 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
3 sgnmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( sgn ` ( A x. B ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
4 2 3 syldan 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( sgn ` ( A x. B ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
5 1 rpxrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR* )
6 1 rpgt0d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> 0 < B )
7 sgnp 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( sgn ` B ) = 1 )
8 5 6 7 syl2anc 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( sgn ` B ) = 1 )
9 8 oveq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( sgn ` A ) x. ( sgn ` B ) ) = ( ( sgn ` A ) x. 1 ) )
10 simpl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. RR )
11 sgnclre 
 |-  ( A e. RR -> ( sgn ` A ) e. RR )
12 ax-1rid 
 |-  ( ( sgn ` A ) e. RR -> ( ( sgn ` A ) x. 1 ) = ( sgn ` A ) )
13 10 11 12 3syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( sgn ` A ) x. 1 ) = ( sgn ` A ) )
14 4 9 13 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( sgn ` ( A x. B ) ) = ( sgn ` A ) )