Metamath Proof Explorer


Theorem prodge0rd

Description: Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005) (Revised by Mario Carneiro, 27-May-2016) (Revised by AV, 9-Jul-2022)

Ref Expression
Hypotheses prodge0rd.1
|- ( ph -> A e. RR+ )
prodge0rd.2
|- ( ph -> B e. RR )
prodge0rd.3
|- ( ph -> 0 <_ ( A x. B ) )
Assertion prodge0rd
|- ( ph -> 0 <_ B )

Proof

Step Hyp Ref Expression
1 prodge0rd.1
 |-  ( ph -> A e. RR+ )
2 prodge0rd.2
 |-  ( ph -> B e. RR )
3 prodge0rd.3
 |-  ( ph -> 0 <_ ( A x. B ) )
4 0red
 |-  ( ph -> 0 e. RR )
5 1 rpred
 |-  ( ph -> A e. RR )
6 5 2 remulcld
 |-  ( ph -> ( A x. B ) e. RR )
7 4 6 3 lensymd
 |-  ( ph -> -. ( A x. B ) < 0 )
8 5 adantr
 |-  ( ( ph /\ 0 < -u B ) -> A e. RR )
9 2 renegcld
 |-  ( ph -> -u B e. RR )
10 9 adantr
 |-  ( ( ph /\ 0 < -u B ) -> -u B e. RR )
11 1 rpgt0d
 |-  ( ph -> 0 < A )
12 11 adantr
 |-  ( ( ph /\ 0 < -u B ) -> 0 < A )
13 simpr
 |-  ( ( ph /\ 0 < -u B ) -> 0 < -u B )
14 8 10 12 13 mulgt0d
 |-  ( ( ph /\ 0 < -u B ) -> 0 < ( A x. -u B ) )
15 5 recnd
 |-  ( ph -> A e. CC )
16 15 adantr
 |-  ( ( ph /\ 0 < -u B ) -> A e. CC )
17 2 recnd
 |-  ( ph -> B e. CC )
18 17 adantr
 |-  ( ( ph /\ 0 < -u B ) -> B e. CC )
19 16 18 mulneg2d
 |-  ( ( ph /\ 0 < -u B ) -> ( A x. -u B ) = -u ( A x. B ) )
20 14 19 breqtrd
 |-  ( ( ph /\ 0 < -u B ) -> 0 < -u ( A x. B ) )
21 20 ex
 |-  ( ph -> ( 0 < -u B -> 0 < -u ( A x. B ) ) )
22 2 lt0neg1d
 |-  ( ph -> ( B < 0 <-> 0 < -u B ) )
23 6 lt0neg1d
 |-  ( ph -> ( ( A x. B ) < 0 <-> 0 < -u ( A x. B ) ) )
24 21 22 23 3imtr4d
 |-  ( ph -> ( B < 0 -> ( A x. B ) < 0 ) )
25 7 24 mtod
 |-  ( ph -> -. B < 0 )
26 4 2 25 nltled
 |-  ( ph -> 0 <_ B )