Metamath Proof Explorer

Theorem quad1

Description: A condition for a quadratic equation with complex coefficients to have (exactly) one complex solution. (Contributed by AV, 23-Jan-2023)

Ref Expression
Hypotheses quad1.a 
|- ( ph -> A e. CC )
quad1.z 
|- ( ph -> A =/= 0 )
quad1.b 
|- ( ph -> B e. CC )
quad1.c 
|- ( ph -> C e. CC )
quad1.d 
|- ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
Assertion quad1 
|- ( ph -> ( E! x e. CC ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) )

Proof

Step Hyp Ref Expression
1 quad1.a 
 |-  ( ph -> A e. CC )
2 quad1.z 
 |-  ( ph -> A =/= 0 )
3 quad1.b 
 |-  ( ph -> B e. CC )
4 quad1.c 
 |-  ( ph -> C e. CC )
5 quad1.d 
 |-  ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
6 1 adantr 
 |-  ( ( ph /\ x e. CC ) -> A e. CC )
7 2 adantr 
 |-  ( ( ph /\ x e. CC ) -> A =/= 0 )
8 3 adantr 
 |-  ( ( ph /\ x e. CC ) -> B e. CC )
9 4 adantr 
 |-  ( ( ph /\ x e. CC ) -> C e. CC )
10 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
11 5 adantr 
 |-  ( ( ph /\ x e. CC ) -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
12 6 7 8 9 10 11 quad 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( 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 ) ) ) ) )
13 12 reubidva 
 |-  ( ph -> ( E! x e. CC ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> E! x e. CC ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) ) )
14 3 negcld 
 |-  ( ph -> -u B e. CC )
15 3 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
16 4cn 
 |-  4 e. CC
17 16 a1i 
 |-  ( ph -> 4 e. CC )
18 1 4 mulcld 
 |-  ( ph -> ( A x. C ) e. CC )
19 17 18 mulcld 
 |-  ( ph -> ( 4 x. ( A x. C ) ) e. CC )
20 15 19 subcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. CC )
21 5 20 eqeltrd 
 |-  ( ph -> D e. CC )
22 21 sqrtcld 
 |-  ( ph -> ( sqrt ` D ) e. CC )
23 14 22 addcld 
 |-  ( ph -> ( -u B + ( sqrt ` D ) ) e. CC )
24 2cnd 
 |-  ( ph -> 2 e. CC )
25 24 1 mulcld 
 |-  ( ph -> ( 2 x. A ) e. CC )
26 2ne0 
 |-  2 =/= 0
27 26 a1i 
 |-  ( ph -> 2 =/= 0 )
28 24 1 27 2 mulne0d 
 |-  ( ph -> ( 2 x. A ) =/= 0 )
29 23 25 28 divcld 
 |-  ( ph -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. CC )
30 14 22 subcld 
 |-  ( ph -> ( -u B - ( sqrt ` D ) ) e. CC )
31 30 25 28 divcld 
 |-  ( ph -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. CC )
32 euoreqb 
 |-  ( ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. CC /\ ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. CC ) -> ( E! x e. CC ( 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 ) ) ) )
33 29 31 32 syl2anc 
 |-  ( ph -> ( E! x e. CC ( 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 ) ) ) )
34 14 22 25 28 divdird 
 |-  ( ph -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
35 14 22 25 28 divsubdird 
 |-  ( ph -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) - ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
36 14 25 28 divcld 
 |-  ( ph -> ( -u B / ( 2 x. A ) ) e. CC )
37 22 25 28 divcld 
 |-  ( ph -> ( ( sqrt ` D ) / ( 2 x. A ) ) e. CC )
38 36 37 negsubd 
 |-  ( ph -> ( ( -u B / ( 2 x. A ) ) + -u ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) - ( ( sqrt ` D ) / ( 2 x. A ) ) ) )
39 22 25 28 divnegd 
 |-  ( ph -> -u ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) )
40 39 oveq2d 
 |-  ( ph -> ( ( -u B / ( 2 x. A ) ) + -u ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) )
41 35 38 40 3eqtr2d 
 |-  ( ph -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) )
42 34 41 eqeq12d 
 |-  ( ph -> ( ( ( -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 ) ) ) ) )
43 22 negcld 
 |-  ( ph -> -u ( sqrt ` D ) e. CC )
44 43 25 28 divcld 
 |-  ( ph -> ( -u ( sqrt ` D ) / ( 2 x. A ) ) e. CC )
45 36 37 44 addcand 
 |-  ( ph -> ( ( ( -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 ) ) ) )
46 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 ) ) )
47 22 43 25 28 46 syl112anc 
 |-  ( ph -> ( ( ( sqrt ` D ) / ( 2 x. A ) ) = ( -u ( sqrt ` D ) / ( 2 x. A ) ) <-> ( sqrt ` D ) = -u ( sqrt ` D ) ) )
48 22 eqnegd 
 |-  ( ph -> ( ( sqrt ` D ) = -u ( sqrt ` D ) <-> ( sqrt ` D ) = 0 ) )
49 cnsqrt00 
 |-  ( D e. CC -> ( ( sqrt ` D ) = 0 <-> D = 0 ) )
50 21 49 syl 
 |-  ( ph -> ( ( sqrt ` D ) = 0 <-> D = 0 ) )
51 48 50 bitrd 
 |-  ( ph -> ( ( sqrt ` D ) = -u ( sqrt ` D ) <-> D = 0 ) )
52 45 47 51 3bitrd 
 |-  ( ph -> ( ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` D ) / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` D ) / ( 2 x. A ) ) ) <-> D = 0 ) )
53 42 52 bitrd 
 |-  ( ph -> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) <-> D = 0 ) )
54 13 33 53 3bitrd 
 |-  ( ph -> ( E! x e. CC ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> D = 0 ) )