Metamath Proof Explorer

Theorem requad01

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

Ref Expression
Hypotheses requad2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
requad2.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
requad2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
requad2.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
requad2.d ⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion requad01 ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 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 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ≠ 0 )
9 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℂ )
11 4 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐶 ∈ ℂ )
13 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
16 7 8 10 12 14 15 quad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
17 eleq1 ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
19 2re ⊢ 2 ∈ ℝ
20 19 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
21 20 1 remulcld ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
23 9 negcld ⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
24 3 resqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
25 4re ⊢ 4 ∈ ℝ
26 25 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
27 1 4 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
28 26 27 remulcld ⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ )
29 24 28 resubcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℝ )
30 5 29 eqeltrd ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
31 30 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
32 31 sqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
33 23 32 addcld ⊢ ( 𝜑 → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ )
34 33 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ )
35 3 renegcld ⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
36 35 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
37 32 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
38 31 negnegd ⊢ ( 𝜑 → - - 𝐷 = 𝐷 )
39 38 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → - - 𝐷 = 𝐷 )
40 39 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → 𝐷 = - - 𝐷 )
41 40 fveq2d ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) = ( √ ‘ - - 𝐷 ) )
42 30 renegcld ⊢ ( 𝜑 → - 𝐷 ∈ ℝ )
43 42 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → - 𝐷 ∈ ℝ )
44 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
45 30 44 ltnled ⊢ ( 𝜑 → ( 𝐷 < 0 ↔ ¬ 0 ≤ 𝐷 ) )
46 ltle ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐷 < 0 → 𝐷 ≤ 0 ) )
47 30 44 46 syl2anc ⊢ ( 𝜑 → ( 𝐷 < 0 → 𝐷 ≤ 0 ) )
48 45 47 sylbird ⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → 𝐷 ≤ 0 ) )
49 48 imp ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → 𝐷 ≤ 0 )
50 30 le0neg1d ⊢ ( 𝜑 → ( 𝐷 ≤ 0 ↔ 0 ≤ - 𝐷 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( 𝐷 ≤ 0 ↔ 0 ≤ - 𝐷 ) )
52 49 51 mpbid ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → 0 ≤ - 𝐷 )
53 43 52 sqrtnegd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - - 𝐷 ) = ( i · ( √ ‘ - 𝐷 ) ) )
54 41 53 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) = ( i · ( √ ‘ - 𝐷 ) ) )
55 ax-icn ⊢ i ∈ ℂ
56 55 a1i ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → i ∈ ℂ )
57 31 negcld ⊢ ( 𝜑 → - 𝐷 ∈ ℂ )
58 57 sqrtcld ⊢ ( 𝜑 → ( √ ‘ - 𝐷 ) ∈ ℂ )
59 58 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - 𝐷 ) ∈ ℂ )
60 56 59 mulcomd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( i · ( √ ‘ - 𝐷 ) ) = ( ( √ ‘ - 𝐷 ) · i ) )
61 43 52 resqrtcld ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - 𝐷 ) ∈ ℝ )
62 inelr ⊢ ¬ i ∈ ℝ
63 eldif ⊢ ( i ∈ ( ℂ ∖ ℝ ) ↔ ( i ∈ ℂ ∧ ¬ i ∈ ℝ ) )
64 55 62 63 mpbir2an ⊢ i ∈ ( ℂ ∖ ℝ )
65 64 a1i ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → i ∈ ( ℂ ∖ ℝ ) )
66 30 lt0neg1d ⊢ ( 𝜑 → ( 𝐷 < 0 ↔ 0 < - 𝐷 ) )
67 ltne ⊢ ( ( 0 ∈ ℝ ∧ 0 < - 𝐷 ) → - 𝐷 ≠ 0 )
68 44 67 sylan ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → - 𝐷 ≠ 0 )
69 42 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → - 𝐷 ∈ ℝ )
70 ltle ⊢ ( ( 0 ∈ ℝ ∧ - 𝐷 ∈ ℝ ) → ( 0 < - 𝐷 → 0 ≤ - 𝐷 ) )
71 44 42 70 syl2anc ⊢ ( 𝜑 → ( 0 < - 𝐷 → 0 ≤ - 𝐷 ) )
72 71 imp ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → 0 ≤ - 𝐷 )
73 sqrt00 ⊢ ( ( - 𝐷 ∈ ℝ ∧ 0 ≤ - 𝐷 ) → ( ( √ ‘ - 𝐷 ) = 0 ↔ - 𝐷 = 0 ) )
74 69 72 73 syl2anc ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( ( √ ‘ - 𝐷 ) = 0 ↔ - 𝐷 = 0 ) )
75 74 bicomd ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( - 𝐷 = 0 ↔ ( √ ‘ - 𝐷 ) = 0 ) )
76 75 necon3bid ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( - 𝐷 ≠ 0 ↔ ( √ ‘ - 𝐷 ) ≠ 0 ) )
77 68 76 mpbid ⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( √ ‘ - 𝐷 ) ≠ 0 )
78 77 ex ⊢ ( 𝜑 → ( 0 < - 𝐷 → ( √ ‘ - 𝐷 ) ≠ 0 ) )
79 66 78 sylbid ⊢ ( 𝜑 → ( 𝐷 < 0 → ( √ ‘ - 𝐷 ) ≠ 0 ) )
80 45 79 sylbird ⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ( √ ‘ - 𝐷 ) ≠ 0 ) )
81 80 imp ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - 𝐷 ) ≠ 0 )
82 61 65 81 recnmulnred ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( ( √ ‘ - 𝐷 ) · i ) ∉ ℝ )
83 df-nel ⊢ ( ( ( √ ‘ - 𝐷 ) · i ) ∉ ℝ ↔ ¬ ( ( √ ‘ - 𝐷 ) · i ) ∈ ℝ )
84 82 83 sylib ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( ( √ ‘ - 𝐷 ) · i ) ∈ ℝ )
85 60 84 eqneltrd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( i · ( √ ‘ - 𝐷 ) ) ∈ ℝ )
86 54 85 eqneltrd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( √ ‘ 𝐷 ) ∈ ℝ )
87 37 86 eldifd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ( ℂ ∖ ℝ ) )
88 36 87 readdcnnred ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∉ ℝ )
89 df-nel ⊢ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∉ ℝ ↔ ¬ ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
90 88 89 sylib ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
91 34 90 eldifd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ( ℂ ∖ ℝ ) )
92 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
93 2ne0 ⊢ 2 ≠ 0
94 93 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
95 92 6 94 2 mulne0d ⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
96 95 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
97 22 91 96 cndivrenred ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ )
98 df-nel ⊢ ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ ↔ ¬ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
99 97 98 sylib ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
100 99 ex ⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ¬ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
101 100 con4d ⊢ ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
103 18 102 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) )
104 103 ex ⊢ ( 𝜑 → ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) ) )
105 eleq1 ⊢ ( 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
106 105 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
107 23 32 subcld ⊢ ( 𝜑 → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ )
108 107 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ )
109 36 87 resubcnnred ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∉ ℝ )
110 df-nel ⊢ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∉ ℝ ↔ ¬ ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
111 109 110 sylib ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
112 108 111 eldifd ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ( ℂ ∖ ℝ ) )
113 22 112 96 cndivrenred ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ )
114 df-nel ⊢ ( ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ ↔ ¬ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
115 113 114 sylib ⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
116 115 ex ⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ¬ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
117 116 con4d ⊢ ( 𝜑 → ( ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
119 106 118 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) )
120 119 ex ⊢ ( 𝜑 → ( 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) ) )
121 104 120 jaod ⊢ ( 𝜑 → ( ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) ) )
122 121 com23 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ → ( ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → 0 ≤ 𝐷 ) ) )
123 122 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → 0 ≤ 𝐷 ) )
124 16 123 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → 0 ≤ 𝐷 ) )
125 124 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → 0 ≤ 𝐷 ) )
126 35 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
127 30 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐷 ∈ ℝ )
128 simpr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 0 ≤ 𝐷 )
129 127 128 resqrtcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
130 126 129 readdcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
131 19 a1i ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 2 ∈ ℝ )
132 1 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ∈ ℝ )
133 131 132 remulcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
134 95 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
135 130 133 134 redivcld ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
136 oveq1 ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ↑ 2 ) = ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) )
137 136 oveq2d ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) )
138 oveq2 ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
139 138 oveq1d ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( ( 𝐵 · 𝑥 ) + 𝐶 ) = ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) )
140 137 139 oveq12d ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) )
141 140 eqeq1d ⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 ) )
142 141 adantl ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 ) )
143 eqidd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) )
144 143 orcd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
145 6 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ∈ ℂ )
146 2 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ≠ 0 )
147 9 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐵 ∈ ℂ )
148 11 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐶 ∈ ℂ )
149 92 6 mulcld ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
150 33 149 95 divcld ⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
151 150 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
152 5 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
153 145 146 147 148 151 152 quad ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 ↔ ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
154 144 153 mpbird ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 )
155 135 142 154 rspcedvd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
156 155 ex ⊢ ( 𝜑 → ( 0 ≤ 𝐷 → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
157 125 156 impbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 0 ≤ 𝐷 ) )