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
|- ( ph -> A e. RR )
requad2.z
|- ( ph -> A =/= 0 )
requad2.b
|- ( ph -> B e. RR )
requad2.c
|- ( ph -> C e. RR )
requad2.d
|- ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
Assertion requad2
|- ( ph -> ( E! p e. ~P RR ( ( # ` p ) = 2 /\ A. x e. p ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 ) <-> 0 < D ) )

Proof

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