Metamath Proof Explorer

Theorem mulsubdivbinom2

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ D e. CC ) -> A e. CC )
2 1 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
3 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
4 simpl 
 |-  ( ( C e. CC /\ C =/= 0 ) -> C e. CC )
5 4 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
6 mulbinom2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( C x. A ) + B ) ^ 2 ) = ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
7 6 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( ( C x. A ) + B ) ^ 2 ) - D ) = ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) - D ) )
8 7 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( ( ( C x. A ) + B ) ^ 2 ) - D ) / C ) = ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) - D ) / C ) )
9 2 3 5 8 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) + B ) ^ 2 ) - D ) / C ) = ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) - D ) / C ) )
10 5 2 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. A ) e. CC )
11 10 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) ^ 2 ) e. CC )
12 2cnd 
 |-  ( C e. CC -> 2 e. CC )
13 id 
 |-  ( C e. CC -> C e. CC )
14 12 13 mulcld 
 |-  ( C e. CC -> ( 2 x. C ) e. CC )
15 14 adantr 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( 2 x. C ) e. CC )
16 15 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( 2 x. C ) e. CC )
17 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
18 17 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ D e. CC ) -> ( A x. B ) e. CC )
19 18 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. B ) e. CC )
20 16 19 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( 2 x. C ) x. ( A x. B ) ) e. CC )
21 11 20 addcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) e. CC )
22 sqcl 
 |-  ( B e. CC -> ( B ^ 2 ) e. CC )
23 22 3ad2ant2 
 |-  ( ( A e. CC /\ B e. CC /\ D e. CC ) -> ( B ^ 2 ) e. CC )
24 23 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( B ^ 2 ) e. CC )
25 21 24 addcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) e. CC )
26 simpl3 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> D e. CC )
27 simpr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C e. CC /\ C =/= 0 ) )
28 divsubdir 
 |-  ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) e. CC /\ D e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) - D ) / C ) = ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) / C ) - ( D / C ) ) )
29 25 26 27 28 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) - D ) / C ) = ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) / C ) - ( D / C ) ) )
30 divdir 
 |-  ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) e. CC /\ ( B ^ 2 ) e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) / C ) = ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) / C ) + ( ( B ^ 2 ) / C ) ) )
31 21 24 27 30 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) / C ) = ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) / C ) + ( ( B ^ 2 ) / C ) ) )
32 divdir 
 |-  ( ( ( ( C x. A ) ^ 2 ) e. CC /\ ( ( 2 x. C ) x. ( A x. B ) ) e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) / C ) = ( ( ( ( C x. A ) ^ 2 ) / C ) + ( ( ( 2 x. C ) x. ( A x. B ) ) / C ) ) )
33 11 20 27 32 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) / C ) = ( ( ( ( C x. A ) ^ 2 ) / C ) + ( ( ( 2 x. C ) x. ( A x. B ) ) / C ) ) )
34 sqmul 
 |-  ( ( C e. CC /\ A e. CC ) -> ( ( C x. A ) ^ 2 ) = ( ( C ^ 2 ) x. ( A ^ 2 ) ) )
35 4 1 34 syl2anr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) ^ 2 ) = ( ( C ^ 2 ) x. ( A ^ 2 ) ) )
36 35 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) ^ 2 ) / C ) = ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) / C ) )
37 sqcl 
 |-  ( C e. CC -> ( C ^ 2 ) e. CC )
38 37 adantr 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( C ^ 2 ) e. CC )
39 38 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C ^ 2 ) e. CC )
40 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
41 40 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ D e. CC ) -> ( A ^ 2 ) e. CC )
42 41 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A ^ 2 ) e. CC )
43 div23 
 |-  ( ( ( C ^ 2 ) e. CC /\ ( A ^ 2 ) e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) / C ) = ( ( ( C ^ 2 ) / C ) x. ( A ^ 2 ) ) )
44 39 42 27 43 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) / C ) = ( ( ( C ^ 2 ) / C ) x. ( A ^ 2 ) ) )
45 sqdivid 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( ( C ^ 2 ) / C ) = C )
46 45 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C ^ 2 ) / C ) = C )
47 46 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C ^ 2 ) / C ) x. ( A ^ 2 ) ) = ( C x. ( A ^ 2 ) ) )
48 36 44 47 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) ^ 2 ) / C ) = ( C x. ( A ^ 2 ) ) )
49 div23 
 |-  ( ( ( 2 x. C ) e. CC /\ ( A x. B ) e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( 2 x. C ) x. ( A x. B ) ) / C ) = ( ( ( 2 x. C ) / C ) x. ( A x. B ) ) )
50 16 19 27 49 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( 2 x. C ) x. ( A x. B ) ) / C ) = ( ( ( 2 x. C ) / C ) x. ( A x. B ) ) )
51 2cnd 
 |-  ( ( C e. CC /\ C =/= 0 ) -> 2 e. CC )
52 simpr 
 |-  ( ( C e. CC /\ C =/= 0 ) -> C =/= 0 )
53 51 4 52 divcan4d 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( ( 2 x. C ) / C ) = 2 )
54 53 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( 2 x. C ) / C ) = 2 )
55 54 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( 2 x. C ) / C ) x. ( A x. B ) ) = ( 2 x. ( A x. B ) ) )
56 50 55 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( 2 x. C ) x. ( A x. B ) ) / C ) = ( 2 x. ( A x. B ) ) )
57 48 56 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) ^ 2 ) / C ) + ( ( ( 2 x. C ) x. ( A x. B ) ) / C ) ) = ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) )
58 33 57 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) / C ) = ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) )
59 58 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) / C ) + ( ( B ^ 2 ) / C ) ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( B ^ 2 ) / C ) ) )
60 31 59 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( B ^ 2 ) / C ) ) )
61 60 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) / C ) - ( D / C ) ) = ( ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( B ^ 2 ) / C ) ) - ( D / C ) ) )
62 5 42 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. ( A ^ 2 ) ) e. CC )
63 2cnd 
 |-  ( ( A e. CC /\ B e. CC ) -> 2 e. CC )
64 63 17 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( A x. B ) ) e. CC )
65 64 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ D e. CC ) -> ( 2 x. ( A x. B ) ) e. CC )
66 65 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( 2 x. ( A x. B ) ) e. CC )
67 62 66 addcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) e. CC )
68 52 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> C =/= 0 )
69 24 5 68 divcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( B ^ 2 ) / C ) e. CC )
70 26 5 68 divcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( D / C ) e. CC )
71 67 69 70 addsubassd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( B ^ 2 ) / C ) ) - ( D / C ) ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) / C ) - ( D / C ) ) ) )
72 29 61 71 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) - D ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) / C ) - ( D / C ) ) ) )
73 divsubdir 
 |-  ( ( ( B ^ 2 ) e. CC /\ D e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( B ^ 2 ) - D ) / C ) = ( ( ( B ^ 2 ) / C ) - ( D / C ) ) )
74 24 26 27 73 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( B ^ 2 ) - D ) / C ) = ( ( ( B ^ 2 ) / C ) - ( D / C ) ) )
75 74 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( B ^ 2 ) / C ) - ( D / C ) ) = ( ( ( B ^ 2 ) - D ) / C ) )
76 75 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) / C ) - ( D / C ) ) ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - D ) / C ) ) )
77 9 72 76 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( ( ( C x. A ) + B ) ^ 2 ) - D ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - D ) / C ) ) )