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

Theorem requad2 44748
Description: A condition for a quadratic equation with real coefficients to have (exactly) two different real solutions. (Contributed by AV, 28-Jan-2023.)
Hypotheses
Ref Expression
requad2.a (𝜑𝐴 ∈ ℝ)
requad2.z (𝜑𝐴 ≠ 0)
requad2.b (𝜑𝐵 ∈ ℝ)
requad2.c (𝜑𝐶 ∈ ℝ)
requad2.d (𝜑𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
Assertion
Ref Expression
requad2 (𝜑 → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷   𝜑,𝑥   𝐴,𝑝   𝐵,𝑝   𝐶,𝑝   𝐷,𝑝   𝜑,𝑝,𝑥

Proof of Theorem requad2
Dummy variables 𝑎 𝑏 𝑦 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 requad2.a . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
21recnd 10861 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
32ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝐴 ∈ ℂ)
4 requad2.z . . . . . . . . 9 (𝜑𝐴 ≠ 0)
54ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝐴 ≠ 0)
6 requad2.b . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
76recnd 10861 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
87ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝐵 ∈ ℂ)
9 requad2.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
109recnd 10861 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1110ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝐶 ∈ ℂ)
12 elelpwi 4525 . . . . . . . . . . . 12 ((𝑥𝑝𝑝 ∈ 𝒫 ℝ) → 𝑥 ∈ ℝ)
1312expcom 417 . . . . . . . . . . 11 (𝑝 ∈ 𝒫 ℝ → (𝑥𝑝𝑥 ∈ ℝ))
1413adantl 485 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) → (𝑥𝑝𝑥 ∈ ℝ))
1514imp 410 . . . . . . . . 9 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝑥 ∈ ℝ)
1615recnd 10861 . . . . . . . 8 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝑥 ∈ ℂ)
17 requad2.d . . . . . . . . 9 (𝜑𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
1817ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
193, 5, 8, 11, 16, 18quad 25723 . . . . . . 7 ((((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) ∧ 𝑥𝑝) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
2019ralbidva 3117 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
2120anbi2d 632 . . . . 5 (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑝 ∈ 𝒫 ℝ) → (((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))))
2221reubidva 3300 . . . 4 ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))))
23 eqid 2737 . . . . . . . 8 {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2} = {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2}
2423pairreueq 44635 . . . . . . 7 (∃!𝑝 ∈ {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2}∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
2524bicomi 227 . . . . . 6 (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) ↔ ∃!𝑝 ∈ {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2}∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))
2625a1i 11 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) ↔ ∃!𝑝 ∈ {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2}∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
276renegcld 11259 . . . . . . . . 9 (𝜑 → -𝐵 ∈ ℝ)
2827adantr 484 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → -𝐵 ∈ ℝ)
296resqcld 13817 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℝ)
30 4re 11914 . . . . . . . . . . . . . 14 4 ∈ ℝ
3130a1i 11 . . . . . . . . . . . . 13 (𝜑 → 4 ∈ ℝ)
321, 9remulcld 10863 . . . . . . . . . . . . 13 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
3331, 32remulcld 10863 . . . . . . . . . . . 12 (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℝ)
3429, 33resubcld 11260 . . . . . . . . . . 11 (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℝ)
3517, 34eqeltrd 2838 . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ)
3635adantr 484 . . . . . . . . 9 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐷 ∈ ℝ)
37 simpr 488 . . . . . . . . 9 ((𝜑 ∧ 0 ≤ 𝐷) → 0 ≤ 𝐷)
3836, 37resqrtcld 14981 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℝ)
3928, 38readdcld 10862 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∈ ℝ)
40 2re 11904 . . . . . . . . . 10 2 ∈ ℝ
4140a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℝ)
4241, 1remulcld 10863 . . . . . . . 8 (𝜑 → (2 · 𝐴) ∈ ℝ)
4342adantr 484 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ)
44 2cnne0 12040 . . . . . . . . . 10 (2 ∈ ℂ ∧ 2 ≠ 0)
4544a1i 11 . . . . . . . . 9 (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
46 mulne0 11474 . . . . . . . . 9 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (2 · 𝐴) ≠ 0)
4745, 2, 4, 46syl12anc 837 . . . . . . . 8 (𝜑 → (2 · 𝐴) ≠ 0)
4847adantr 484 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0)
4939, 43, 48redivcld 11660 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
506adantr 484 . . . . . . . . 9 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐵 ∈ ℝ)
5150renegcld 11259 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → -𝐵 ∈ ℝ)
5251, 38resubcld 11260 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 − (√‘𝐷)) ∈ ℝ)
5340a1i 11 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → 2 ∈ ℝ)
541adantr 484 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ∈ ℝ)
5553, 54remulcld 10863 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ)
5652, 55, 48redivcld 11660 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
57 fveqeq2 6726 . . . . . . 7 (𝑞 = 𝑥 → ((♯‘𝑞) = 2 ↔ (♯‘𝑥) = 2))
5857cbvrabv 3402 . . . . . 6 {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2} = {𝑥 ∈ 𝒫 ℝ ∣ (♯‘𝑥) = 2}
5949, 56, 58paireqne 44636 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑝 ∈ {𝑞 ∈ 𝒫 ℝ ∣ (♯‘𝑞) = 2}∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ≠ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))
607negcld 11176 . . . . . . . . . . 11 (𝜑 → -𝐵 ∈ ℂ)
6135recnd 10861 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
6261sqrtcld 15001 . . . . . . . . . . 11 (𝜑 → (√‘𝐷) ∈ ℂ)
6360, 62addcld 10852 . . . . . . . . . 10 (𝜑 → (-𝐵 + (√‘𝐷)) ∈ ℂ)
6460, 62subcld 11189 . . . . . . . . . 10 (𝜑 → (-𝐵 − (√‘𝐷)) ∈ ℂ)
65 2cnd 11908 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
6665, 2mulcld 10853 . . . . . . . . . 10 (𝜑 → (2 · 𝐴) ∈ ℂ)
67 div11 11518 . . . . . . . . . 10 (((-𝐵 + (√‘𝐷)) ∈ ℂ ∧ (-𝐵 − (√‘𝐷)) ∈ ℂ ∧ ((2 · 𝐴) ∈ ℂ ∧ (2 · 𝐴) ≠ 0)) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ (-𝐵 + (√‘𝐷)) = (-𝐵 − (√‘𝐷))))
6863, 64, 66, 47, 67syl112anc 1376 . . . . . . . . 9 (𝜑 → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ (-𝐵 + (√‘𝐷)) = (-𝐵 − (√‘𝐷))))
6960, 62negsubd 11195 . . . . . . . . . . 11 (𝜑 → (-𝐵 + -(√‘𝐷)) = (-𝐵 − (√‘𝐷)))
7069eqcomd 2743 . . . . . . . . . 10 (𝜑 → (-𝐵 − (√‘𝐷)) = (-𝐵 + -(√‘𝐷)))
7170eqeq2d 2748 . . . . . . . . 9 (𝜑 → ((-𝐵 + (√‘𝐷)) = (-𝐵 − (√‘𝐷)) ↔ (-𝐵 + (√‘𝐷)) = (-𝐵 + -(√‘𝐷))))
7262negcld 11176 . . . . . . . . . 10 (𝜑 → -(√‘𝐷) ∈ ℂ)
7360, 62, 72addcand 11035 . . . . . . . . 9 (𝜑 → ((-𝐵 + (√‘𝐷)) = (-𝐵 + -(√‘𝐷)) ↔ (√‘𝐷) = -(√‘𝐷)))
7468, 71, 733bitrd 308 . . . . . . . 8 (𝜑 → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ (√‘𝐷) = -(√‘𝐷)))
7574necon3bid 2985 . . . . . . 7 (𝜑 → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ≠ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ (√‘𝐷) ≠ -(√‘𝐷)))
7675adantr 484 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ≠ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ (√‘𝐷) ≠ -(√‘𝐷)))
77 cnsqrt00 14956 . . . . . . . . . 10 (𝐷 ∈ ℂ → ((√‘𝐷) = 0 ↔ 𝐷 = 0))
7861, 77syl 17 . . . . . . . . 9 (𝜑 → ((√‘𝐷) = 0 ↔ 𝐷 = 0))
7978necon3bid 2985 . . . . . . . 8 (𝜑 → ((√‘𝐷) ≠ 0 ↔ 𝐷 ≠ 0))
8079adantr 484 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) ≠ 0 ↔ 𝐷 ≠ 0))
8162eqnegd 11553 . . . . . . . . 9 (𝜑 → ((√‘𝐷) = -(√‘𝐷) ↔ (√‘𝐷) = 0))
8281adantr 484 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = -(√‘𝐷) ↔ (√‘𝐷) = 0))
8382necon3bid 2985 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) ≠ -(√‘𝐷) ↔ (√‘𝐷) ≠ 0))
84 0red 10836 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝐷) → 0 ∈ ℝ)
8584, 36, 37leltned 10985 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝐷) → (0 < 𝐷𝐷 ≠ 0))
8680, 83, 853bitr4d 314 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) ≠ -(√‘𝐷) ↔ 0 < 𝐷))
8776, 86bitrd 282 . . . . 5 ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ≠ ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ 0 < 𝐷))
8826, 59, 873bitrd 308 . . . 4 ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) ↔ 0 < 𝐷))
8922, 88bitrd 282 . . 3 ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷))
9089expcom 417 . 2 (0 ≤ 𝐷 → (𝜑 → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷)))
91 hash2prb 14038 . . . . . . . . . . . . 13 (𝑝 ∈ 𝒫 ℝ → ((♯‘𝑝) = 2 ↔ ∃𝑎𝑝𝑏𝑝 (𝑎𝑏𝑝 = {𝑎, 𝑏})))
9291adantl 485 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ 𝒫 ℝ) → ((♯‘𝑝) = 2 ↔ ∃𝑎𝑝𝑏𝑝 (𝑎𝑏𝑝 = {𝑎, 𝑏})))
93 raleq 3319 . . . . . . . . . . . . . . . . . 18 (𝑝 = {𝑎, 𝑏} → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ∀𝑥 ∈ {𝑎, 𝑏} ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))
94 vex 3412 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ V
95 vex 3412 . . . . . . . . . . . . . . . . . . 19 𝑏 ∈ V
96 oveq1 7220 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → (𝑥↑2) = (𝑎↑2))
9796oveq2d 7229 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → (𝐴 · (𝑥↑2)) = (𝐴 · (𝑎↑2)))
98 oveq2 7221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → (𝐵 · 𝑥) = (𝐵 · 𝑎))
9998oveq1d 7228 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → ((𝐵 · 𝑥) + 𝐶) = ((𝐵 · 𝑎) + 𝐶))
10097, 99oveq12d 7231 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = ((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)))
101100eqeq1d 2739 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)) = 0))
102 oveq1 7220 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝑥↑2) = (𝑏↑2))
103102oveq2d 7229 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝐴 · (𝑥↑2)) = (𝐴 · (𝑏↑2)))
104 oveq2 7221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝐵 · 𝑥) = (𝐵 · 𝑏))
105104oveq1d 7228 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → ((𝐵 · 𝑥) + 𝐶) = ((𝐵 · 𝑏) + 𝐶))
106103, 105oveq12d 7231 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑏 → ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)))
107106eqeq1d 2739 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑏 → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0))
10894, 95, 101, 107ralpr 4616 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ {𝑎, 𝑏} ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)) = 0 ∧ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0))
10993, 108bitrdi 290 . . . . . . . . . . . . . . . . 17 (𝑝 = {𝑎, 𝑏} → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)) = 0 ∧ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0)))
110109adantl 485 . . . . . . . . . . . . . . . 16 ((𝑎𝑏𝑝 = {𝑎, 𝑏}) → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)) = 0 ∧ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0)))
111110adantl 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) ∧ (𝑎𝑏𝑝 = {𝑎, 𝑏})) → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)) = 0 ∧ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0)))
112 elelpwi 4525 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑝𝑝 ∈ 𝒫 ℝ) → 𝑏 ∈ ℝ)
113112ex 416 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑝 → (𝑝 ∈ 𝒫 ℝ → 𝑏 ∈ ℝ))
114113adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑝𝑏𝑝) → (𝑝 ∈ 𝒫 ℝ → 𝑏 ∈ ℝ))
115114com12 32 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ 𝒫 ℝ → ((𝑎𝑝𝑏𝑝) → 𝑏 ∈ ℝ))
116115adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ 𝒫 ℝ) → ((𝑎𝑝𝑏𝑝) → 𝑏 ∈ ℝ))
117116imp 410 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) → 𝑏 ∈ ℝ)
118 oveq1 7220 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑏 → (𝑦↑2) = (𝑏↑2))
119118oveq2d 7229 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝐴 · (𝑦↑2)) = (𝐴 · (𝑏↑2)))
120 oveq2 7221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑏 → (𝐵 · 𝑦) = (𝐵 · 𝑏))
121120oveq1d 7228 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → ((𝐵 · 𝑦) + 𝐶) = ((𝐵 · 𝑏) + 𝐶))
122119, 121oveq12d 7231 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)))
123122eqeq1d 2739 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → (((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0 ↔ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0))
124123adantl 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) ∧ 𝑦 = 𝑏) → (((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0 ↔ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0))
125117, 124rspcedv 3530 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) → (((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0 → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0))
126125adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) ∧ (𝑎𝑏𝑝 = {𝑎, 𝑏})) → (((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0 → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0))
127126adantld 494 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) ∧ (𝑎𝑏𝑝 = {𝑎, 𝑏})) → ((((𝐴 · (𝑎↑2)) + ((𝐵 · 𝑎) + 𝐶)) = 0 ∧ ((𝐴 · (𝑏↑2)) + ((𝐵 · 𝑏) + 𝐶)) = 0) → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0))
128111, 127sylbid 243 . . . . . . . . . . . . . 14 ((((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) ∧ (𝑎𝑏𝑝 = {𝑎, 𝑏})) → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0))
129128ex 416 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ 𝒫 ℝ) ∧ (𝑎𝑝𝑏𝑝)) → ((𝑎𝑏𝑝 = {𝑎, 𝑏}) → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0)))
130129rexlimdvva 3213 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ 𝒫 ℝ) → (∃𝑎𝑝𝑏𝑝 (𝑎𝑏𝑝 = {𝑎, 𝑏}) → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0)))
13192, 130sylbid 243 . . . . . . . . . . 11 ((𝜑𝑝 ∈ 𝒫 ℝ) → ((♯‘𝑝) = 2 → (∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0)))
132131impd 414 . . . . . . . . . 10 ((𝜑𝑝 ∈ 𝒫 ℝ) → (((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0))
133132rexlimdva 3203 . . . . . . . . 9 (𝜑 → (∃𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) → ∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0))
1341, 4, 6, 9, 17requad01 44746 . . . . . . . . 9 (𝜑 → (∃𝑦 ∈ ℝ ((𝐴 · (𝑦↑2)) + ((𝐵 · 𝑦) + 𝐶)) = 0 ↔ 0 ≤ 𝐷))
135133, 134sylibd 242 . . . . . . . 8 (𝜑 → (∃𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) → 0 ≤ 𝐷))
136135con3d 155 . . . . . . 7 (𝜑 → (¬ 0 ≤ 𝐷 → ¬ ∃𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)))
137136impcom 411 . . . . . 6 ((¬ 0 ≤ 𝐷𝜑) → ¬ ∃𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))
138 reurex 3338 . . . . . 6 (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) → ∃𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))
139137, 138nsyl 142 . . . . 5 ((¬ 0 ≤ 𝐷𝜑) → ¬ ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))
140139pm2.21d 121 . . . 4 ((¬ 0 ≤ 𝐷𝜑) → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) → 0 < 𝐷))
141 0red 10836 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
142 ltle 10921 . . . . . . . 8 ((0 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (0 < 𝐷 → 0 ≤ 𝐷))
143141, 35, 142syl2anc 587 . . . . . . 7 (𝜑 → (0 < 𝐷 → 0 ≤ 𝐷))
144 pm2.24 124 . . . . . . 7 (0 ≤ 𝐷 → (¬ 0 ≤ 𝐷 → ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)))
145143, 144syl6 35 . . . . . 6 (𝜑 → (0 < 𝐷 → (¬ 0 ≤ 𝐷 → ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))))
146145com23 86 . . . . 5 (𝜑 → (¬ 0 ≤ 𝐷 → (0 < 𝐷 → ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))))
147146impcom 411 . . . 4 ((¬ 0 ≤ 𝐷𝜑) → (0 < 𝐷 → ∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)))
148140, 147impbid 215 . . 3 ((¬ 0 ≤ 𝐷𝜑) → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷))
149148ex 416 . 2 (¬ 0 ≤ 𝐷 → (𝜑 → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷)))
15090, 149pm2.61i 185 1 (𝜑 → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  ∃!wreu 3063  {crab 3065  𝒫 cpw 4513  {cpr 4543   class class class wbr 5053  cfv 6380  (class class class)co 7213  cc 10727  cr 10728  0cc0 10729   + caddc 10732   · cmul 10734   < clt 10867  cle 10868  cmin 11062  -cneg 11063   / cdiv 11489  2c2 11885  4c4 11887  cexp 13635  chash 13896  csqrt 14796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-oadd 8206  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-dju 9517  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-n0 12091  df-z 12177  df-uz 12439  df-rp 12587  df-fz 13096  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799
This theorem is referenced by:  itscnhlinecirc02p  45804
  Copyright terms: Public domain W3C validator