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∈ℂ∧B∈ℂ∧D∈ℂ∧C∈ℂ∧C≠0→C⁢A+B2−DC=C⁢A2+2⁢A⁢B+B2−DC

Proof

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