This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem redivdird

Description: Distribution of division over addition. (Contributed by SN, 9-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		rediv23d.a	$⊢ φ \to A \in ℝ$
2		rediv23d.b	$⊢ φ \to B \in ℝ$
3		rediv23d.c	$⊢ φ \to C \in ℝ$
4		rediv23d.z	$⊢ φ \to C \neq 0$
5	3	recnd	$⊢ φ \to C \in ℂ$
6	1 3 4	sn-redivcld	Could not format ( ph -> ( A /R C ) e. RR ) : No typesetting found for \|- ( ph -> ( A /R C ) e. RR ) with typecode \|-
7	6	recnd	Could not format ( ph -> ( A /R C ) e. CC ) : No typesetting found for \|- ( ph -> ( A /R C ) e. CC ) with typecode \|-
8	2 3 4	sn-redivcld	Could not format ( ph -> ( B /R C ) e. RR ) : No typesetting found for \|- ( ph -> ( B /R C ) e. RR ) with typecode \|-
9	8	recnd	Could not format ( ph -> ( B /R C ) e. CC ) : No typesetting found for \|- ( ph -> ( B /R C ) e. CC ) with typecode \|-
10	5 7 9	adddid	Could not format ( ph -> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( ( C x. ( A /R C ) ) + ( C x. ( B /R C ) ) ) ) : No typesetting found for \|- ( ph -> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( ( C x. ( A /R C ) ) + ( C x. ( B /R C ) ) ) ) with typecode \|-
11	1 3 4	redivcan2d	Could not format ( ph -> ( C x. ( A /R C ) ) = A ) : No typesetting found for \|- ( ph -> ( C x. ( A /R C ) ) = A ) with typecode \|-
12	2 3 4	redivcan2d	Could not format ( ph -> ( C x. ( B /R C ) ) = B ) : No typesetting found for \|- ( ph -> ( C x. ( B /R C ) ) = B ) with typecode \|-
13	11 12	oveq12d	Could not format ( ph -> ( ( C x. ( A /R C ) ) + ( C x. ( B /R C ) ) ) = ( A + B ) ) : No typesetting found for \|- ( ph -> ( ( C x. ( A /R C ) ) + ( C x. ( B /R C ) ) ) = ( A + B ) ) with typecode \|-
14	10 13	eqtrd	Could not format ( ph -> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( A + B ) ) : No typesetting found for \|- ( ph -> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( A + B ) ) with typecode \|-
15	1 2	readdcld	$⊢ φ \to A + B \in ℝ$
16	6 8	readdcld	Could not format ( ph -> ( ( A /R C ) + ( B /R C ) ) e. RR ) : No typesetting found for \|- ( ph -> ( ( A /R C ) + ( B /R C ) ) e. RR ) with typecode \|-
17	15 16 3 4	redivmuld	Could not format ( ph -> ( ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) <-> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( A + B ) ) ) : No typesetting found for \|- ( ph -> ( ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) <-> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( A + B ) ) ) with typecode \|-
18	14 17	mpbird	Could not format ( ph -> ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) ) : No typesetting found for \|- ( ph -> ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) ) with typecode \|-