This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )