Metamath Proof Explorer

Theorem requad1

Description: A condition for a quadratic equation with real coefficients to have (exactly) one real solution. (Contributed by AV, 26-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 requad1 
|- ( ph -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) )

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 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> A e. CC )
8 2 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> A =/= 0 )
9 3 recnd 
 |-  ( ph -> B e. CC )
10 9 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> B e. CC )
11 4 recnd 
 |-  ( ph -> C e. CC )
12 11 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> C e. CC )
13 recn 
 |-  ( x e. RR -> x e. CC )
14 13 adantl 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> x e. CC )
15 5 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
16 7 8 10 12 14 15 quad 
 |-  ( ( ( ph /\ 0 <_ D ) /\ x e. RR ) -> ( ( ( 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 ) ) ) ) )
17 16 reubidva 
 |-  ( ( ph /\ 0 <_ D ) -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> E! x e. RR ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) ) )
18 3 renegcld 
 |-  ( ph -> -u B e. RR )
19 18 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> -u B e. RR )
20 3 resqcld 
 |-  ( ph -> ( B ^ 2 ) e. RR )
21 4re 
 |-  4 e. RR
22 21 a1i 
 |-  ( ph -> 4 e. RR )
23 1 4 remulcld 
 |-  ( ph -> ( A x. C ) e. RR )
24 22 23 remulcld 
 |-  ( ph -> ( 4 x. ( A x. C ) ) e. RR )
25 20 24 resubcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. RR )
26 5 25 eqeltrd 
 |-  ( ph -> D e. RR )
27 resqrtcl 
 |-  ( ( D e. RR /\ 0 <_ D ) -> ( sqrt ` D ) e. RR )
28 26 27 sylan 
 |-  ( ( ph /\ 0 <_ D ) -> ( sqrt ` D ) e. RR )
29 19 28 readdcld 
 |-  ( ( ph /\ 0 <_ D ) -> ( -u B + ( sqrt ` D ) ) e. RR )
30 2re 
 |-  2 e. RR
31 30 a1i 
 |-  ( ph -> 2 e. RR )
32 31 1 remulcld 
 |-  ( ph -> ( 2 x. A ) e. RR )
33 32 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( 2 x. A ) e. RR )
34 2cnd 
 |-  ( ph -> 2 e. CC )
35 2ne0 
 |-  2 =/= 0
36 35 a1i 
 |-  ( ph -> 2 =/= 0 )
37 34 6 36 2 mulne0d 
 |-  ( ph -> ( 2 x. A ) =/= 0 )
38 37 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( 2 x. A ) =/= 0 )
39 29 33 38 redivcld 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
40 19 28 resubcld 
 |-  ( ( ph /\ 0 <_ D ) -> ( -u B - ( sqrt ` D ) ) e. RR )
41 40 33 38 redivcld 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
42 euoreqb 
 |-  ( ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR /\ ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) -> ( E! x e. RR ( 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 ) ) ) )
43 39 41 42 syl2anc 
 |-  ( ( ph /\ 0 <_ D ) -> ( E! x e. RR ( 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 ) ) ) )
44 9 negcld 
 |-  ( ph -> -u B e. CC )
45 26 recnd 
 |-  ( ph -> D e. CC )
46 45 sqrtcld 
 |-  ( ph -> ( sqrt ` D ) e. CC )
47 32 recnd 
 |-  ( ph -> ( 2 x. A ) e. CC )
48 44 46 47 37 divdird 
 |-  ( ph -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
49 48 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
50 44 46 47 37 divsubdird 
 |-  ( ph -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) - ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
51 50 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) - ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
52 44 47 37 divcld 
 |-  ( ph -> ( -u B / ( 2 x. A ) ) e. CC )
53 52 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( -u B / ( 2 x. A ) ) e. CC )
54 46 47 37 divcld 
 |-  ( ph -> ( ( sqrt ` D ) / ( 2 x. A ) ) e. CC )
