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

Metamath Proof Explorer

Theorem mulgt0con1dlem

Description: Lemma for mulgt0con1d . Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024)

Ref Expression
Hypotheses mulgt0con1dlem.a 
|- ( ph -> A e. RR )
mulgt0con1dlem.b 
|- ( ph -> B e. RR )
mulgt0con1dlem.1 
|- ( ph -> ( 0 < A -> 0 < B ) )
mulgt0con1dlem.2 
|- ( ph -> ( A = 0 -> B = 0 ) )
Assertion mulgt0con1dlem 
|- ( ph -> ( B < 0 -> A < 0 ) )

Proof

Step Hyp Ref Expression
1 mulgt0con1dlem.a 
 |-  ( ph -> A e. RR )
2 mulgt0con1dlem.b 
 |-  ( ph -> B e. RR )
3 mulgt0con1dlem.1 
 |-  ( ph -> ( 0 < A -> 0 < B ) )
4 mulgt0con1dlem.2 
 |-  ( ph -> ( A = 0 -> B = 0 ) )
5 0red 
 |-  ( ph -> 0 e. RR )
6 2 5 lttrid 
 |-  ( ph -> ( B < 0 <-> -. ( B = 0 \/ 0 < B ) ) )
7 4 3 orim12d 
 |-  ( ph -> ( ( A = 0 \/ 0 < A ) -> ( B = 0 \/ 0 < B ) ) )
8 7 con3d 
 |-  ( ph -> ( -. ( B = 0 \/ 0 < B ) -> -. ( A = 0 \/ 0 < A ) ) )
9 1 5 lttrid 
 |-  ( ph -> ( A < 0 <-> -. ( A = 0 \/ 0 < A ) ) )
10 8 9 sylibrd 
 |-  ( ph -> ( -. ( B = 0 \/ 0 < B ) -> A < 0 ) )
11 6 10 sylbid 
 |-  ( ph -> ( B < 0 -> A < 0 ) )