Metamath Proof Explorer

Theorem divdir

Description: Distribution of division over addition. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
2 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
3 reccl 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( 1 / C ) e. CC )
4 3 3ad2ant3 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( 1 / C ) e. CC )
5 1 2 4 adddird 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + B ) x. ( 1 / C ) ) = ( ( A x. ( 1 / C ) ) + ( B x. ( 1 / C ) ) ) )
6 1 2 addcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A + B ) e. CC )
7 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
8 simp3r 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C =/= 0 )
9 divrec 
 |-  ( ( ( A + B ) e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( A + B ) / C ) = ( ( A + B ) x. ( 1 / C ) ) )
10 6 7 8 9 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + B ) / C ) = ( ( A + B ) x. ( 1 / C ) ) )
11 divrec 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) = ( A x. ( 1 / C ) ) )
12 1 7 8 11 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) = ( A x. ( 1 / C ) ) )
13 divrec 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
14 2 7 8 13 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
15 12 14 oveq12d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) + ( B / C ) ) = ( ( A x. ( 1 / C ) ) + ( B x. ( 1 / C ) ) ) )
16 5 10 15 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )