Theorem sn-mulgt1d

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

	Ref	Expression
Hypotheses	sn-mulgt1d.a	$$⊢\phi \to A\in ℝ$$
	sn-mulgt1d.b	$$⊢\phi \to B\in ℝ$$
	sn-mulgt1d.1	$$⊢\phi \to 1<A$$
	sn-mulgt1d.2	$$⊢\phi \to 1<B$$
Assertion	sn-mulgt1d	$$⊢\phi \to 1<AB$$

Proof

Step	Hyp	Ref	Expression
1		sn-mulgt1d.a	$$⊢\phi \to A\in ℝ$$
2		sn-mulgt1d.b	$$⊢\phi \to B\in ℝ$$
3		sn-mulgt1d.1	$$⊢\phi \to 1<A$$
4		sn-mulgt1d.2	$$⊢\phi \to 1<B$$
5		1red	$$⊢\phi \to 1\in ℝ$$
6	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
7		0red	$$⊢\phi \to 0\in ℝ$$
8		sn-0lt1	$$⊢0<1$$
9	8	a1i	$$⊢\phi \to 0<1$$
10	7 5 1 9 3	lttrd	$$⊢\phi \to 0<A$$
11	2 1 10	sn-ltmulgt11d	$$⊢\phi \to \left(1<B\leftrightarrow A<AB\right)$$
12	4 11	mpbid	$$⊢\phi \to A<AB$$
13	5 1 6 3 12	lttrd	$$⊢\phi \to 1<AB$$