Theorem redivdird

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

	Ref	Expression
Hypotheses	rediv23d.a	|- ( ph -> A e. RR )
	rediv23d.b	|- ( ph -> B e. RR )
	rediv23d.c	|- ( ph -> C e. RR )
	rediv23d.z	|- ( ph -> C =/= 0 )
Assertion	redivdird	|- ( ph -> ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) )

Proof

Step	Hyp	Ref	Expression
1		rediv23d.a	|- ( ph -> A e. RR )
2		rediv23d.b	|- ( ph -> B e. RR )
3		rediv23d.c	|- ( ph -> C e. RR )
4		rediv23d.z	|- ( ph -> C =/= 0 )
5	3	recnd	|- ( ph -> C e. CC )
6	1 3 4	sn-redivcld	|- ( ph -> ( A /R C ) e. RR )
7	6	recnd	|- ( ph -> ( A /R C ) e. CC )
8	2 3 4	sn-redivcld	|- ( ph -> ( B /R C ) e. RR )
9	8	recnd	|- ( ph -> ( B /R C ) e. CC )
10	5 7 9	adddid	|- ( ph -> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( ( C x. ( A /R C ) ) + ( C x. ( B /R C ) ) ) )
11	1 3 4	redivcan2d	|- ( ph -> ( C x. ( A /R C ) ) = A )
12	2 3 4	redivcan2d	|- ( ph -> ( C x. ( B /R C ) ) = B )
13	11 12	oveq12d	|- ( ph -> ( ( C x. ( A /R C ) ) + ( C x. ( B /R C ) ) ) = ( A + B ) )
14	10 13	eqtrd	|- ( ph -> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( A + B ) )
15	1 2	readdcld	|- ( ph -> ( A + B ) e. RR )
16	6 8	readdcld	|- ( ph -> ( ( A /R C ) + ( B /R C ) ) e. RR )
17	15 16 3 4	redivmuld	|- ( ph -> ( ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) <-> ( C x. ( ( A /R C ) + ( B /R C ) ) ) = ( A + B ) ) )
18	14 17	mpbird	|- ( ph -> ( ( A + B ) /R C ) = ( ( A /R C ) + ( B /R C ) ) )