Proof of Theorem discr1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥↑2) = (𝑋↑2)) | 
| 2 | 1 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐴 · (𝑥↑2)) = (𝐴 · (𝑋↑2))) | 
| 3 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐵 · 𝑥) = (𝐵 · 𝑋)) | 
| 4 | 2, 3 | oveq12d 7449 | . . . . . 6
⊢ (𝑥 = 𝑋 → ((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋))) | 
| 5 | 4 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 𝑋 → (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶)) | 
| 6 | 5 | breq2d 5155 | . . . 4
⊢ (𝑥 = 𝑋 → (0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) ↔ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) | 
| 7 |  | discr.4 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) | 
| 8 | 7 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) | 
| 10 |  | discr1.5 | . . . . 5
⊢ 𝑋 = if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) | 
| 11 |  | discr.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 12 | 11 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐵 ∈ ℝ) | 
| 13 |  | discr.3 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 14 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐶 ∈ ℝ) | 
| 15 |  | 0re 11263 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 16 |  | ifcl 4571 | . . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) | 
| 17 | 14, 15, 16 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) | 
| 18 | 12, 17 | readdcld 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ) | 
| 19 |  | peano2re 11434 | . . . . . . . 8
⊢ ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ → ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ∈ ℝ) | 
| 20 | 18, 19 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ∈ ℝ) | 
| 21 |  | discr.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐴 ∈ ℝ) | 
| 23 | 22 | renegcld 11690 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → -𝐴 ∈ ℝ) | 
| 24 | 21 | lt0neg1d 11832 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 < 0 ↔ 0 < -𝐴)) | 
| 25 | 24 | biimpa 476 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < -𝐴) | 
| 26 | 25 | gt0ne0d 11827 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → -𝐴 ≠ 0) | 
| 27 | 20, 23, 26 | redivcld 12095 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ) | 
| 28 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 29 |  | ifcl 4571 | . . . . . 6
⊢
(((((𝐵 + if(0 ≤
𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ if(1 ≤ (((𝐵 +
if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ∈ ℝ) | 
| 30 | 27, 28, 29 | sylancl 586 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ∈ ℝ) | 
| 31 | 10, 30 | eqeltrid 2845 | . . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝑋 ∈ ℝ) | 
| 32 | 6, 9, 31 | rspcdva 3623 | . . 3
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶)) | 
| 33 |  | resqcl 14164 | . . . . . . . . 9
⊢ (𝑋 ∈ ℝ → (𝑋↑2) ∈
ℝ) | 
| 34 | 31, 33 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝑋↑2) ∈ ℝ) | 
| 35 | 22, 34 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · (𝑋↑2)) ∈ ℝ) | 
| 36 | 12, 31 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 · 𝑋) ∈ ℝ) | 
| 37 | 35, 36 | readdcld 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℝ) | 
| 38 | 37, 14 | readdcld 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ∈ ℝ) | 
| 39 | 22, 31 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · 𝑋) ∈ ℝ) | 
| 40 | 39, 18 | readdcld 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) ∈ ℝ) | 
| 41 | 40, 31 | remulcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) ∈ ℝ) | 
| 42 | 15 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 ∈
ℝ) | 
| 43 | 17, 31 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋) ∈ ℝ) | 
| 44 |  | max2 13229 | . . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 𝐶
≤ if(0 ≤ 𝐶, 𝐶, 0)) | 
| 45 | 15, 14, 44 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0)) | 
| 46 |  | max1 13227 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) | 
| 47 | 15, 14, 46 | sylancr 587 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) | 
| 48 |  | max1 13227 | . . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (((𝐵 +
if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ) → 1 ≤ if(1 ≤
(((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) | 
| 49 | 28, 27, 48 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → 1 ≤ if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) | 
| 50 | 49, 10 | breqtrrdi 5185 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 1 ≤ 𝑋) | 
| 51 | 17, 31, 47, 50 | lemulge11d 12205 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → if(0 ≤ 𝐶, 𝐶, 0) ≤ (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋)) | 
| 52 | 14, 17, 43, 45, 51 | letrd 11418 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐶 ≤ (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋)) | 
| 53 | 14, 43, 37, 52 | leadd2dd 11878 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) | 
| 54 | 39, 12 | readdcld 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + 𝐵) ∈ ℝ) | 
| 55 | 54 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + 𝐵) ∈ ℂ) | 
| 56 | 17 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ) | 
| 57 | 31 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝑋 ∈ ℂ) | 
| 58 | 55, 56, 57 | adddird 11286 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · 𝑋) + 𝐵) + if(0 ≤ 𝐶, 𝐶, 0)) · 𝑋) = ((((𝐴 · 𝑋) + 𝐵) · 𝑋) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) | 
| 59 | 39 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · 𝑋) ∈ ℂ) | 
| 60 | 12 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐵 ∈ ℂ) | 
| 61 | 59, 60, 56 | addassd 11283 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + 𝐵) + if(0 ≤ 𝐶, 𝐶, 0)) = ((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)))) | 
| 62 | 61 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · 𝑋) + 𝐵) + if(0 ≤ 𝐶, 𝐶, 0)) · 𝑋) = (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋)) | 
| 63 | 22 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐴 ∈ ℂ) | 
| 64 | 63, 57, 57 | mulassd 11284 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) · 𝑋) = (𝐴 · (𝑋 · 𝑋))) | 
| 65 |  | sqval 14155 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋↑2) = (𝑋 · 𝑋)) | 
| 66 | 57, 65 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝑋↑2) = (𝑋 · 𝑋)) | 
| 67 | 66 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · (𝑋↑2)) = (𝐴 · (𝑋 · 𝑋))) | 
| 68 | 64, 67 | eqtr4d 2780 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) · 𝑋) = (𝐴 · (𝑋↑2))) | 
| 69 | 68 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) · 𝑋) + (𝐵 · 𝑋)) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋))) | 
| 70 | 59, 57, 60, 69 | joinlmuladdmuld 11288 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + 𝐵) · 𝑋) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋))) | 
| 71 | 70 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · 𝑋) + 𝐵) · 𝑋) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) | 
| 72 | 58, 62, 71 | 3eqtr3d 2785 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) | 
| 73 | 53, 72 | breqtrrd 5171 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ≤ (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋)) | 
| 74 | 23, 31 | remulcld 11291 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → (-𝐴 · 𝑋) ∈ ℝ) | 
| 75 | 18 | ltp1d 12198 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1)) | 
| 76 |  | max2 13229 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ (((𝐵 +
if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) | 
| 77 | 28, 27, 76 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) | 
| 78 | 77, 10 | breqtrrdi 5185 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ 𝑋) | 
| 79 |  | ledivmul 12144 | . . . . . . . . . . . 12
⊢ ((((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ (-𝐴 ∈ ℝ ∧ 0 <
-𝐴)) → ((((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ 𝑋 ↔ ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ≤ (-𝐴 · 𝑋))) | 
| 80 | 20, 31, 23, 25, 79 | syl112anc 1376 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ 𝑋 ↔ ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ≤ (-𝐴 · 𝑋))) | 
| 81 | 78, 80 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ≤ (-𝐴 · 𝑋)) | 
| 82 | 18, 20, 74, 75, 81 | ltletrd 11421 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < (-𝐴 · 𝑋)) | 
| 83 | 63, 57 | mulneg1d 11716 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → (-𝐴 · 𝑋) = -(𝐴 · 𝑋)) | 
| 84 |  | df-neg 11495 | . . . . . . . . . 10
⊢ -(𝐴 · 𝑋) = (0 − (𝐴 · 𝑋)) | 
| 85 | 83, 84 | eqtrdi 2793 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (-𝐴 · 𝑋) = (0 − (𝐴 · 𝑋))) | 
| 86 | 82, 85 | breqtrd 5169 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < (0 − (𝐴 · 𝑋))) | 
| 87 | 39, 18, 42 | ltaddsub2d 11864 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0 ↔ (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < (0 − (𝐴 · 𝑋)))) | 
| 88 | 86, 87 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0) | 
| 89 | 28 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 1 ∈
ℝ) | 
| 90 |  | 0lt1 11785 | . . . . . . . . . 10
⊢ 0 <
1 | 
| 91 | 90 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 1) | 
| 92 | 42, 89, 31, 91, 50 | ltletrd 11421 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 𝑋) | 
| 93 |  | ltmul1 12117 | . . . . . . . 8
⊢ ((((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) ∈ ℝ ∧ 0 ∈ ℝ
∧ (𝑋 ∈ ℝ
∧ 0 < 𝑋)) →
(((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0 ↔ (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < (0 · 𝑋))) | 
| 94 | 40, 42, 31, 92, 93 | syl112anc 1376 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0 ↔ (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < (0 · 𝑋))) | 
| 95 | 88, 94 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < (0 · 𝑋)) | 
| 96 | 57 | mul02d 11459 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (0 · 𝑋) = 0) | 
| 97 | 95, 96 | breqtrd 5169 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < 0) | 
| 98 | 38, 41, 42, 73, 97 | lelttrd 11419 | . . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) < 0) | 
| 99 |  | ltnle 11340 | . . . . 5
⊢
(((((𝐴 ·
(𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((((𝐴 ·
(𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) < 0 ↔ ¬ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) | 
| 100 | 38, 15, 99 | sylancl 586 | . . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) < 0 ↔ ¬ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) | 
| 101 | 98, 100 | mpbid 232 | . . 3
⊢ ((𝜑 ∧ 𝐴 < 0) → ¬ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶)) | 
| 102 | 32, 101 | pm2.65da 817 | . 2
⊢ (𝜑 → ¬ 𝐴 < 0) | 
| 103 |  | lelttric 11368 | . . . 4
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ∨ 𝐴 < 0)) | 
| 104 | 15, 21, 103 | sylancr 587 | . . 3
⊢ (𝜑 → (0 ≤ 𝐴 ∨ 𝐴 < 0)) | 
| 105 | 104 | ord 865 | . 2
⊢ (𝜑 → (¬ 0 ≤ 𝐴 → 𝐴 < 0)) | 
| 106 | 102, 105 | mt3d 148 | 1
⊢ (𝜑 → 0 ≤ 𝐴) |