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 ) )