2itscp

Description: A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023) (Revised by AV, 16-May-2023)

	Ref	Expression
Hypotheses	2itscp.a	$⊢ φ \to A \in ℝ$
	2itscp.b	$⊢ φ \to B \in ℝ$
	2itscp.x	$⊢ φ \to X \in ℝ$
	2itscp.y	$⊢ φ \to Y \in ℝ$
	2itscp.d	$⊢ D = X - A$
	2itscp.e	$⊢ E = B - Y$
	2itscp.c	$⊢ C = D B + E A$
	2itscp.r	$⊢ φ \to R \in ℝ$
	2itscp.l	$⊢ φ \to A^{2} + B^{2} < R^{2}$
	2itscp.n	$⊢ φ \to (B \neq Y \lor A \neq X)$
	2itscp.q	$⊢ Q = E^{2} + D^{2}$
	2itscp.s	$⊢ S = R^{2} Q - C^{2}$
Assertion	2itscp	$⊢ φ \to 0 < S$

Proof

Step	Hyp	Ref	Expression
1		2itscp.a	$⊢ φ \to A \in ℝ$
2		2itscp.b	$⊢ φ \to B \in ℝ$
3		2itscp.x	$⊢ φ \to X \in ℝ$
4		2itscp.y	$⊢ φ \to Y \in ℝ$
5		2itscp.d	$⊢ D = X - A$
6		2itscp.e	$⊢ E = B - Y$
7		2itscp.c	$⊢ C = D B + E A$
8		2itscp.r	$⊢ φ \to R \in ℝ$
9		2itscp.l	$⊢ φ \to A^{2} + B^{2} < R^{2}$
10		2itscp.n	$⊢ φ \to (B \neq Y \lor A \neq X)$
11		2itscp.q	$⊢ Q = E^{2} + D^{2}$
12		2itscp.s	$⊢ S = R^{2} Q - C^{2}$
13	2	recnd	$⊢ φ \to B \in ℂ$
14	13	adantr	$⊢ (φ \land B \neq Y) \to B \in ℂ$
15	4	recnd	$⊢ φ \to Y \in ℂ$
16	15	adantr	$⊢ (φ \land B \neq Y) \to Y \in ℂ$
17		simpr	$⊢ (φ \land B \neq Y) \to B \neq Y$
18	14 16 17	subne0d	$⊢ (φ \land B \neq Y) \to B - Y \neq 0$
19	18	ex	$⊢ φ \to (B \neq Y \to B - Y \neq 0)$
20	3	recnd	$⊢ φ \to X \in ℂ$
21	20	adantr	$⊢ (φ \land A \neq X) \to X \in ℂ$
22	1	recnd	$⊢ φ \to A \in ℂ$
23	22	adantr	$⊢ (φ \land A \neq X) \to A \in ℂ$
24		simpr	$⊢ (φ \land A \neq X) \to A \neq X$
25	24	necomd	$⊢ (φ \land A \neq X) \to X \neq A$
26	21 23 25	subne0d	$⊢ (φ \land A \neq X) \to X - A \neq 0$
27	26	ex	$⊢ φ \to (A \neq X \to X - A \neq 0)$
28	6	neeq1i	$⊢ E \neq 0 \leftrightarrow B - Y \neq 0$
29	5	neeq1i	$⊢ D \neq 0 \leftrightarrow X - A \neq 0$
30	28 29	anbi12i	$⊢ (E \neq 0 \land D \neq 0) \leftrightarrow (B - Y \neq 0 \land X - A \neq 0)$
31		2re	$⊢ 2 \in ℝ$
32	31	a1i	$⊢ φ \to 2 \in ℝ$
33	3 1	resubcld	$⊢ φ \to X - A \in ℝ$
34	5 33	eqeltrid	$⊢ φ \to D \in ℝ$
35	34 1	remulcld	$⊢ φ \to D A \in ℝ$
36	2 4	resubcld	$⊢ φ \to B - Y \in ℝ$
37	6 36	eqeltrid	$⊢ φ \to E \in ℝ$
38	37 2	remulcld	$⊢ φ \to E B \in ℝ$
39	35 38	remulcld	$⊢ φ \to D A E B \in ℝ$
40	32 39	remulcld	$⊢ φ \to 2 D A E B \in ℝ$
41	40	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to 2 D A E B \in ℝ$
42	37	resqcld	$⊢ φ \to E^{2} \in ℝ$
43	2	resqcld	$⊢ φ \to B^{2} \in ℝ$
44	42 43	remulcld	$⊢ φ \to E^{2} B^{2} \in ℝ$
45	34	resqcld	$⊢ φ \to D^{2} \in ℝ$
46	1	resqcld	$⊢ φ \to A^{2} \in ℝ$
47	45 46	remulcld	$⊢ φ \to D^{2} A^{2} \in ℝ$
48	44 47	readdcld	$⊢ φ \to E^{2} B^{2} + D^{2} A^{2} \in ℝ$
49	48	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} B^{2} + D^{2} A^{2} \in ℝ$
50	8	resqcld	$⊢ φ \to R^{2} \in ℝ$
51	50 46	resubcld	$⊢ φ \to R^{2} - A^{2} \in ℝ$
52	42 51	remulcld	$⊢ φ \to E^{2} (R^{2} - A^{2}) \in ℝ$
53	50 43	resubcld	$⊢ φ \to R^{2} - B^{2} \in ℝ$
54	45 53	remulcld	$⊢ φ \to D^{2} (R^{2} - B^{2}) \in ℝ$
55	52 54	readdcld	$⊢ φ \to E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) \in ℝ$
56	55	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) \in ℝ$
57	35 38	resubcld	$⊢ φ \to D A - E B \in ℝ$
58	57	sqge0d	$⊢ φ \to 0 \leq {(D A - E B)}^{2}$
59	1 2 3 4 5 6	2itscplem1	$⊢ φ \to E^{2} B^{2} + D^{2} A^{2} - 2 D A E B = {(D A - E B)}^{2}$
60	58 59	breqtrrd	$⊢ φ \to 0 \leq E^{2} B^{2} + D^{2} A^{2} - 2 D A E B$
61	48 40	subge0d	$⊢ φ \to (0 \leq E^{2} B^{2} + D^{2} A^{2} - 2 D A E B \leftrightarrow 2 D A E B \leq E^{2} B^{2} + D^{2} A^{2})$
62	60 61	mpbid	$⊢ φ \to 2 D A E B \leq E^{2} B^{2} + D^{2} A^{2}$
63	62	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to 2 D A E B \leq E^{2} B^{2} + D^{2} A^{2}$
64	44	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} B^{2} \in ℝ$
65	47	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to D^{2} A^{2} \in ℝ$
66	52	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} (R^{2} - A^{2}) \in ℝ$
67	54	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to D^{2} (R^{2} - B^{2}) \in ℝ$
68	43	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to B^{2} \in ℝ$
69	51	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to R^{2} - A^{2} \in ℝ$
70		simpl	$⊢ (E \neq 0 \land D \neq 0) \to E \neq 0$
71		sqn0rp	$⊢ (E \in ℝ \land E \neq 0) \to E^{2} \in ℝ^{+}$
72	37 70 71	syl2an	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} \in ℝ^{+}$
73	46 43 50	ltaddsub2d	$⊢ φ \to (A^{2} + B^{2} < R^{2} \leftrightarrow B^{2} < R^{2} - A^{2})$
74	9 73	mpbid	$⊢ φ \to B^{2} < R^{2} - A^{2}$
75	74	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to B^{2} < R^{2} - A^{2}$
76	68 69 72 75	ltmul2dd	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} B^{2} < E^{2} (R^{2} - A^{2})$
77	46	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to A^{2} \in ℝ$
78	53	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to R^{2} - B^{2} \in ℝ$
79		simpr	$⊢ (E \neq 0 \land D \neq 0) \to D \neq 0$
80		sqn0rp	$⊢ (D \in ℝ \land D \neq 0) \to D^{2} \in ℝ^{+}$
81	34 79 80	syl2an	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to D^{2} \in ℝ^{+}$
82	46 43 50	ltaddsubd	$⊢ φ \to (A^{2} + B^{2} < R^{2} \leftrightarrow A^{2} < R^{2} - B^{2})$
83	9 82	mpbid	$⊢ φ \to A^{2} < R^{2} - B^{2}$
84	83	adantr	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to A^{2} < R^{2} - B^{2}$
85	77 78 81 84	ltmul2dd	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to D^{2} A^{2} < D^{2} (R^{2} - B^{2})$
86	64 65 66 67 76 85	lt2addd	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to E^{2} B^{2} + D^{2} A^{2} < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
87	41 49 56 63 86	lelttrd	$⊢ (φ \land (E \neq 0 \land D \neq 0)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
88	87	ex	$⊢ φ \to ((E \neq 0 \land D \neq 0) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
89	30 88	biimtrrid	$⊢ φ \to ((B - Y \neq 0 \land X - A \neq 0) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
90	19 27 89	syl2and	$⊢ φ \to ((B \neq Y \land A \neq X) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
91	90	imp	$⊢ (φ \land (B \neq Y \land A \neq X)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
92		nne	$⊢ \neg A \neq X \leftrightarrow A = X$
93		eqcom	$⊢ A = X \leftrightarrow X = A$
94	20 22	subeq0ad	$⊢ φ \to (X - A = 0 \leftrightarrow X = A)$
95	94	biimprd	$⊢ φ \to (X = A \to X - A = 0)$
96	93 95	biimtrid	$⊢ φ \to (A = X \to X - A = 0)$
97	92 96	biimtrid	$⊢ φ \to (\neg A \neq X \to X - A = 0)$
98	5	eqeq1i	$⊢ D = 0 \leftrightarrow X - A = 0$
99	28 98	anbi12i	$⊢ (E \neq 0 \land D = 0) \leftrightarrow (B - Y \neq 0 \land X - A = 0)$
100		0red	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 0 \in ℝ$
101	44	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} B^{2} \in ℝ$
102	52	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} (R^{2} - A^{2}) \in ℝ$
103	37	sqge0d	$⊢ φ \to 0 \leq E^{2}$
104	2	sqge0d	$⊢ φ \to 0 \leq B^{2}$
105	42 43 103 104	mulge0d	$⊢ φ \to 0 \leq E^{2} B^{2}$
106	105	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 0 \leq E^{2} B^{2}$
107	43	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to B^{2} \in ℝ$
108	51	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to R^{2} - A^{2} \in ℝ$
109		simprl	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E \neq 0$
110	37 109 71	syl2an2r	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} \in ℝ^{+}$
111	74	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to B^{2} < R^{2} - A^{2}$
112	107 108 110 111	ltmul2dd	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} B^{2} < E^{2} (R^{2} - A^{2})$
113	100 101 102 106 112	lelttrd	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 0 < E^{2} (R^{2} - A^{2})$
114		oveq1	$⊢ D = 0 \to D A = 0 \cdot A$
115	114	adantl	$⊢ (E \neq 0 \land D = 0) \to D A = 0 \cdot A$
116	22	mul02d	$⊢ φ \to 0 \cdot A = 0$
117	115 116	sylan9eqr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to D A = 0$
118	117	oveq1d	$⊢ (φ \land (E \neq 0 \land D = 0)) \to D A E B = 0 \cdot E B$
119	38	recnd	$⊢ φ \to E B \in ℂ$
120	119	mul02d	$⊢ φ \to 0 \cdot E B = 0$
121	120	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 0 \cdot E B = 0$
122	118 121	eqtrd	$⊢ (φ \land (E \neq 0 \land D = 0)) \to D A E B = 0$
123	122	oveq2d	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 2 D A E B = 2 \cdot 0$
124		2t0e0	$⊢ 2 \cdot 0 = 0$
125	123 124	eqtrdi	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 2 D A E B = 0$
126		sq0i	$⊢ D = 0 \to D^{2} = 0$
127	126	adantl	$⊢ (E \neq 0 \land D = 0) \to D^{2} = 0$
128	127	adantl	$⊢ (φ \land (E \neq 0 \land D = 0)) \to D^{2} = 0$
129	128	oveq1d	$⊢ (φ \land (E \neq 0 \land D = 0)) \to D^{2} (R^{2} - B^{2}) = 0 \cdot (R^{2} - B^{2})$
130	53	recnd	$⊢ φ \to R^{2} - B^{2} \in ℂ$
131	130	mul02d	$⊢ φ \to 0 \cdot (R^{2} - B^{2}) = 0$
132	131	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 0 \cdot (R^{2} - B^{2}) = 0$
133	129 132	eqtrd	$⊢ (φ \land (E \neq 0 \land D = 0)) \to D^{2} (R^{2} - B^{2}) = 0$
134	133	oveq2d	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) = E^{2} (R^{2} - A^{2}) + 0$
135	52	recnd	$⊢ φ \to E^{2} (R^{2} - A^{2}) \in ℂ$
136	135	addridd	$⊢ φ \to E^{2} (R^{2} - A^{2}) + 0 = E^{2} (R^{2} - A^{2})$
137	136	adantr	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} (R^{2} - A^{2}) + 0 = E^{2} (R^{2} - A^{2})$
138	134 137	eqtrd	$⊢ (φ \land (E \neq 0 \land D = 0)) \to E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) = E^{2} (R^{2} - A^{2})$
139	113 125 138	3brtr4d	$⊢ (φ \land (E \neq 0 \land D = 0)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
140	139	ex	$⊢ φ \to ((E \neq 0 \land D = 0) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
141	99 140	biimtrrid	$⊢ φ \to ((B - Y \neq 0 \land X - A = 0) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
142	19 97 141	syl2and	$⊢ φ \to ((B \neq Y \land \neg A \neq X) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
143	142	imp	$⊢ (φ \land (B \neq Y \land \neg A \neq X)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
144		nne	$⊢ \neg B \neq Y \leftrightarrow B = Y$
145	13 15	subeq0ad	$⊢ φ \to (B - Y = 0 \leftrightarrow B = Y)$
146	145	biimprd	$⊢ φ \to (B = Y \to B - Y = 0)$
147	144 146	biimtrid	$⊢ φ \to (\neg B \neq Y \to B - Y = 0)$
148	6	eqeq1i	$⊢ E = 0 \leftrightarrow B - Y = 0$
149	148 29	anbi12i	$⊢ (E = 0 \land D \neq 0) \leftrightarrow (B - Y = 0 \land X - A \neq 0)$
150		0red	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 0 \in ℝ$
151	47	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D^{2} A^{2} \in ℝ$
152	54	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D^{2} (R^{2} - B^{2}) \in ℝ$
153	34	sqge0d	$⊢ φ \to 0 \leq D^{2}$
154	1	sqge0d	$⊢ φ \to 0 \leq A^{2}$
155	45 46 153 154	mulge0d	$⊢ φ \to 0 \leq D^{2} A^{2}$
156	155	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 0 \leq D^{2} A^{2}$
157	46	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to A^{2} \in ℝ$
158	53	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to R^{2} - B^{2} \in ℝ$
159		simprr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D \neq 0$
160	34 159 80	syl2an2r	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D^{2} \in ℝ^{+}$
161	43	recnd	$⊢ φ \to B^{2} \in ℂ$
162	46	recnd	$⊢ φ \to A^{2} \in ℂ$
163	161 162	addcomd	$⊢ φ \to B^{2} + A^{2} = A^{2} + B^{2}$
164	163 9	eqbrtrd	$⊢ φ \to B^{2} + A^{2} < R^{2}$
165	43 46 50	ltaddsub2d	$⊢ φ \to (B^{2} + A^{2} < R^{2} \leftrightarrow A^{2} < R^{2} - B^{2})$
166	164 165	mpbid	$⊢ φ \to A^{2} < R^{2} - B^{2}$
167	166	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to A^{2} < R^{2} - B^{2}$
168	157 158 160 167	ltmul2dd	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D^{2} A^{2} < D^{2} (R^{2} - B^{2})$
169	150 151 152 156 168	lelttrd	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 0 < D^{2} (R^{2} - B^{2})$
170		oveq1	$⊢ E = 0 \to E B = 0 \cdot B$
171	170	adantr	$⊢ (E = 0 \land D \neq 0) \to E B = 0 \cdot B$
172	13	mul02d	$⊢ φ \to 0 \cdot B = 0$
173	171 172	sylan9eqr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to E B = 0$
174	173	oveq2d	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D A E B = D A \cdot 0$
175	34	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D \in ℝ$
176	175	recnd	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D \in ℂ$
177	22	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to A \in ℂ$
178	176 177	mulcld	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D A \in ℂ$
179	178	mul01d	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D A \cdot 0 = 0$
180	174 179	eqtrd	$⊢ (φ \land (E = 0 \land D \neq 0)) \to D A E B = 0$
181	180	oveq2d	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 2 D A E B = 2 \cdot 0$
182	181 124	eqtrdi	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 2 D A E B = 0$
183		sq0i	$⊢ E = 0 \to E^{2} = 0$
184	183	adantr	$⊢ (E = 0 \land D \neq 0) \to E^{2} = 0$
185	184	adantl	$⊢ (φ \land (E = 0 \land D \neq 0)) \to E^{2} = 0$
186	185	oveq1d	$⊢ (φ \land (E = 0 \land D \neq 0)) \to E^{2} (R^{2} - A^{2}) = 0 \cdot (R^{2} - A^{2})$
187	51	recnd	$⊢ φ \to R^{2} - A^{2} \in ℂ$
188	187	mul02d	$⊢ φ \to 0 \cdot (R^{2} - A^{2}) = 0$
189	188	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 0 \cdot (R^{2} - A^{2}) = 0$
190	186 189	eqtrd	$⊢ (φ \land (E = 0 \land D \neq 0)) \to E^{2} (R^{2} - A^{2}) = 0$
191	190	oveq1d	$⊢ (φ \land (E = 0 \land D \neq 0)) \to E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) = 0 + D^{2} (R^{2} - B^{2})$
192	54	recnd	$⊢ φ \to D^{2} (R^{2} - B^{2}) \in ℂ$
193	192	addlidd	$⊢ φ \to 0 + D^{2} (R^{2} - B^{2}) = D^{2} (R^{2} - B^{2})$
194	193	adantr	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 0 + D^{2} (R^{2} - B^{2}) = D^{2} (R^{2} - B^{2})$
195	191 194	eqtrd	$⊢ (φ \land (E = 0 \land D \neq 0)) \to E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) = D^{2} (R^{2} - B^{2})$
196	169 182 195	3brtr4d	$⊢ (φ \land (E = 0 \land D \neq 0)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
197	196	ex	$⊢ φ \to ((E = 0 \land D \neq 0) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
198	149 197	biimtrrid	$⊢ φ \to ((B - Y = 0 \land X - A \neq 0) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
199	147 27 198	syl2and	$⊢ φ \to ((\neg B \neq Y \land A \neq X) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
200	199	imp	$⊢ (φ \land (\neg B \neq Y \land A \neq X)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
201		ioran	$⊢ \neg (B \neq Y \lor A \neq X) \leftrightarrow (\neg B \neq Y \land \neg A \neq X)$
202	10	pm2.24d	$⊢ φ \to (\neg (B \neq Y \lor A \neq X) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
203	201 202	biimtrrid	$⊢ φ \to ((\neg B \neq Y \land \neg A \neq X) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}))$
204	203	imp	$⊢ (φ \land (\neg B \neq Y \land \neg A \neq X)) \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
205	91 143 200 204	4casesdan	$⊢ φ \to 2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2})$
206	40 55	posdifd	$⊢ φ \to (2 D A E B < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) \leftrightarrow 0 < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) - 2 D A E B)$
207	205 206	mpbid	$⊢ φ \to 0 < E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) - 2 D A E B$
208	1 2 3 4 5 6 7 8 11 12	2itscplem3	$⊢ φ \to S = E^{2} (R^{2} - A^{2}) + D^{2} (R^{2} - B^{2}) - 2 D A E B$
209	207 208	breqtrrd	$⊢ φ \to 0 < S$

Metamath Proof Explorer

Theorem 2itscp

Proof