Theorem mulgt0con1d

Description: Counterpart to mulgt0con2d , though not a lemma. This is the first use of ax-pre-mulgt0 . One direction of mulgt0b2d . (Contributed by SN, 26-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		mulgt0con1d.a	|- ( ph -> A e. RR )
2		mulgt0con1d.b	|- ( ph -> B e. RR )
3		mulgt0con1d.1	|- ( ph -> 0 < B )
4		mulgt0con1d.2	|- ( ph -> ( A x. B ) < 0 )
5	1 2	remulcld	|- ( ph -> ( A x. B ) e. RR )
6	1	adantr	|- ( ( ph /\ 0 < A ) -> A e. RR )
7	2	adantr	|- ( ( ph /\ 0 < A ) -> B e. RR )
8		simpr	|- ( ( ph /\ 0 < A ) -> 0 < A )
9	3	adantr	|- ( ( ph /\ 0 < A ) -> 0 < B )
10	6 7 8 9	mulgt0d	|- ( ( ph /\ 0 < A ) -> 0 < ( A x. B ) )
11	10	ex	|- ( ph -> ( 0 < A -> 0 < ( A x. B ) ) )
12		remul02	|- ( B e. RR -> ( 0 x. B ) = 0 )
13	2 12	syl	|- ( ph -> ( 0 x. B ) = 0 )
14		oveq1	|- ( A = 0 -> ( A x. B ) = ( 0 x. B ) )
15	14	eqeq1d	|- ( A = 0 -> ( ( A x. B ) = 0 <-> ( 0 x. B ) = 0 ) )
16	13 15	syl5ibrcom	|- ( ph -> ( A = 0 -> ( A x. B ) = 0 ) )
17	1 5 11 16	mulgt0con1dlem	|- ( ph -> ( ( A x. B ) < 0 -> A < 0 ) )
18	4 17	mpd	|- ( ph -> A < 0 )