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

Proof

Step Hyp Ref Expression
1 requad2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 requad2.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 requad2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 requad2.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5 requad2.d ⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
6 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
8 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ≠ 0 )
9 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℂ )
11 4 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐶 ∈ ℂ )
13 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
15 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
16 7 8 10 12 14 15 quad ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
17 16 reubidva ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ∃! 𝑥 ∈ ℝ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
18 3 renegcld ⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
20 3 resqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
21 4re ⊢ 4 ∈ ℝ
22 21 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
23 1 4 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
24 22 23 remulcld ⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ )
25 20 24 resubcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℝ )
26 5 25 eqeltrd ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
27 resqrtcl ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
28 26 27 sylan ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
29 19 28 readdcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
30 2re ⊢ 2 ∈ ℝ
31 30 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
32 31 1 remulcld ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
34 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
35 2ne0 ⊢ 2 ≠ 0
36 35 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
37 34 6 36 2 mulne0d ⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
39 29 33 38 redivcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
40 19 28 resubcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
41 40 33 38 redivcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
42 euoreqb ⊢ ( ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ∧ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
43 39 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑥 ∈ ℝ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
44 9 negcld ⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
45 26 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
46 45 sqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
47 32 recnd ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
48 44 46 47 37 divdird ⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
50 44 46 47 37 divsubdird ⊢ ( 𝜑 → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
52 44 47 37 divcld ⊢ ( 𝜑 → ( - 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
54 46 47 37 divcld ⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
55 54 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
56 53 55 negsubd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 / ( 2 · 𝐴 ) ) + - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
57 46 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
58 47 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℂ )
59 57 58 38 divnegd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) )
60 59 oveq2d ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 / ( 2 · 𝐴 ) ) + - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
61 51 56 60 3eqtr2d ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
62 49 61 eqeq12d ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ) )
63 46 negcld ⊢ ( 𝜑 → - ( √ ‘ 𝐷 ) ∈ ℂ )
64 63 47 37 divcld ⊢ ( 𝜑 → ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
65 64 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
66 53 55 65 addcand ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ↔ ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
67 div11 ⊢ ( ( ( √ ‘ 𝐷 ) ∈ ℂ ∧ - ( √ ‘ 𝐷 ) ∈ ℂ ∧ ( ( 2 · 𝐴 ) ∈ ℂ ∧ ( 2 · 𝐴 ) ≠ 0 ) ) → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
68 46 63 47 37 67 syl112anc ⊢ ( 𝜑 → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
70 57 eqnegd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ ( √ ‘ 𝐷 ) = 0 ) )
71 sqrt00 ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
72 26 71 sylan ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
73 70 72 bitrd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ 𝐷 = 0 ) )
74 66 69 73 3bitrd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ↔ 𝐷 = 0 ) )
75 62 74 bitrd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ 𝐷 = 0 ) )
76 17 43 75 3bitrd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )
77 76 expcom ⊢ ( 0 ≤ 𝐷 → ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) ) )
78 1 2 3 4 5 requad01 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 0 ≤ 𝐷 ) )
79 78 notbid ⊢ ( 𝜑 → ( ¬ ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ¬ 0 ≤ 𝐷 ) )
80 79 biimparc ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ¬ ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
81 reurex ⊢ ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
82 80 81 nsyl ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ¬ ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
83 82 pm2.21d ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → 𝐷 = 0 ) )
84 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
85 26 84 ltnled ⊢ ( 𝜑 → ( 𝐷 < 0 ↔ ¬ 0 ≤ 𝐷 ) )
86 85 biimparc ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → 𝐷 < 0 )
87 86 lt0ne0d ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → 𝐷 ≠ 0 )
88 eqneqall ⊢ ( 𝐷 = 0 → ( 𝐷 ≠ 0 → ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
89 87 88 syl5com ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( 𝐷 = 0 → ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
90 83 89 impbid ⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )
91 90 ex ⊢ ( ¬ 0 ≤ 𝐷 → ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) ) )
92 77 91 pm2.61i ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )