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 \in ℂ \land B \in ℂ \land D \in ℂ) \land (C \in ℂ \land C \neq 0)) \to \frac{{(C A + B)}^{2} - D}{C} = C A^{2} + 2 A B + (\frac{B^{2} - D}{C})$

Proof

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

Metamath Proof Explorer

Theorem mulsubdivbinom2

Proof