Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  requad01 Structured version   Visualization version   GIF version

Theorem requad01 45325
Description: A condition for a quadratic equation with real coefficients to have (at least) one real solution. (Contributed by AV, 23-Jan-2023.)
Hypotheses
Ref Expression
requad2.a (𝜑𝐴 ∈ ℝ)
requad2.z (𝜑𝐴 ≠ 0)
requad2.b (𝜑𝐵 ∈ ℝ)
requad2.c (𝜑𝐶 ∈ ℝ)
requad2.d (𝜑𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
Assertion
Ref Expression
requad01 (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷   𝜑,𝑥

Proof of Theorem requad01
StepHypRef Expression
1 requad2.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
21recnd 11076 . . . . . 6 (𝜑𝐴 ∈ ℂ)
32adantr 481 . . . . 5 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℂ)
4 requad2.z . . . . . 6 (𝜑𝐴 ≠ 0)
54adantr 481 . . . . 5 ((𝜑𝑥 ∈ ℝ) → 𝐴 ≠ 0)
6 requad2.b . . . . . . 7 (𝜑𝐵 ∈ ℝ)
76recnd 11076 . . . . . 6 (𝜑𝐵 ∈ ℂ)
87adantr 481 . . . . 5 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℂ)
9 requad2.c . . . . . . 7 (𝜑𝐶 ∈ ℝ)
109recnd 11076 . . . . . 6 (𝜑𝐶 ∈ ℂ)
1110adantr 481 . . . . 5 ((𝜑𝑥 ∈ ℝ) → 𝐶 ∈ ℂ)
12 recn 11034 . . . . . 6 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
1312adantl 482 . . . . 5 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
14 requad2.d . . . . . 6 (𝜑𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
1514adantr 481 . . . . 5 ((𝜑𝑥 ∈ ℝ) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
163, 5, 8, 11, 13, 15quad 26062 . . . 4 ((𝜑𝑥 ∈ ℝ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
17 eleq1 2825 . . . . . . . . . 10 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
1817adantl 482 . . . . . . . . 9 ((𝜑𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
19 2re 12120 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
2019a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℝ)
2120, 1remulcld 11078 . . . . . . . . . . . . . . 15 (𝜑 → (2 · 𝐴) ∈ ℝ)
2221adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ)
237negcld 11392 . . . . . . . . . . . . . . . . 17 (𝜑 → -𝐵 ∈ ℂ)
246resqcld 14038 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵↑2) ∈ ℝ)
25 4re 12130 . . . . . . . . . . . . . . . . . . . . . . 23 4 ∈ ℝ
2625a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 4 ∈ ℝ)
271, 9remulcld 11078 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
2826, 27remulcld 11078 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℝ)
2924, 28resubcld 11476 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℝ)
3014, 29eqeltrd 2838 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ∈ ℝ)
3130recnd 11076 . . . . . . . . . . . . . . . . . 18 (𝜑𝐷 ∈ ℂ)
3231sqrtcld 15221 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘𝐷) ∈ ℂ)
3323, 32addcld 11067 . . . . . . . . . . . . . . . 16 (𝜑 → (-𝐵 + (√‘𝐷)) ∈ ℂ)
3433adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∈ ℂ)
356renegcld 11475 . . . . . . . . . . . . . . . . . 18 (𝜑 → -𝐵 ∈ ℝ)
3635adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → -𝐵 ∈ ℝ)
3732adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℂ)
3831negnegd 11396 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → --𝐷 = 𝐷)
3938adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → --𝐷 = 𝐷)
4039eqcomd 2743 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → 𝐷 = --𝐷)
4140fveq2d 6815 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) = (√‘--𝐷))
4230renegcld 11475 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -𝐷 ∈ ℝ)
4342adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → -𝐷 ∈ ℝ)
44 0red 11051 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 0 ∈ ℝ)
4530, 44ltnled 11195 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐷 < 0 ↔ ¬ 0 ≤ 𝐷))
46 ltle 11136 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐷 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐷 < 0 → 𝐷 ≤ 0))
4730, 44, 46syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐷 < 0 → 𝐷 ≤ 0))
4845, 47sylbird 259 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (¬ 0 ≤ 𝐷𝐷 ≤ 0))
4948imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → 𝐷 ≤ 0)
5030le0neg1d 11619 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐷 ≤ 0 ↔ 0 ≤ -𝐷))
5150adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (𝐷 ≤ 0 ↔ 0 ≤ -𝐷))
5249, 51mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → 0 ≤ -𝐷)
5343, 52sqrtnegd 15205 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘--𝐷) = (i · (√‘-𝐷)))
5441, 53eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) = (i · (√‘-𝐷)))
55 ax-icn 11003 . . . . . . . . . . . . . . . . . . . . . 22 i ∈ ℂ
5655a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → i ∈ ℂ)
5731negcld 11392 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → -𝐷 ∈ ℂ)
5857sqrtcld 15221 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (√‘-𝐷) ∈ ℂ)
5958adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘-𝐷) ∈ ℂ)
6056, 59mulcomd 11069 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (i · (√‘-𝐷)) = ((√‘-𝐷) · i))
6143, 52resqrtcld 15201 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘-𝐷) ∈ ℝ)
62 inelr 12036 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ i ∈ ℝ
63 eldif 3907 . . . . . . . . . . . . . . . . . . . . . . . 24 (i ∈ (ℂ ∖ ℝ) ↔ (i ∈ ℂ ∧ ¬ i ∈ ℝ))
6455, 62, 63mpbir2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 i ∈ (ℂ ∖ ℝ)
6564a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → i ∈ (ℂ ∖ ℝ))
6630lt0neg1d 11617 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐷 < 0 ↔ 0 < -𝐷))
67 ltne 11145 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0 ∈ ℝ ∧ 0 < -𝐷) → -𝐷 ≠ 0)
6844, 67sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 0 < -𝐷) → -𝐷 ≠ 0)
6942adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ 0 < -𝐷) → -𝐷 ∈ ℝ)
70 ltle 11136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ ℝ ∧ -𝐷 ∈ ℝ) → (0 < -𝐷 → 0 ≤ -𝐷))
7144, 42, 70syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (0 < -𝐷 → 0 ≤ -𝐷))
7271imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ 0 < -𝐷) → 0 ≤ -𝐷)
73 sqrt00 15047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((-𝐷 ∈ ℝ ∧ 0 ≤ -𝐷) → ((√‘-𝐷) = 0 ↔ -𝐷 = 0))
7469, 72, 73syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ 0 < -𝐷) → ((√‘-𝐷) = 0 ↔ -𝐷 = 0))
7574bicomd 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ 0 < -𝐷) → (-𝐷 = 0 ↔ (√‘-𝐷) = 0))
7675necon3bid 2986 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 0 < -𝐷) → (-𝐷 ≠ 0 ↔ (√‘-𝐷) ≠ 0))
7768, 76mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 0 < -𝐷) → (√‘-𝐷) ≠ 0)
7877ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (0 < -𝐷 → (√‘-𝐷) ≠ 0))
7966, 78sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐷 < 0 → (√‘-𝐷) ≠ 0))
8045, 79sylbird 259 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (¬ 0 ≤ 𝐷 → (√‘-𝐷) ≠ 0))
8180imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘-𝐷) ≠ 0)
8261, 65, 81recnmulnred 45049 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ((√‘-𝐷) · i) ∉ ℝ)
83 df-nel 3048 . . . . . . . . . . . . . . . . . . . . 21 (((√‘-𝐷) · i) ∉ ℝ ↔ ¬ ((√‘-𝐷) · i) ∈ ℝ)
8482, 83sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ ((√‘-𝐷) · i) ∈ ℝ)
8560, 84eqneltrd 2857 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (i · (√‘-𝐷)) ∈ ℝ)
8654, 85eqneltrd 2857 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (√‘𝐷) ∈ ℝ)
8737, 86eldifd 3908 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) ∈ (ℂ ∖ ℝ))
8836, 87readdcnnred 45047 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∉ ℝ)
89 df-nel 3048 . . . . . . . . . . . . . . . 16 ((-𝐵 + (√‘𝐷)) ∉ ℝ ↔ ¬ (-𝐵 + (√‘𝐷)) ∈ ℝ)
9088, 89sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (-𝐵 + (√‘𝐷)) ∈ ℝ)
9134, 90eldifd 3908 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∈ (ℂ ∖ ℝ))
92 2cnd 12124 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℂ)
93 2ne0 12150 . . . . . . . . . . . . . . . . 17 2 ≠ 0
9493a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 0)
9592, 2, 94, 4mulne0d 11700 . . . . . . . . . . . . . . 15 (𝜑 → (2 · 𝐴) ≠ 0)
9695adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0)
9722, 91, 96cndivrenred 45050 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ)
98 df-nel 3048 . . . . . . . . . . . . 13 (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ ↔ ¬ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
9997, 98sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
10099ex 413 . . . . . . . . . . 11 (𝜑 → (¬ 0 ≤ 𝐷 → ¬ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
101100con4d 115 . . . . . . . . . 10 (𝜑 → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
102101adantr 481 . . . . . . . . 9 ((𝜑𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
10318, 102sylbid 239 . . . . . . . 8 ((𝜑𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ → 0 ≤ 𝐷))
104103ex 413 . . . . . . 7 (𝜑 → (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ → 0 ≤ 𝐷)))
105 eleq1 2825 . . . . . . . . . 10 (𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ ↔ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
106105adantl 482 . . . . . . . . 9 ((𝜑𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ ↔ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
10723, 32subcld 11405 . . . . . . . . . . . . . . . 16 (𝜑 → (-𝐵 − (√‘𝐷)) ∈ ℂ)
108107adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (-𝐵 − (√‘𝐷)) ∈ ℂ)
10936, 87resubcnnred 45048 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (-𝐵 − (√‘𝐷)) ∉ ℝ)
110 df-nel 3048 . . . . . . . . . . . . . . . 16 ((-𝐵 − (√‘𝐷)) ∉ ℝ ↔ ¬ (-𝐵 − (√‘𝐷)) ∈ ℝ)
111109, 110sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (-𝐵 − (√‘𝐷)) ∈ ℝ)
112108, 111eldifd 3908 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (-𝐵 − (√‘𝐷)) ∈ (ℂ ∖ ℝ))
11322, 112, 96cndivrenred 45050 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ)
114 df-nel 3048 . . . . . . . . . . . . 13 (((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ ↔ ¬ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
115113, 114sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
116115ex 413 . . . . . . . . . . 11 (𝜑 → (¬ 0 ≤ 𝐷 → ¬ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
117116con4d 115 . . . . . . . . . 10 (𝜑 → (((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
118117adantr 481 . . . . . . . . 9 ((𝜑𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
119106, 118sylbid 239 . . . . . . . 8 ((𝜑𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ → 0 ≤ 𝐷))
120119ex 413 . . . . . . 7 (𝜑 → (𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ → 0 ≤ 𝐷)))
121104, 120jaod 856 . . . . . 6 (𝜑 → ((𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ → 0 ≤ 𝐷)))
122121com23 86 . . . . 5 (𝜑 → (𝑥 ∈ ℝ → ((𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) → 0 ≤ 𝐷)))
123122imp 407 . . . 4 ((𝜑𝑥 ∈ ℝ) → ((𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) → 0 ≤ 𝐷))
12416, 123sylbid 239 . . 3 ((𝜑𝑥 ∈ ℝ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → 0 ≤ 𝐷))
125124rexlimdva 3149 . 2 (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → 0 ≤ 𝐷))
12635adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → -𝐵 ∈ ℝ)
12730adantr 481 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐷 ∈ ℝ)
128 simpr 485 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → 0 ≤ 𝐷)
129127, 128resqrtcld 15201 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℝ)
130126, 129readdcld 11077 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∈ ℝ)
13119a1i 11 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 2 ∈ ℝ)
1321adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ∈ ℝ)
133131, 132remulcld 11078 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ)
13495adantr 481 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0)
135130, 133, 134redivcld 11876 . . . 4 ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
136 oveq1 7322 . . . . . . . 8 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝑥↑2) = (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2))
137136oveq2d 7331 . . . . . . 7 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝐴 · (𝑥↑2)) = (𝐴 · (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)))
138 oveq2 7323 . . . . . . . 8 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝐵 · 𝑥) = (𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))))
139138oveq1d 7330 . . . . . . 7 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → ((𝐵 · 𝑥) + 𝐶) = ((𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶))
140137, 139oveq12d 7333 . . . . . 6 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = ((𝐴 · (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)))
141140eqeq1d 2739 . . . . 5 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ((𝐴 · (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0))
142141adantl 482 . . . 4 (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ((𝐴 · (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0))
143 eqidd 2738 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)))
144143orcd 870 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))
1452adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ∈ ℂ)
1464adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ≠ 0)
1477adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐵 ∈ ℂ)
14810adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐶 ∈ ℂ)
14992, 2mulcld 11068 . . . . . . . 8 (𝜑 → (2 · 𝐴) ∈ ℂ)
15033, 149, 95divcld 11824 . . . . . . 7 (𝜑 → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℂ)
151150adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℂ)
15214adantr 481 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
153145, 146, 147, 148, 151, 152quad 26062 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (((𝐴 · (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0 ↔ (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
154144, 153mpbird 256 . . . 4 ((𝜑 ∧ 0 ≤ 𝐷) → ((𝐴 · (((-𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · ((-𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0)
155135, 142, 154rspcedvd 3572 . . 3 ((𝜑 ∧ 0 ≤ 𝐷) → ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)
156155ex 413 . 2 (𝜑 → (0 ≤ 𝐷 → ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))
157125, 156impbid 211 1 (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1540  wcel 2105  wne 2941  wnel 3047  wrex 3071  cdif 3894   class class class wbr 5087  cfv 6465  (class class class)co 7315  cc 10942  cr 10943  0cc0 10944  ici 10946   + caddc 10947   · cmul 10949   < clt 11082  cle 11083  cmin 11278  -cneg 11279   / cdiv 11705  2c2 12101  4c4 12103  cexp 13855  csqrt 15016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-sup 9271  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-n0 12307  df-z 12393  df-uz 12656  df-rp 12804  df-seq 13795  df-exp 13856  df-cj 14882  df-re 14883  df-im 14884  df-sqrt 15018  df-abs 15019
This theorem is referenced by:  requad1  45326  requad2  45327
  Copyright terms: Public domain W3C validator