remulcand

Description: Commuted version of remulcan2d without ax-mulcom . (Contributed by SN, 21-Feb-2024)

	Ref	Expression
Hypotheses	remulcand.1	$⊢ φ \to A \in ℝ$
	remulcand.2	$⊢ φ \to B \in ℝ$
	remulcand.3	$⊢ φ \to C \in ℝ$
	remulcand.4	$⊢ φ \to C \neq 0$
Assertion	remulcand	$⊢ φ \to (C A = C B \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		remulcand.1	$⊢ φ \to A \in ℝ$
2		remulcand.2	$⊢ φ \to B \in ℝ$
3		remulcand.3	$⊢ φ \to C \in ℝ$
4		remulcand.4	$⊢ φ \to C \neq 0$
5		ax-rrecex	$⊢ (C \in ℝ \land C \neq 0) \to \exists x \in ℝ C x = 1$
6	3 4 5	syl2anc	$⊢ φ \to \exists x \in ℝ C x = 1$
7	3	adantr	$⊢ (φ \land x \in ℝ) \to C \in ℝ$
8	7	adantr	$⊢ ((φ \land x \in ℝ) \land C x = 1) \to C \in ℝ$
9		simplr	$⊢ ((φ \land x \in ℝ) \land C x = 1) \to x \in ℝ$
10		simpr	$⊢ ((φ \land x \in ℝ) \land C x = 1) \to C x = 1$
11	8 9 10	remulinvcom	$⊢ ((φ \land x \in ℝ) \land C x = 1) \to x C = 1$
12	11	ex	$⊢ (φ \land x \in ℝ) \to (C x = 1 \to x C = 1)$
13		oveq2	$⊢ C A = C B \to x C A = x C B$
14	13	3ad2ant3	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C A = x C B$
15		simp2	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C = 1$
16	15	oveq1d	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C A = 1 A$
17		simp1r	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x \in ℝ$
18	17	recnd	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x \in ℂ$
19	7	3ad2ant1	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to C \in ℝ$
20	19	recnd	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to C \in ℂ$
21		simp1l	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to φ$
22	21 1	syl	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to A \in ℝ$
23	22	recnd	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to A \in ℂ$
24	18 20 23	mulassd	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C A = x C A$
25		remullid	$⊢ A \in ℝ \to 1 A = A$
26	22 25	syl	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to 1 A = A$
27	16 24 26	3eqtr3d	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C A = A$
28	15	oveq1d	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C B = 1 B$
29	21 2	syl	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to B \in ℝ$
30	29	recnd	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to B \in ℂ$
31	18 20 30	mulassd	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C B = x C B$
32		remullid	$⊢ B \in ℝ \to 1 B = B$
33	29 32	syl	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to 1 B = B$
34	28 31 33	3eqtr3d	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to x C B = B$
35	14 27 34	3eqtr3d	$⊢ ((φ \land x \in ℝ) \land x C = 1 \land C A = C B) \to A = B$
36	35	3exp	$⊢ (φ \land x \in ℝ) \to (x C = 1 \to (C A = C B \to A = B))$
37	12 36	syld	$⊢ (φ \land x \in ℝ) \to (C x = 1 \to (C A = C B \to A = B))$
38	37	impr	$⊢ (φ \land (x \in ℝ \land C x = 1)) \to (C A = C B \to A = B)$
39	6 38	rexlimddv	$⊢ φ \to (C A = C B \to A = B)$
40		oveq2	$⊢ A = B \to C A = C B$
41	39 40	impbid1	$⊢ φ \to (C A = C B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem remulcand

Proof