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