itsclc0yqsollem1

	Ref	Expression
Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
	itscnhlc0yqe.t	$⊢ T = - 2 B C$
	itscnhlc0yqe.u	$⊢ U = C^{2} - A^{2} R^{2}$
	itsclc0yqsollem1.d	$⊢ D = R^{2} Q - C^{2}$
Assertion	itsclc0yqsollem1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to T^{2} - 4 Q U = 4 A^{2} D$

Proof

Step	Hyp	Ref	Expression
1		itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
2		itscnhlc0yqe.t	$⊢ T = - 2 B C$
3		itscnhlc0yqe.u	$⊢ U = C^{2} - A^{2} R^{2}$
4		itsclc0yqsollem1.d	$⊢ D = R^{2} Q - C^{2}$
5	2	oveq1i	$⊢ T^{2} = {(- 2 B C)}^{2}$
6		2cnd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 2 \in ℂ$
7		simpl2	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B \in ℂ$
8		simpl3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to C \in ℂ$
9	7 8	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B C \in ℂ$
10	6 9	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 2 B C \in ℂ$
11		sqneg	$⊢ 2 B C \in ℂ \to {(- 2 B C)}^{2} = {2 B C}^{2}$
12	10 11	syl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to {(- 2 B C)}^{2} = {2 B C}^{2}$
13	6 9	sqmuld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to {2 B C}^{2} = 2^{2} {B C}^{2}$
14		sq2	$⊢ 2^{2} = 4$
15	14	a1i	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 2^{2} = 4$
16	7 8	sqmuld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to {B C}^{2} = B^{2} C^{2}$
17	15 16	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 2^{2} {B C}^{2} = 4 B^{2} C^{2}$
18	12 13 17	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to {(- 2 B C)}^{2} = 4 B^{2} C^{2}$
19	5 18	syl5eq	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to T^{2} = 4 B^{2} C^{2}$
20	1 3	oveq12i	$⊢ Q U = (A^{2} + B^{2}) (C^{2} - A^{2} R^{2})$
21		simpl1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A \in ℂ$
22	21	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} \in ℂ$
23	7	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} \in ℂ$
24	22 23	addcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} + B^{2} \in ℂ$
25	8	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to C^{2} \in ℂ$
26		simpr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R \in ℂ$
27	26	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} \in ℂ$
28	22 27	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} R^{2} \in ℂ$
29	24 25 28	subdid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) (C^{2} - A^{2} R^{2}) = (A^{2} + B^{2}) C^{2} - (A^{2} + B^{2}) A^{2} R^{2}$
30	22 23 25	adddird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) C^{2} = A^{2} C^{2} + B^{2} C^{2}$
31	22 23 28	adddird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) A^{2} R^{2} = A^{2} A^{2} R^{2} + B^{2} A^{2} R^{2}$
32	30 31	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) C^{2} - (A^{2} + B^{2}) A^{2} R^{2} = A^{2} C^{2} + B^{2} C^{2} - (A^{2} A^{2} R^{2} + B^{2} A^{2} R^{2})$
33	23 25	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} \in ℂ$
34	22 25	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} C^{2} \in ℂ$
35	22 28	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} \in ℂ$
36	23 27	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} R^{2} \in ℂ$
37	22 36	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} B^{2} R^{2} \in ℂ$
38	35 37	addcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} \in ℂ$
39	34 33	addcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} C^{2} + B^{2} C^{2} = B^{2} C^{2} + A^{2} C^{2}$
40	23 22 27	mul12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} A^{2} R^{2} = A^{2} B^{2} R^{2}$
41	40	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} + B^{2} A^{2} R^{2} = A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}$
42	39 41	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} C^{2} + B^{2} C^{2} - (A^{2} A^{2} R^{2} + B^{2} A^{2} R^{2}) = B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})$
43	33 34 38 42	assraddsubd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} C^{2} + B^{2} C^{2} - (A^{2} A^{2} R^{2} + B^{2} A^{2} R^{2}) = B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})$
44	29 32 43	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) (C^{2} - A^{2} R^{2}) = B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})$
45	20 44	syl5eq	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to Q U = B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})$
46	45	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 4 Q U = 4 (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))$
47	19 46	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to T^{2} - 4 Q U = 4 B^{2} C^{2} - 4 (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))$
48		4cn	$⊢ 4 \in ℂ$
49	48	a1i	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 4 \in ℂ$
50		simp1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A \in ℂ$
51	50	sqcld	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A^{2} \in ℂ$
52	51	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} \in ℂ$
53	1 24	eqeltrid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to Q \in ℂ$
54	27 53	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} Q \in ℂ$
55	54 25	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} Q - C^{2} \in ℂ$
56	4 55	eqeltrid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to D \in ℂ$
57	49 52 56	mulassd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 4 A^{2} D = 4 A^{2} D$
58	34 38	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}) \in ℂ$
59	33 33 58	subsub4d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} - B^{2} C^{2} - (A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = B^{2} C^{2} - (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))$
60	33	subidd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} - B^{2} C^{2} = 0$
61	60	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} - B^{2} C^{2} - (A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = 0 - (A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))$
62		0cnd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 0 \in ℂ$
63	62 34 38	subsub2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 0 - (A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = 0 + (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}) - A^{2} C^{2}$
64	38 34	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} - A^{2} C^{2} \in ℂ$
65	64	addid2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 0 + (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}) - A^{2} C^{2} = A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} - A^{2} C^{2}$
66	61 63 65	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} - B^{2} C^{2} - (A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} - A^{2} C^{2}$
67	59 66	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} - (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} - A^{2} C^{2}$
68	22 28 36	adddid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} (A^{2} R^{2} + B^{2} R^{2}) = A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}$
69	22 23 27	adddird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) R^{2} = A^{2} R^{2} + B^{2} R^{2}$
70	69	eqcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} R^{2} + B^{2} R^{2} = (A^{2} + B^{2}) R^{2}$
71	70	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} (A^{2} R^{2} + B^{2} R^{2}) = A^{2} (A^{2} + B^{2}) R^{2}$
72	68 71	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} = A^{2} (A^{2} + B^{2}) R^{2}$
73	72	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} - A^{2} C^{2} = A^{2} (A^{2} + B^{2}) R^{2} - A^{2} C^{2}$
74	24 27	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) R^{2} \in ℂ$
75	22 74 25	subdid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} ((A^{2} + B^{2}) R^{2} - C^{2}) = A^{2} (A^{2} + B^{2}) R^{2} - A^{2} C^{2}$
76	73 75	eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2} - A^{2} C^{2} = A^{2} ((A^{2} + B^{2}) R^{2} - C^{2})$
77	1	a1i	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to Q = A^{2} + B^{2}$
78	77	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} Q = R^{2} (A^{2} + B^{2})$
79	27 24	mulcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} (A^{2} + B^{2}) = (A^{2} + B^{2}) R^{2}$
80	78 79	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} Q = (A^{2} + B^{2}) R^{2}$
81	80	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to R^{2} Q - C^{2} = (A^{2} + B^{2}) R^{2} - C^{2}$
82	4 81	syl5eq	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to D = (A^{2} + B^{2}) R^{2} - C^{2}$
83	82	eqcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to (A^{2} + B^{2}) R^{2} - C^{2} = D$
84	83	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to A^{2} ((A^{2} + B^{2}) R^{2} - C^{2}) = A^{2} D$
85	67 76 84	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} - (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = A^{2} D$
86	85	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 4 (B^{2} C^{2} - (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))) = 4 A^{2} D$
87	33 58	addcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}) \in ℂ$
88	49 33 87	subdid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 4 (B^{2} C^{2} - (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))) = 4 B^{2} C^{2} - 4 (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2}))$
89	57 86 88	3eqtr2rd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to 4 B^{2} C^{2} - 4 (B^{2} C^{2} + A^{2} C^{2} - (A^{2} A^{2} R^{2} + A^{2} B^{2} R^{2})) = 4 A^{2} D$
90	47 89	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to T^{2} - 4 Q U = 4 A^{2} D$

Metamath Proof Explorer

Theorem itsclc0yqsollem1

Proof