Theorem itscnhlinecirc02plem1

Description: Lemma 1 for itscnhlinecirc02p . (Contributed by AV, 6-Mar-2023)

	Ref	Expression
Hypotheses	2itscp.a	$$⊢\phi \to A\in ℝ$$
	2itscp.b	$$⊢\phi \to B\in ℝ$$
	2itscp.x	$$⊢\phi \to X\in ℝ$$
	2itscp.y	$$⊢\phi \to Y\in ℝ$$
	2itscp.d	$$⊢D=X-A$$
	2itscp.e	$$⊢E=B-Y$$
	2itscp.c	$$⊢C=DB+EA$$
	2itscp.r	$$⊢\phi \to R\in ℝ$$
	2itscp.l	$$⊢\phi \to A^2+B^2<R^2$$
	itscnhlinecirc02plem1.n	$$⊢\phi \to B\ne Y$$
Assertion	itscnhlinecirc02plem1	$$⊢\phi \to 0<{\left(-2DC\right)}^2-4\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		2itscp.a	$$⊢\phi \to A\in ℝ$$
2		2itscp.b	$$⊢\phi \to B\in ℝ$$
3		2itscp.x	$$⊢\phi \to X\in ℝ$$
4		2itscp.y	$$⊢\phi \to Y\in ℝ$$
5		2itscp.d	$$⊢D=X-A$$
6		2itscp.e	$$⊢E=B-Y$$
7		2itscp.c	$$⊢C=DB+EA$$
8		2itscp.r	$$⊢\phi \to R\in ℝ$$
9		2itscp.l	$$⊢\phi \to A^2+B^2<R^2$$
10		itscnhlinecirc02plem1.n	$$⊢\phi \to B\ne Y$$
11		4re	$$⊢4\in ℝ$$
12	11	a1i	$$⊢\phi \to 4\in ℝ$$
13	3 1	resubcld	$$⊢\phi \to X-A\in ℝ$$
14	5 13	eqeltrid	$$⊢\phi \to D\in ℝ$$
15	14	resqcld	$$⊢\phi \to D^2\in ℝ$$
16	14 2	remulcld	$$⊢\phi \to DB\in ℝ$$
17	2 4	resubcld	$$⊢\phi \to B-Y\in ℝ$$
18	6 17	eqeltrid	$$⊢\phi \to E\in ℝ$$
19	18 1	remulcld	$$⊢\phi \to EA\in ℝ$$
20	16 19	readdcld	$$⊢\phi \to DB+EA\in ℝ$$
21	7 20	eqeltrid	$$⊢\phi \to C\in ℝ$$
22	21	resqcld	$$⊢\phi \to C^2\in ℝ$$
23	15 22	remulcld	$$⊢\phi \to D^2{C}^2\in ℝ$$
24	18	resqcld	$$⊢\phi \to E^2\in ℝ$$
25	24 15	readdcld	$$⊢\phi \to E^2+D^2\in ℝ$$
26	8	resqcld	$$⊢\phi \to R^2\in ℝ$$
27	24 26	remulcld	$$⊢\phi \to E^2{R}^2\in ℝ$$
28	22 27	resubcld	$$⊢\phi \to C^2-E^2{R}^2\in ℝ$$
29	25 28	remulcld	$$⊢\phi \to \left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)\in ℝ$$
30	23 29	resubcld	$$⊢\phi \to D^2{C}^2-\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)\in ℝ$$
31		4pos	$$⊢0<4$$
32	31	a1i	$$⊢\phi \to 0<4$$
33	15 26	remulcld	$$⊢\phi \to D^2{R}^2\in ℝ$$
34	27 33	readdcld	$$⊢\phi \to E^2{R}^2+D^2{R}^2\in ℝ$$
35	34 22	resubcld	$$⊢\phi \to E^2{R}^2+D^2{R}^2-C^2\in ℝ$$
36	6	a1i	$$⊢\phi \to E=B-Y$$
37	2	recnd	$$⊢\phi \to B\in ℂ$$
38	4	recnd	$$⊢\phi \to Y\in ℂ$$
39	37 38 10	subne0d	$$⊢\phi \to B-Y\ne 0$$
40	36 39	eqnetrd	$$⊢\phi \to E\ne 0$$
41	18 40	sqgt0d	$$⊢\phi \to 0<E^2$$
42	10	orcd	$$⊢\phi \to \left(B\ne Y\vee A\ne X\right)$$
43		eqid	$$⊢E^2+D^2=E^2+D^2$$
44		eqid	$$⊢R^2\left(E^2+D^2\right)-C^2=R^2\left(E^2+D^2\right)-C^2$$
45	1 2 3 4 5 6 7 8 9 42 43 44	2itscp	$$⊢\phi \to 0<R^2\left(E^2+D^2\right)-C^2$$
46	24	recnd	$$⊢\phi \to E^2\in ℂ$$
47	15	recnd	$$⊢\phi \to D^2\in ℂ$$
48	26	recnd	$$⊢\phi \to R^2\in ℂ$$
49	46 47 48	adddird	$$⊢\phi \to \left(E^2+D^2\right)R^2=E^2{R}^2+D^2{R}^2$$
50	46 47	addcld	$$⊢\phi \to E^2+D^2\in ℂ$$
51	50 48	mulcomd	$$⊢\phi \to \left(E^2+D^2\right)R^2=R^2\left(E^2+D^2\right)$$
52	49 51	eqtr3d	$$⊢\phi \to E^2{R}^2+D^2{R}^2=R^2\left(E^2+D^2\right)$$
53	52	oveq1d	$$⊢\phi \to E^2{R}^2+D^2{R}^2-C^2=R^2\left(E^2+D^2\right)-C^2$$
54	45 53	breqtrrd	$$⊢\phi \to 0<E^2{R}^2+D^2{R}^2-C^2$$
55	24 35 41 54	mulgt0d	$$⊢\phi \to 0<E^2\left(E^2{R}^2+D^2{R}^2-C^2\right)$$
56	47 46 48	mul12d	$$⊢\phi \to D^2{E}^2{R}^2=E^2{D}^2{R}^2$$
57	56	oveq2d	$$⊢\phi \to E^2{E}^2{R}^2+D^2{E}^2{R}^2=E^2{E}^2{R}^2+E^2{D}^2{R}^2$$
58	46 48	mulcld	$$⊢\phi \to E^2{R}^2\in ℂ$$
59	47 48	mulcld	$$⊢\phi \to D^2{R}^2\in ℂ$$
60	46 58 59	adddid	$$⊢\phi \to E^2\left(E^2{R}^2+D^2{R}^2\right)=E^2{E}^2{R}^2+E^2{D}^2{R}^2$$
61	57 60	eqtr4d	$$⊢\phi \to E^2{E}^2{R}^2+D^2{E}^2{R}^2=E^2\left(E^2{R}^2+D^2{R}^2\right)$$
62	61	oveq1d	$$⊢\phi \to E^2{E}^2{R}^2+D^2{E}^2{R}^2-E^2{C}^2=E^2\left(E^2{R}^2+D^2{R}^2\right)-E^2{C}^2$$
63	58 59	addcld	$$⊢\phi \to E^2{R}^2+D^2{R}^2\in ℂ$$
64	22	recnd	$$⊢\phi \to C^2\in ℂ$$
65	46 63 64	subdid	$$⊢\phi \to E^2\left(E^2{R}^2+D^2{R}^2-C^2\right)=E^2\left(E^2{R}^2+D^2{R}^2\right)-E^2{C}^2$$
66	62 65	eqtr4d	$$⊢\phi \to E^2{E}^2{R}^2+D^2{E}^2{R}^2-E^2{C}^2=E^2\left(E^2{R}^2+D^2{R}^2-C^2\right)$$
67	55 66	breqtrrd	$$⊢\phi \to 0<E^2{E}^2{R}^2+D^2{E}^2{R}^2-E^2{C}^2$$
68	18	recnd	$$⊢\phi \to E\in ℂ$$
69	68	sqcld	$$⊢\phi \to E^2\in ℂ$$
70	14	recnd	$$⊢\phi \to D\in ℂ$$
71	70	sqcld	$$⊢\phi \to D^2\in ℂ$$
72	27	recnd	$$⊢\phi \to E^2{R}^2\in ℂ$$
73		mulsubaddmulsub	$$⊢\left(\left(E^2\in ℂ\wedge D^2\in ℂ\right)\wedge \left(C^2\in ℂ\wedge E^2{R}^2\in ℂ\right)\right)\to D^2{C}^2-\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)=E^2{E}^2{R}^2+D^2{E}^2{R}^2-E^2{C}^2$$
74	69 71 64 72 73	syl22anc	$$⊢\phi \to D^2{C}^2-\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)=E^2{E}^2{R}^2+D^2{E}^2{R}^2-E^2{C}^2$$
75	67 74	breqtrrd	$$⊢\phi \to 0<D^2{C}^2-\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)$$
76	12 30 32 75	mulgt0d	$$⊢\phi \to 0<4\left(D^2{C}^2-\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)\right)$$
77		4cn	$$⊢4\in ℂ$$
78	77	a1i	$$⊢\phi \to 4\in ℂ$$
79	21	recnd	$$⊢\phi \to C\in ℂ$$
80	79	sqcld	$$⊢\phi \to C^2\in ℂ$$
81	71 80	mulcld	$$⊢\phi \to D^2{C}^2\in ℂ$$
82	69 71	addcld	$$⊢\phi \to E^2+D^2\in ℂ$$
83	8	recnd	$$⊢\phi \to R\in ℂ$$
84	83	sqcld	$$⊢\phi \to R^2\in ℂ$$
85	69 84	mulcld	$$⊢\phi \to E^2{R}^2\in ℂ$$
86	80 85	subcld	$$⊢\phi \to C^2-E^2{R}^2\in ℂ$$
87	82 86	mulcld	$$⊢\phi \to \left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)\in ℂ$$
88	78 81 87	subdid	$$⊢\phi \to 4\left(D^2{C}^2-\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)\right)=4D^2{C}^2-4\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)$$
89	76 88	breqtrd	$$⊢\phi \to 0<4D^2{C}^2-4\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)$$
90		2cnd	$$⊢\phi \to 2\in ℂ$$
91	70 79	mulcld	$$⊢\phi \to DC\in ℂ$$
92	90 91	mulcld	$$⊢\phi \to 2DC\in ℂ$$
93		sqneg	$$⊢2DC\in ℂ\to {\left(-2DC\right)}^2={2DC}^2$$
94	92 93	syl	$$⊢\phi \to {\left(-2DC\right)}^2={2DC}^2$$
95	90 91	sqmuld	$$⊢\phi \to {2DC}^2=2^2{DC}^2$$
96		sq2	$$⊢2^2=4$$
97	96	a1i	$$⊢\phi \to 2^2=4$$
98	70 79	sqmuld	$$⊢\phi \to {DC}^2=D^2{C}^2$$
99	97 98	oveq12d	$$⊢\phi \to 2^2{DC}^2=4D^2{C}^2$$
100	94 95 99	3eqtrd	$$⊢\phi \to {\left(-2DC\right)}^2=4D^2{C}^2$$
101	100	oveq1d	$$⊢\phi \to {\left(-2DC\right)}^2-4\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)=4D^2{C}^2-4\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)$$
102	89 101	breqtrrd	$$⊢\phi \to 0<{\left(-2DC\right)}^2-4\left(E^2+D^2\right)\left(C^2-E^2{R}^2\right)$$