Metamath Proof Explorer

Theorem muladd11r

Description: A simple product of sums expansion. (Contributed by AV, 30-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
2 1cnd 
 |-  ( ( A e. CC /\ B e. CC ) -> 1 e. CC )
3 1 2 addcomd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + 1 ) = ( 1 + A ) )
4 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
5 4 2 addcomd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B + 1 ) = ( 1 + B ) )
6 3 5 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + 1 ) x. ( B + 1 ) ) = ( ( 1 + A ) x. ( 1 + B ) ) )
7 muladd11 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( 1 + A ) + ( B + ( A x. B ) ) ) )
8 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
9 4 8 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B + ( A x. B ) ) e. CC )
10 2 1 9 addassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) + ( B + ( A x. B ) ) ) = ( 1 + ( A + ( B + ( A x. B ) ) ) ) )
11 1 9 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( B + ( A x. B ) ) ) e. CC )
12 2 11 addcomd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 + ( A + ( B + ( A x. B ) ) ) ) = ( ( A + ( B + ( A x. B ) ) ) + 1 ) )
13 1 4 8 addassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + ( A x. B ) ) = ( A + ( B + ( A x. B ) ) ) )
14 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
15 14 8 addcomd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + ( A x. B ) ) = ( ( A x. B ) + ( A + B ) ) )
16 13 15 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( B + ( A x. B ) ) ) = ( ( A x. B ) + ( A + B ) ) )
17 16 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + ( B + ( A x. B ) ) ) + 1 ) = ( ( ( A x. B ) + ( A + B ) ) + 1 ) )
18 10 12 17 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) + ( B + ( A x. B ) ) ) = ( ( ( A x. B ) + ( A + B ) ) + 1 ) )
19 6 7 18 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + 1 ) x. ( B + 1 ) ) = ( ( ( A x. B ) + ( A + B ) ) + 1 ) )