55 54 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( sqrt ` D ) / ( 2 x. A ) ) e. CC )
56 53 55 negsubd 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B / ( 2 x. A ) ) + -u ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) - ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
57 46 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( sqrt ` D ) e. CC )
58 47 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( 2 x. A ) e. CC )
59 57 58 38 divnegd 
 |-  ( ( ph /\ 0 <_ D ) -> -u ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) )
60 59 oveq2d 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B / ( 2 x. A ) ) + -u ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) )
61 51 56 60 3eqtr2d 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) )
62 49 61 eqeq12d 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) <-> ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) ) )
63 46 negcld 
 |-  ( ph -> -u ( sqrt ` D ) e. CC )
64 63 47 37 divcld 
 |-  ( ph -> ( -u ( sqrt ` D ) / ( 2 x. A ) ) e. CC )
65 64 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( -u ( sqrt ` D ) / ( 2 x. A ) ) e. CC )
66 53 55 65 addcand 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) <-> ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) )
67 div11 
 |-  ( ( ( sqrt ` D ) e. CC /\ -u ( sqrt ` D ) e. CC /\ ( ( 2 x. A ) e. CC /\ ( 2 x. A ) =/= 0 ) ) -> ( ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) <-> ( sqrt ` D ) = -u ( sqrt ` D ) ) )
68 46 63 47 37 67 syl112anc 
 |-  ( ph -> ( ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) <-> ( sqrt ` D ) = -u ( sqrt ` D ) ) )
69 68 adantr 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) <-> ( sqrt ` D ) = -u ( sqrt ` D ) ) )
70 57 eqnegd 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( sqrt ` D ) = -u ( sqrt ` D ) <-> ( sqrt ` D ) = 0 ) )
71 sqrt00 
 |-  ( ( D e. RR /\ 0 <_ D ) -> ( ( sqrt ` D ) = 0 <-> D = 0 ) )
72 26 71 sylan 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( sqrt ` D ) = 0 <-> D = 0 ) )
73 70 72 bitrd 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( sqrt ` D ) = -u ( sqrt ` D ) <-> D = 0 ) )
74 66 69 73 3bitrd 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) <-> D = 0 ) )
75 62 74 bitrd 
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) <-> D = 0 ) )
76 17 43 75 3bitrd 
 |-  ( ( ph /\ 0 <_ D ) -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) )
77 76 expcom 
 |-  ( 0 <_ D -> ( ph -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) ) )
78 1 2 3 4 5 requad01 
 |-  ( ph -> ( E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> 0 <_ D ) )
79 78 notbid 
 |-  ( ph -> ( -. E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> -. 0 <_ D ) )
80 79 biimparc 
 |-  ( ( -. 0 <_ D /\ ph ) -> -. E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 )
81 reurex 
 |-  ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 -> E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 )
82 80 81 nsyl 
 |-  ( ( -. 0 <_ D /\ ph ) -> -. E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 )
83 82 pm2.21d 
 |-  ( ( -. 0 <_ D /\ ph ) -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 -> D = 0 ) )
84 0red 
 |-  ( ph -> 0 e. RR )
85 26 84 ltnled 
 |-  ( ph -> ( D < 0 <-> -. 0 <_ D ) )
86 85 biimparc 
 |-  ( ( -. 0 <_ D /\ ph ) -> D < 0 )
87 86 lt0ne0d 
 |-  ( ( -. 0 <_ D /\ ph ) -> D =/= 0 )
88 eqneqall 
 |-  ( D = 0 -> ( D =/= 0 -> E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 ) )
89 87 88 syl5com 
 |-  ( ( -. 0 <_ D /\ ph ) -> ( D = 0 -> E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 ) )
90 83 89 impbid 
 |-  ( ( -. 0 <_ D /\ ph ) -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) )
91 90 ex 
 |-  ( -. 0 <_ D -> ( ph -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) ) )
92 77 91 pm2.61i 
 |-  ( ph -> ( E! x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) )