redivmul2d

Description: Relationship between division and multiplication. (Contributed by SN, 2-Apr-2026)

	Ref	Expression
Hypotheses	redivmuld.a	$⊢ φ \to A \in ℝ$
	redivmuld.b	$⊢ φ \to B \in ℝ$
	redivmuld.c	$⊢ φ \to C \in ℝ$
	redivmuld.z	$⊢ φ \to C \neq 0$
Assertion	redivmul2d	Could not format assertion : No typesetting found for \|- ( ph -> ( ( A /R C ) = B <-> A = ( C x. B ) ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		redivmuld.a	$⊢ φ \to A \in ℝ$
2		redivmuld.b	$⊢ φ \to B \in ℝ$
3		redivmuld.c	$⊢ φ \to C \in ℝ$
4		redivmuld.z	$⊢ φ \to C \neq 0$
5	1 2 3 4	redivmuld	Could not format ( ph -> ( ( A /R C ) = B <-> ( C x. B ) = A ) ) : No typesetting found for \|- ( ph -> ( ( A /R C ) = B <-> ( C x. B ) = A ) ) with typecode \|-
6		eqcom	$⊢ C B = A \leftrightarrow A = C B$
7	5 6	bitrdi	Could not format ( ph -> ( ( A /R C ) = B <-> A = ( C x. B ) ) ) : No typesetting found for \|- ( ph -> ( ( A /R C ) = B <-> A = ( C x. B ) ) ) with typecode \|-

Metamath Proof Explorer