Metamath Proof Explorer

Theorem muladd11

Description: A simple product of sums expansion. (Contributed by NM, 21-Feb-2005)

Ref Expression
Assertion muladd11 
|- ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( 1 + A ) + ( B + ( A x. B ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 addcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 + A ) e. CC )
3 1 2 mpan 
 |-  ( A e. CC -> ( 1 + A ) e. CC )
4 adddi 
 |-  ( ( ( 1 + A ) e. CC /\ 1 e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( ( 1 + A ) x. 1 ) + ( ( 1 + A ) x. B ) ) )
5 1 4 mp3an2 
 |-  ( ( ( 1 + A ) e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( ( 1 + A ) x. 1 ) + ( ( 1 + A ) x. B ) ) )
6 3 5 sylan 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( ( 1 + A ) x. 1 ) + ( ( 1 + A ) x. B ) ) )
7 3 mulridd 
 |-  ( A e. CC -> ( ( 1 + A ) x. 1 ) = ( 1 + A ) )
8 7 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. 1 ) = ( 1 + A ) )
9 adddir 
 |-  ( ( 1 e. CC /\ A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. B ) = ( ( 1 x. B ) + ( A x. B ) ) )
10 1 9 mp3an1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. B ) = ( ( 1 x. B ) + ( A x. B ) ) )
11 mullid 
 |-  ( B e. CC -> ( 1 x. B ) = B )
12 11 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. B ) = B )
13 12 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 x. B ) + ( A x. B ) ) = ( B + ( A x. B ) ) )
14 10 13 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. B ) = ( B + ( A x. B ) ) )
15 8 14 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( 1 + A ) x. 1 ) + ( ( 1 + A ) x. B ) ) = ( ( 1 + A ) + ( B + ( A x. B ) ) ) )
16 6 15 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( 1 + A ) + ( B + ( A x. B ) ) ) )