Metamath Proof Explorer

Theorem muldivdir

Description: Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021)

Ref Expression
Assertion muldivdir 
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) + B ) / C ) = ( A + ( B / C ) ) )

Proof

Step Hyp Ref Expression
1 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
2 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
3 1 2 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. A ) e. CC )
4 divdir 
 |-  ( ( ( C x. A ) e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) + B ) / C ) = ( ( ( C x. A ) / C ) + ( B / C ) ) )
5 3 4 syld3an1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) + B ) / C ) = ( ( ( C x. A ) / C ) + ( B / C ) ) )
6 3anass 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) <-> ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) )
7 6 biimpri 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A e. CC /\ C e. CC /\ C =/= 0 ) )
8 7 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A e. CC /\ C e. CC /\ C =/= 0 ) )
9 divcan3 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( C x. A ) / C ) = A )
10 8 9 syl 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) / C ) = A )
11 10 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) / C ) + ( B / C ) ) = ( A + ( B / C ) ) )
12 5 11 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) + B ) / C ) = ( A + ( B / C ) ) )