Metamath Proof Explorer

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 < 𝐷 ) )