Proof of Theorem requad1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | requad2.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 | 1 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 3 | 2 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ) | 
| 4 |  | requad2.z | . . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 0) | 
| 5 | 4 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐴 ≠ 0) | 
| 6 |  | requad2.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 7 | 6 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 8 | 7 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ) | 
| 9 |  | requad2.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 10 | 9 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 11 | 10 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐶 ∈ ℂ) | 
| 12 |  | recn 11245 | . . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) | 
| 13 | 12 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) | 
| 14 |  | requad2.d | . . . . . . 7
⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) | 
| 15 | 14 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) | 
| 16 | 3, 5, 8, 11, 13, 15 | quad 26883 | . . . . 5
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) | 
| 17 | 16 | reubidva 3396 | . . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ∃!𝑥 ∈ ℝ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) | 
| 18 | 6 | renegcld 11690 | . . . . . . . 8
⊢ (𝜑 → -𝐵 ∈ ℝ) | 
| 19 | 18 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → -𝐵 ∈ ℝ) | 
| 20 | 6 | resqcld 14165 | . . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℝ) | 
| 21 |  | 4re 12350 | . . . . . . . . . . . 12
⊢ 4 ∈
ℝ | 
| 22 | 21 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 4 ∈
ℝ) | 
| 23 | 1, 9 | remulcld 11291 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℝ) | 
| 24 | 22, 23 | remulcld 11291 | . . . . . . . . . 10
⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℝ) | 
| 25 | 20, 24 | resubcld 11691 | . . . . . . . . 9
⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℝ) | 
| 26 | 14, 25 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 27 |  | resqrtcl 15292 | . . . . . . . 8
⊢ ((𝐷 ∈ ℝ ∧ 0 ≤
𝐷) →
(√‘𝐷) ∈
ℝ) | 
| 28 | 26, 27 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℝ) | 
| 29 | 19, 28 | readdcld 11290 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∈ ℝ) | 
| 30 |  | 2re 12340 | . . . . . . . . 9
⊢ 2 ∈
ℝ | 
| 31 | 30 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) | 
| 32 | 31, 1 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → (2 · 𝐴) ∈
ℝ) | 
| 33 | 32 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ) | 
| 34 |  | 2cnd 12344 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) | 
| 35 |  | 2ne0 12370 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 36 | 35 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ≠ 0) | 
| 37 | 34, 2, 36, 4 | mulne0d 11915 | . . . . . . 7
⊢ (𝜑 → (2 · 𝐴) ≠ 0) | 
| 38 | 37 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0) | 
| 39 | 29, 33, 38 | redivcld 12095 | . . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ) | 
| 40 | 19, 28 | resubcld 11691 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 − (√‘𝐷)) ∈ ℝ) | 
| 41 | 40, 33, 38 | redivcld 12095 | . . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ) | 
| 42 |  | euoreqb 47121 | . . . . 5
⊢
((((-𝐵 +
(√‘𝐷)) / (2
· 𝐴)) ∈ ℝ
∧ ((-𝐵 −
(√‘𝐷)) / (2
· 𝐴)) ∈
ℝ) → (∃!𝑥
∈ ℝ (𝑥 =
((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) | 
| 43 | 39, 41, 42 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑥 ∈ ℝ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) | 
| 44 | 7 | negcld 11607 | . . . . . . . 8
⊢ (𝜑 → -𝐵 ∈ ℂ) | 
| 45 | 26 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 46 | 45 | sqrtcld 15476 | . . . . . . . 8
⊢ (𝜑 → (√‘𝐷) ∈
ℂ) | 
| 47 | 32 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝐴) ∈
ℂ) | 
| 48 | 44, 46, 47, 37 | divdird 12081 | . . . . . . 7
⊢ (𝜑 → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴)))) | 
| 49 | 48 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴)))) | 
| 50 | 44, 46, 47, 37 | divsubdird 12082 | . . . . . . . 8
⊢ (𝜑 → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) | 
| 51 | 50 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) | 
| 52 | 44, 47, 37 | divcld 12043 | . . . . . . . . 9
⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ) | 
| 53 | 52 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 / (2 · 𝐴)) ∈ ℂ) | 
| 54 | 46, 47, 37 | divcld 12043 | . . . . . . . . 9
⊢ (𝜑 → ((√‘𝐷) / (2 · 𝐴)) ∈
ℂ) | 
| 55 | 54 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) / (2 · 𝐴)) ∈ ℂ) | 
| 56 | 53, 55 | negsubd 11626 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 / (2 · 𝐴)) + -((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) | 
| 57 | 46 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℂ) | 
| 58 | 47 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℂ) | 
| 59 | 57, 58, 38 | divnegd 12056 | . . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → -((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴))) | 
| 60 | 59 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 / (2 · 𝐴)) + -((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴)))) | 
| 61 | 51, 56, 60 | 3eqtr2d 2783 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴)))) | 
| 62 | 49, 61 | eqeq12d 2753 | . . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))))) | 
| 63 | 46 | negcld 11607 | . . . . . . . . 9
⊢ (𝜑 → -(√‘𝐷) ∈
ℂ) | 
| 64 | 63, 47, 37 | divcld 12043 | . . . . . . . 8
⊢ (𝜑 → (-(√‘𝐷) / (2 · 𝐴)) ∈
ℂ) | 
| 65 | 64 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-(√‘𝐷) / (2 · 𝐴)) ∈ ℂ) | 
| 66 | 53, 55, 65 | addcand 11464 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))) ↔ ((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)))) | 
| 67 |  | div11 11950 | . . . . . . . 8
⊢
(((√‘𝐷)
∈ ℂ ∧ -(√‘𝐷) ∈ ℂ ∧ ((2 · 𝐴) ∈ ℂ ∧ (2
· 𝐴) ≠ 0)) →
(((√‘𝐷) / (2
· 𝐴)) =
(-(√‘𝐷) / (2
· 𝐴)) ↔
(√‘𝐷) =
-(√‘𝐷))) | 
| 68 | 46, 63, 47, 37, 67 | syl112anc 1376 | . . . . . . 7
⊢ (𝜑 → (((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)) ↔ (√‘𝐷) = -(√‘𝐷))) | 
| 69 | 68 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)) ↔ (√‘𝐷) = -(√‘𝐷))) | 
| 70 | 57 | eqnegd 11988 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = -(√‘𝐷) ↔ (√‘𝐷) = 0)) | 
| 71 |  | sqrt00 15302 | . . . . . . . 8
⊢ ((𝐷 ∈ ℝ ∧ 0 ≤
𝐷) →
((√‘𝐷) = 0
↔ 𝐷 =
0)) | 
| 72 | 26, 71 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = 0 ↔ 𝐷 = 0)) | 
| 73 | 70, 72 | bitrd 279 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = -(√‘𝐷) ↔ 𝐷 = 0)) | 
| 74 | 66, 69, 73 | 3bitrd 305 | . . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))) ↔ 𝐷 = 0)) | 
| 75 | 62, 74 | bitrd 279 | . . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ 𝐷 = 0)) | 
| 76 | 17, 43, 75 | 3bitrd 305 | . . 3
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) | 
| 77 | 76 | expcom 413 | . 2
⊢ (0 ≤
𝐷 → (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0))) | 
| 78 | 1, 4, 6, 9, 14 | requad01 47608 | . . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷)) | 
| 79 | 78 | notbid 318 | . . . . . . 7
⊢ (𝜑 → (¬ ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ¬ 0 ≤ 𝐷)) | 
| 80 | 79 | biimparc 479 | . . . . . 6
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → ¬ ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) | 
| 81 |  | reurex 3384 | . . . . . 6
⊢
(∃!𝑥 ∈
ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) | 
| 82 | 80, 81 | nsyl 140 | . . . . 5
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → ¬ ∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) | 
| 83 | 82 | pm2.21d 121 | . . . 4
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → 𝐷 = 0)) | 
| 84 |  | 0red 11264 | . . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) | 
| 85 | 26, 84 | ltnled 11408 | . . . . . . 7
⊢ (𝜑 → (𝐷 < 0 ↔ ¬ 0 ≤ 𝐷)) | 
| 86 | 85 | biimparc 479 | . . . . . 6
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → 𝐷 < 0) | 
| 87 | 86 | lt0ne0d 11828 | . . . . 5
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → 𝐷 ≠ 0) | 
| 88 |  | eqneqall 2951 | . . . . 5
⊢ (𝐷 = 0 → (𝐷 ≠ 0 → ∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)) | 
| 89 | 87, 88 | syl5com 31 | . . . 4
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → (𝐷 = 0 → ∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)) | 
| 90 | 83, 89 | impbid 212 | . . 3
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) | 
| 91 | 90 | ex 412 | . 2
⊢ (¬ 0
≤ 𝐷 → (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0))) | 
| 92 | 77, 91 | pm2.61i 182 | 1
⊢ (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) |