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