Theorem sn-ltmul2d

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

	Ref	Expression
Hypotheses	sn-ltmul2d.a	$$⊢\phi \to A\in ℝ$$
	sn-ltmul2d.b	$$⊢\phi \to B\in ℝ$$
	sn-ltmul2d.c	$$⊢\phi \to C\in ℝ$$
	sn-ltmul2d.1	$$⊢\phi \to 0<C$$
Assertion	sn-ltmul2d	$$⊢\phi \to \left(CA<CB\leftrightarrow A<B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sn-ltmul2d.a	$$⊢\phi \to A\in ℝ$$
2		sn-ltmul2d.b	$$⊢\phi \to B\in ℝ$$
3		sn-ltmul2d.c	$$⊢\phi \to C\in ℝ$$
4		sn-ltmul2d.1	$$⊢\phi \to 0<C$$
5		rersubcl	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to B{-}_{ℝ}A\in ℝ$$
6	2 1 5	syl2anc	$$⊢\phi \to B{-}_{ℝ}A\in ℝ$$
7	3 6 4	mulgt0b1d	$$⊢\phi \to \left(0<B{-}_{ℝ}A\leftrightarrow 0<C\left(B{-}_{ℝ}A\right)\right)$$
8		resubdi	$$⊢\left(C\in ℝ\wedge B\in ℝ\wedge A\in ℝ\right)\to C\left(B{-}_{ℝ}A\right)=CB{-}_{ℝ}CA$$
9	3 2 1 8	syl3anc	$$⊢\phi \to C\left(B{-}_{ℝ}A\right)=CB{-}_{ℝ}CA$$
10	9	breq2d	$$⊢\phi \to \left(0<C\left(B{-}_{ℝ}A\right)\leftrightarrow 0<CB{-}_{ℝ}CA\right)$$
11	7 10	bitr2d	$$⊢\phi \to \left(0<CB{-}_{ℝ}CA\leftrightarrow 0<B{-}_{ℝ}A\right)$$
12	3 1	remulcld	$$⊢\phi \to CA\in ℝ$$
13	3 2	remulcld	$$⊢\phi \to CB\in ℝ$$
14		reposdif	$$⊢\left(CA\in ℝ\wedge CB\in ℝ\right)\to \left(CA<CB\leftrightarrow 0<CB{-}_{ℝ}CA\right)$$
15	12 13 14	syl2anc	$$⊢\phi \to \left(CA<CB\leftrightarrow 0<CB{-}_{ℝ}CA\right)$$
16		reposdif	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow 0<B{-}_{ℝ}A\right)$$
17	1 2 16	syl2anc	$$⊢\phi \to \left(A<B\leftrightarrow 0<B{-}_{ℝ}A\right)$$
18	11 15 17	3bitr4d	$$⊢\phi \to \left(CA<CB\leftrightarrow A<B\right)$$