Theorem requad2

Description: A condition for a quadratic equation with real coefficients to have (exactly) two different real solutions. (Contributed by AV, 28-Jan-2023)

	Ref	Expression
Hypotheses	requad2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	requad2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	requad2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	requad2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	requad2.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion	requad2	⊢ ( 𝜑 → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ 0 < 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		requad2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		requad2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		requad2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		requad2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5		requad2.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
6	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝐴 ∈ ℂ )
8	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝐴 ≠ 0 )
9	3	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝐵 ∈ ℂ )
11	4	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
12	11	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝐶 ∈ ℂ )
13		elelpwi	⊢ ( ( 𝑥 ∈ 𝑝 ∧ 𝑝 ∈ 𝒫 ℝ ) → 𝑥 ∈ ℝ )
14	13	expcom	⊢ ( 𝑝 ∈ 𝒫 ℝ → ( 𝑥 ∈ 𝑝 → 𝑥 ∈ ℝ ) )
15	14	adantl	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) → ( 𝑥 ∈ 𝑝 → 𝑥 ∈ ℝ ) )
16	15	imp	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝑥 ∈ ℝ )
17	16	recnd	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝑥 ∈ ℂ )
18	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
19	7 8 10 12 17 18	quad	⊢ ( ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ 𝑥 ∈ 𝑝 ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
20	19	ralbidva	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
21	20	anbi2d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) ) )
22	21	reubidva	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) ) )
23		eqid	⊢ { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 } = { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 }
24	23	pairreueq	⊢ ( ∃! 𝑝 ∈ { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 } ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
25	24	bicomi	⊢ ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) ↔ ∃! 𝑝 ∈ { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 } ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
26	25	a1i	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) ↔ ∃! 𝑝 ∈ { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 } ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
27	3	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
28	27	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
29	3	resqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
30		4re	⊢ 4 ∈ ℝ
31	30	a1i	⊢ ( 𝜑 → 4 ∈ ℝ )
32	1 4	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
33	31 32	remulcld	⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ )
34	29 33	resubcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℝ )
35	5 34	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
36	35	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐷 ∈ ℝ )
37		simpr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 0 ≤ 𝐷 )
38	36 37	resqrtcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
39	28 38	readdcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
40		2re	⊢ 2 ∈ ℝ
41	40	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
42	41 1	remulcld	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
43	42	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
44		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
45	44	a1i	⊢ ( 𝜑 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
46		mulne0	⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( 2 · 𝐴 ) ≠ 0 )
47	45 6 2 46	syl12anc	⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
48	47	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
49	39 43 48	redivcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
50	3	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐵 ∈ ℝ )
51	50	renegcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
52	51 38	resubcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
53	40	a1i	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 2 ∈ ℝ )
54	1	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ∈ ℝ )
55	53 54	remulcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
56	52 55 48	redivcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
57		fveqeq2	⊢ ( 𝑞 = 𝑥 → ( ( ♯ ‘ 𝑞 ) = 2 ↔ ( ♯ ‘ 𝑥 ) = 2 ) )
58	57	cbvrabv	⊢ { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 } = { 𝑥 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑥 ) = 2 }
59	49 56 58	paireqne	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑝 ∈ { 𝑞 ∈ 𝒫 ℝ ∣ ( ♯ ‘ 𝑞 ) = 2 } ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ≠ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
60	9	negcld	⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
61	35	recnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
62	61	sqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
63	60 62	addcld	⊢ ( 𝜑 → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ )
64	60 62	subcld	⊢ ( 𝜑 → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ )
65		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
66	65 6	mulcld	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
67		div11	⊢ ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ ∧ ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ ∧ ( ( 2 · 𝐴 ) ∈ ℂ ∧ ( 2 · 𝐴 ) ≠ 0 ) ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( - 𝐵 + ( √ ‘ 𝐷 ) ) = ( - 𝐵 − ( √ ‘ 𝐷 ) ) ) )
68	63 64 66 47 67	syl112anc	⊢ ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( - 𝐵 + ( √ ‘ 𝐷 ) ) = ( - 𝐵 − ( √ ‘ 𝐷 ) ) ) )
69	60 62	negsubd	⊢ ( 𝜑 → ( - 𝐵 + - ( √ ‘ 𝐷 ) ) = ( - 𝐵 − ( √ ‘ 𝐷 ) ) )
70	69	eqcomd	⊢ ( 𝜑 → ( - 𝐵 − ( √ ‘ 𝐷 ) ) = ( - 𝐵 + - ( √ ‘ 𝐷 ) ) )
71	70	eqeq2d	⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) = ( - 𝐵 − ( √ ‘ 𝐷 ) ) ↔ ( - 𝐵 + ( √ ‘ 𝐷 ) ) = ( - 𝐵 + - ( √ ‘ 𝐷 ) ) ) )
72	62	negcld	⊢ ( 𝜑 → - ( √ ‘ 𝐷 ) ∈ ℂ )
73	60 62 72	addcand	⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) = ( - 𝐵 + - ( √ ‘ 𝐷 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
74	68 71 73	3bitrd	⊢ ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
75	74	necon3bid	⊢ ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ≠ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) ≠ - ( √ ‘ 𝐷 ) ) )
76	75	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ≠ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) ≠ - ( √ ‘ 𝐷 ) ) )
77		cnsqrt00	⊢ ( 𝐷 ∈ ℂ → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
78	61 77	syl	⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
79	78	necon3bid	⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) ≠ 0 ↔ 𝐷 ≠ 0 ) )
80	79	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) ≠ 0 ↔ 𝐷 ≠ 0 ) )
81	62	eqnegd	⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ ( √ ‘ 𝐷 ) = 0 ) )
82	81	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ ( √ ‘ 𝐷 ) = 0 ) )
83	82	necon3bid	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) ≠ - ( √ ‘ 𝐷 ) ↔ ( √ ‘ 𝐷 ) ≠ 0 ) )
84		0red	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 0 ∈ ℝ )
85	84 36 37	leltned	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 0 < 𝐷 ↔ 𝐷 ≠ 0 ) )
86	80 83 85	3bitr4d	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) ≠ - ( √ ‘ 𝐷 ) ↔ 0 < 𝐷 ) )
87	76 86	bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ≠ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ 0 < 𝐷 ) )
88	26 59 87	3bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) ↔ 0 < 𝐷 ) )
89	22 88	bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ 0 < 𝐷 ) )
90	89	expcom	⊢ ( 0 ≤ 𝐷 → ( 𝜑 → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ 0 < 𝐷 ) ) )
91		hash2prb	⊢ ( 𝑝 ∈ 𝒫 ℝ → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) )
92	91	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) )
93		raleq	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ∀ 𝑥 ∈ { 𝑎 , 𝑏 } ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
94		vex	⊢ 𝑎 ∈ V
95		vex	⊢ 𝑏 ∈ V
96		oveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
97	96	oveq2d	⊢ ( 𝑥 = 𝑎 → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( 𝑎 ↑ 2 ) ) )
98		oveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑎 ) )
99	98	oveq1d	⊢ ( 𝑥 = 𝑎 → ( ( 𝐵 · 𝑥 ) + 𝐶 ) = ( ( 𝐵 · 𝑎 ) + 𝐶 ) )
100	97 99	oveq12d	⊢ ( 𝑥 = 𝑎 → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) )
101	100	eqeq1d	⊢ ( 𝑥 = 𝑎 → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) = 0 ) )
102		oveq1	⊢ ( 𝑥 = 𝑏 → ( 𝑥 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
103	102	oveq2d	⊢ ( 𝑥 = 𝑏 → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( 𝑏 ↑ 2 ) ) )
104		oveq2	⊢ ( 𝑥 = 𝑏 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑏 ) )
105	104	oveq1d	⊢ ( 𝑥 = 𝑏 → ( ( 𝐵 · 𝑥 ) + 𝐶 ) = ( ( 𝐵 · 𝑏 ) + 𝐶 ) )
106	103 105	oveq12d	⊢ ( 𝑥 = 𝑏 → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) )
107	106	eqeq1d	⊢ ( 𝑥 = 𝑏 → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) )
108	94 95 101 107	ralpr	⊢ ( ∀ 𝑥 ∈ { 𝑎 , 𝑏 } ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) = 0 ∧ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) )
109	93 108	bitrdi	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) = 0 ∧ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) ) )
110	109	adantl	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) = 0 ∧ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) ) )
111	110	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) = 0 ∧ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) ) )
112		elelpwi	⊢ ( ( 𝑏 ∈ 𝑝 ∧ 𝑝 ∈ 𝒫 ℝ ) → 𝑏 ∈ ℝ )
113	112	ex	⊢ ( 𝑏 ∈ 𝑝 → ( 𝑝 ∈ 𝒫 ℝ → 𝑏 ∈ ℝ ) )
114	113	adantl	⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) → ( 𝑝 ∈ 𝒫 ℝ → 𝑏 ∈ ℝ ) )
115	114	com12	⊢ ( 𝑝 ∈ 𝒫 ℝ → ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) → 𝑏 ∈ ℝ ) )
116	115	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) → 𝑏 ∈ ℝ ) )
117	116	imp	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) → 𝑏 ∈ ℝ )
118		oveq1	⊢ ( 𝑦 = 𝑏 → ( 𝑦 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
119	118	oveq2d	⊢ ( 𝑦 = 𝑏 → ( 𝐴 · ( 𝑦 ↑ 2 ) ) = ( 𝐴 · ( 𝑏 ↑ 2 ) ) )
120		oveq2	⊢ ( 𝑦 = 𝑏 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑏 ) )
121	120	oveq1d	⊢ ( 𝑦 = 𝑏 → ( ( 𝐵 · 𝑦 ) + 𝐶 ) = ( ( 𝐵 · 𝑏 ) + 𝐶 ) )
122	119 121	oveq12d	⊢ ( 𝑦 = 𝑏 → ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) )
123	122	eqeq1d	⊢ ( 𝑦 = 𝑏 → ( ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) )
124	123	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) ∧ 𝑦 = 𝑏 ) → ( ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) )
125	117 124	rspcedv	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) → ( ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) )
126	125	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) )
127	126	adantld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ( ( 𝐴 · ( 𝑎 ↑ 2 ) ) + ( ( 𝐵 · 𝑎 ) + 𝐶 ) ) = 0 ∧ ( ( 𝐴 · ( 𝑏 ↑ 2 ) ) + ( ( 𝐵 · 𝑏 ) + 𝐶 ) ) = 0 ) → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) )
128	111 127	sylbid	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) )
129	128	ex	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑝 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) ) )
130	129	rexlimdvva	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) ) )
131	92 130	sylbid	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ( ♯ ‘ 𝑝 ) = 2 → ( ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) ) )
132	131	impd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝒫 ℝ ) → ( ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) )
133	132	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) → ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ) )
134	1 2 3 4 5	requad01	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( ( 𝐴 · ( 𝑦 ↑ 2 ) ) + ( ( 𝐵 · 𝑦 ) + 𝐶 ) ) = 0 ↔ 0 ≤ 𝐷 ) )
135	133 134	sylibd	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) → 0 ≤ 𝐷 ) )
136	135	con3d	⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ¬ ∃ 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ) )
137	136	impcom	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ¬ ∃ 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
138		reurex	⊢ ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) → ∃ 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
139	137 138	nsyl	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ¬ ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
140	139	pm2.21d	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) → 0 < 𝐷 ) )
141		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
142		ltle	⊢ ( ( 0 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 0 < 𝐷 → 0 ≤ 𝐷 ) )
143	141 35 142	syl2anc	⊢ ( 𝜑 → ( 0 < 𝐷 → 0 ≤ 𝐷 ) )
144		pm2.24	⊢ ( 0 ≤ 𝐷 → ( ¬ 0 ≤ 𝐷 → ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ) )
145	143 144	syl6	⊢ ( 𝜑 → ( 0 < 𝐷 → ( ¬ 0 ≤ 𝐷 → ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ) ) )
146	145	com23	⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ( 0 < 𝐷 → ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ) ) )
147	146	impcom	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( 0 < 𝐷 → ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ) )
148	140 147	impbid	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ 0 < 𝐷 ) )
149	148	ex	⊢ ( ¬ 0 ≤ 𝐷 → ( 𝜑 → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ 0 < 𝐷 ) ) )
150	90 149	pm2.61i	⊢ ( 𝜑 → ( ∃! 𝑝 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑝 ) = 2 ∧ ∀ 𝑥 ∈ 𝑝 ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) ↔ 0 < 𝐷 ) )