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