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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	2itscp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	2itscp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	2itscp.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	2itscp.d	⊢ 𝐷 = ( 𝑋 − 𝐴 )
	2itscp.e	⊢ 𝐸 = ( 𝐵 − 𝑌 )
	2itscp.c	⊢ 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) )
	2itscp.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
	2itscp.l	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
	2itscp.n	⊢ ( 𝜑 → ( 𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋 ) )
	2itscp.q	⊢ 𝑄 = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) )
	2itscp.s	⊢ 𝑆 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion	2itscp	⊢ ( 𝜑 → 0 < 𝑆 )

Proof

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

Metamath Proof Explorer

Theorem 2itscp

Proof