itscnhlinecirc02plem2

Description: Lemma 2 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-2023)

	Ref	Expression
Hypotheses	itscnhlinecirc02plem2.d	$⊢ D = X - A$
	itscnhlinecirc02plem2.e	$⊢ E = B - Y$
	itscnhlinecirc02plem2.c	$⊢ C = B X - A Y$
Assertion	itscnhlinecirc02plem2	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to 0 < {(- 2 D C)}^{2} - 4 (E^{2} + D^{2}) (C^{2} - E^{2} R^{2})$

Proof

Step	Hyp	Ref	Expression
1		itscnhlinecirc02plem2.d	$⊢ D = X - A$
2		itscnhlinecirc02plem2.e	$⊢ E = B - Y$
3		itscnhlinecirc02plem2.c	$⊢ C = B X - A Y$
4		simpl1l	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to A \in ℝ$
5		simpl1r	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to B \in ℝ$
6		simpl2l	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to X \in ℝ$
7		simpl2r	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to Y \in ℝ$
8		eqid	$⊢ D B + E A = D B + E A$
9		simprl	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to R \in ℝ$
10		simprr	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to A^{2} + B^{2} < R^{2}$
11		simpl3	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to B \neq Y$
12	4 5 6 7 1 2 8 9 10 11	itscnhlinecirc02plem1	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to 0 < {(- 2 D (D B + E A))}^{2} - 4 (E^{2} + D^{2}) ({(D B + E A)}^{2} - E^{2} R^{2})$
13		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℝ$
14	13	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
15		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℝ$
16	15	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℂ$
17	14 16	mulcomd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B X = X B$
18		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to A \in ℝ$
19	18	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to A \in ℂ$
20		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℝ$
21	20	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℂ$
22	19 21	mulcomd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to A Y = Y A$
23	17 22	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B X - A Y = X B - Y A$
24	16 19 14	subdird	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (X - A) B = X B - A B$
25	14 21 19	subdird	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (B - Y) A = B A - Y A$
26	24 25	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (X - A) B + (B - Y) A = (X B - A B) + B A - Y A$
27	14 19	mulcomd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B A = A B$
28	27	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B A - Y A = A B - Y A$
29	28	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (X B - A B) + B A - Y A = (X B - A B) + A B - Y A$
30	16 14	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to X B \in ℂ$
31	19 14	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to A B \in ℂ$
32	21 19	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to Y A \in ℂ$
33	30 31 32	npncand	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (X B - A B) + A B - Y A = X B - Y A$
34	26 29 33	3eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (X - A) B + (B - Y) A = X B - Y A$
35	23 34	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B X - A Y = (X - A) B + (B - Y) A$
36	1	oveq1i	$⊢ D B = (X - A) B$
37	2	oveq1i	$⊢ E A = (B - Y) A$
38	36 37	oveq12i	$⊢ D B + E A = (X - A) B + (B - Y) A$
39	35 3 38	3eqtr4g	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to C = D B + E A$
40	39	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to D C = D (D B + E A)$
41	40	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to 2 D C = 2 D (D B + E A)$
42	41	negeqd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to - 2 D C = - 2 D (D B + E A)$
43	42	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to {(- 2 D C)}^{2} = {(- 2 D (D B + E A))}^{2}$
44	39	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to C^{2} = {(D B + E A)}^{2}$
45	44	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - E^{2} R^{2} = {(D B + E A)}^{2} - E^{2} R^{2}$
46	45	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (E^{2} + D^{2}) (C^{2} - E^{2} R^{2}) = (E^{2} + D^{2}) ({(D B + E A)}^{2} - E^{2} R^{2})$
47	46	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to 4 (E^{2} + D^{2}) (C^{2} - E^{2} R^{2}) = 4 (E^{2} + D^{2}) ({(D B + E A)}^{2} - E^{2} R^{2})$
48	43 47	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to {(- 2 D C)}^{2} - 4 (E^{2} + D^{2}) (C^{2} - E^{2} R^{2}) = {(- 2 D (D B + E A))}^{2} - 4 (E^{2} + D^{2}) ({(D B + E A)}^{2} - E^{2} R^{2})$
49	48	3adant3	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \to {(- 2 D C)}^{2} - 4 (E^{2} + D^{2}) (C^{2} - E^{2} R^{2}) = {(- 2 D (D B + E A))}^{2} - 4 (E^{2} + D^{2}) ({(D B + E A)}^{2} - E^{2} R^{2})$
50	49	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to {(- 2 D C)}^{2} - 4 (E^{2} + D^{2}) (C^{2} - E^{2} R^{2}) = {(- 2 D (D B + E A))}^{2} - 4 (E^{2} + D^{2}) ({(D B + E A)}^{2} - E^{2} R^{2})$
51	12 50	breqtrrd	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ) \land B \neq Y) \land (R \in ℝ \land A^{2} + B^{2} < R^{2})) \to 0 < {(- 2 D C)}^{2} - 4 (E^{2} + D^{2}) (C^{2} - E^{2} R^{2})$

Metamath Proof Explorer

Theorem itscnhlinecirc02plem2

Proof