Theorem sn-ltmulgt11d

Description: ltmulgt11d without ax-mulcom . (Contributed by SN, 26-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sn-ltmulgt11d.a	|- ( ph -> A e. RR )
2		sn-ltmulgt11d.b	|- ( ph -> B e. RR )
3		sn-ltmulgt11d.1	|- ( ph -> 0 < B )
4		1red	|- ( ph -> 1 e. RR )
5	4 1 2 3	sn-ltmul2d	|- ( ph -> ( ( B x. 1 ) < ( B x. A ) <-> 1 < A ) )
6		ax-1rid	|- ( B e. RR -> ( B x. 1 ) = B )
7	2 6	syl	|- ( ph -> ( B x. 1 ) = B )
8	7	breq1d	|- ( ph -> ( ( B x. 1 ) < ( B x. A ) <-> B < ( B x. A ) ) )
9	5 8	bitr3d	|- ( ph -> ( 1 < A <-> B < ( B x. A ) ) )