Metamath Proof Explorer

Theorem muldivbinom2

Description: The square of a binomial with factor divided by a nonzero number. (Contributed by AV, 19-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
2 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
3 0cnd 
 |-  ( ( A e. CC /\ B e. CC ) -> 0 e. CC )
4 1 2 3 3jca 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A e. CC /\ B e. CC /\ 0 e. CC ) )
5 mulsubdivbinom2 
 |-  ( ( ( A e. CC /\ B e. CC /\ 0 e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) + B ) ^ 2 ) - 0 ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 0 ) / C ) ) )
6 4 5 stoic3 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) + B ) ^ 2 ) - 0 ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 0 ) / C ) ) )
7 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
8 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
9 7 8 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. A ) e. CC )
10 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
11 9 10 addcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) + B ) e. CC )
12 11 sqcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) + B ) ^ 2 ) e. CC )
13 12 subid1d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) + B ) ^ 2 ) - 0 ) = ( ( ( C x. A ) + B ) ^ 2 ) )
14 13 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) + B ) ^ 2 ) = ( ( ( ( C x. A ) + B ) ^ 2 ) - 0 ) )
15 14 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) + B ) ^ 2 ) / C ) = ( ( ( ( ( C x. A ) + B ) ^ 2 ) - 0 ) / C ) )
16 sqcl 
 |-  ( B e. CC -> ( B ^ 2 ) e. CC )
17 16 subid1d 
 |-  ( B e. CC -> ( ( B ^ 2 ) - 0 ) = ( B ^ 2 ) )
18 17 3ad2ant2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( B ^ 2 ) - 0 ) = ( B ^ 2 ) )
19 18 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B ^ 2 ) = ( ( B ^ 2 ) - 0 ) )
20 19 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( B ^ 2 ) / C ) = ( ( ( B ^ 2 ) - 0 ) / C ) )
21 20 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( B ^ 2 ) / C ) ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 0 ) / C ) ) )
22 6 15 21 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) + B ) ^ 2 ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( B ^ 2 ) / C ) ) )