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 
|- ( 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 ) ) )