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 ( 𝜑𝐴 ∈ ℂ )
quad1.z ( 𝜑𝐴 ≠ 0 )
quad1.b ( 𝜑𝐵 ∈ ℂ )
quad1.c ( 𝜑𝐶 ∈ ℂ )
quad1.d ( 𝜑𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion quad1 ( 𝜑 → ( ∃! 𝑥 ∈ ℂ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )

Proof

Step Hyp Ref Expression
1 quad1.a ( 𝜑𝐴 ∈ ℂ )
2 quad1.z ( 𝜑𝐴 ≠ 0 )
3 quad1.b ( 𝜑𝐵 ∈ ℂ )
4 quad1.c ( 𝜑𝐶 ∈ ℂ )
5 quad1.d ( 𝜑𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
6 1 adantr ( ( 𝜑𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
7 2 adantr ( ( 𝜑𝑥 ∈ ℂ ) → 𝐴 ≠ 0 )
8 3 adantr ( ( 𝜑𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
9 4 adantr ( ( 𝜑𝑥 ∈ ℂ ) → 𝐶 ∈ ℂ )
10 simpr ( ( 𝜑𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
11 5 adantr ( ( 𝜑𝑥 ∈ ℂ ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
12 6 7 8 9 10 11 quad ( ( 𝜑𝑥 ∈ ℂ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
13 12 reubidva ( 𝜑 → ( ∃! 𝑥 ∈ ℂ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ∃! 𝑥 ∈ ℂ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
14 3 negcld ( 𝜑 → - 𝐵 ∈ ℂ )
15 3 sqcld ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
16 4cn 4 ∈ ℂ
17 16 a1i ( 𝜑 → 4 ∈ ℂ )
18 1 4 mulcld ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
19 17 18 mulcld ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
20 15 19 subcld ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ )
21 5 20 eqeltrd ( 𝜑𝐷 ∈ ℂ )
22 21 sqrtcld ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
23 14 22 addcld ( 𝜑 → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ )
24 2cnd ( 𝜑 → 2 ∈ ℂ )
25 24 1 mulcld ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
26 2ne0 2 ≠ 0
27 26 a1i ( 𝜑 → 2 ≠ 0 )
28 24 1 27 2 mulne0d ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
29 23 25 28 divcld ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
30 14 22 subcld ( 𝜑 → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ )
31 30 25 28 divcld ( 𝜑 → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
32 euoreqb ( ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ ∧ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ ) → ( ∃! 𝑥 ∈ ℂ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
33 29 31 32 syl2anc ( 𝜑 → ( ∃! 𝑥 ∈ ℂ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
34 14 22 25 28 divdird ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
35 14 22 25 28 divsubdird ( 𝜑 → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
36 14 25 28 divcld ( 𝜑 → ( - 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
37 22 25 28 divcld ( 𝜑 → ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
38 36 37 negsubd ( 𝜑 → ( ( - 𝐵 / ( 2 · 𝐴 ) ) + - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
39 22 25 28 divnegd ( 𝜑 → - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) )
40 39 oveq2d ( 𝜑 → ( ( - 𝐵 / ( 2 · 𝐴 ) ) + - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
41 35 38 40 3eqtr2d ( 𝜑 → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
42 34 41 eqeq12d ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ) )
43 22 negcld ( 𝜑 → - ( √ ‘ 𝐷 ) ∈ ℂ )
44 43 25 28 divcld ( 𝜑 → ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
45 36 37 44 addcand ( 𝜑 → ( ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ↔ ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
46 div11 ( ( ( √ ‘ 𝐷 ) ∈ ℂ ∧ - ( √ ‘ 𝐷 ) ∈ ℂ ∧ ( ( 2 · 𝐴 ) ∈ ℂ ∧ ( 2 · 𝐴 ) ≠ 0 ) ) → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
47 22 43 25 28 46 syl112anc ( 𝜑 → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
48 22 eqnegd ( 𝜑 → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ ( √ ‘ 𝐷 ) = 0 ) )
49 cnsqrt00 ( 𝐷 ∈ ℂ → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
50 21 49 syl ( 𝜑 → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
51 48 50 bitrd ( 𝜑 → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ 𝐷 = 0 ) )
52 45 47 51 3bitrd ( 𝜑 → ( ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ↔ 𝐷 = 0 ) )
53 42 52 bitrd ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ 𝐷 = 0 ) )
54 13 33 53 3bitrd ( 𝜑 → ( ∃! 𝑥 ∈ ℂ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )