Proof of Theorem discr1
Step | Hyp | Ref
| Expression |
1 | | discr1.5 |
. . . . 5
⊢ 𝑋 = if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) |
2 | | discr.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐵 ∈ ℝ) |
4 | | discr.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
5 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐶 ∈ ℝ) |
6 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
7 | | ifcl 4080 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
8 | 5, 6, 7 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
9 | 3, 8 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ) |
10 | | peano2re 10088 |
. . . . . . . 8
⊢ ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ → ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ∈ ℝ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ∈ ℝ) |
12 | | discr.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
13 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐴 ∈ ℝ) |
14 | 13 | renegcld 10336 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → -𝐴 ∈ ℝ) |
15 | 12 | lt0neg1d 10476 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 < 0 ↔ 0 < -𝐴)) |
16 | 15 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < -𝐴) |
17 | 16 | gt0ne0d 10471 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → -𝐴 ≠ 0) |
18 | 11, 14, 17 | redivcld 10732 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ) |
19 | | 1re 9918 |
. . . . . 6
⊢ 1 ∈
ℝ |
20 | | ifcl 4080 |
. . . . . 6
⊢
(((((𝐵 + if(0 ≤
𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ if(1 ≤ (((𝐵 +
if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ∈ ℝ) |
21 | 18, 19, 20 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ∈ ℝ) |
22 | 1, 21 | syl5eqel 2692 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝑋 ∈ ℝ) |
23 | | discr.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
24 | 23 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
25 | 24 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
26 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥↑2) = (𝑋↑2)) |
27 | 26 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐴 · (𝑥↑2)) = (𝐴 · (𝑋↑2))) |
28 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐵 · 𝑥) = (𝐵 · 𝑋)) |
29 | 27, 28 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋))) |
30 | 29 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶)) |
31 | 30 | breq2d 4595 |
. . . . 5
⊢ (𝑥 = 𝑋 → (0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) ↔ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) |
32 | 31 | rspcv 3278 |
. . . 4
⊢ (𝑋 ∈ ℝ →
(∀𝑥 ∈ ℝ 0
≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) → 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) |
33 | 22, 25, 32 | sylc 63 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶)) |
34 | | resqcl 12793 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ → (𝑋↑2) ∈
ℝ) |
35 | 22, 34 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝑋↑2) ∈ ℝ) |
36 | 13, 35 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · (𝑋↑2)) ∈ ℝ) |
37 | 3, 22 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 · 𝑋) ∈ ℝ) |
38 | 36, 37 | readdcld 9948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℝ) |
39 | 38, 5 | readdcld 9948 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ∈ ℝ) |
40 | 13, 22 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · 𝑋) ∈ ℝ) |
41 | 40, 9 | readdcld 9948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) ∈ ℝ) |
42 | 41, 22 | remulcld 9949 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) ∈ ℝ) |
43 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 ∈
ℝ) |
44 | 8, 22 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋) ∈ ℝ) |
45 | | max2 11892 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 𝐶
≤ if(0 ≤ 𝐶, 𝐶, 0)) |
46 | 6, 5, 45 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
47 | | max1 11890 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
48 | 6, 5, 47 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
49 | | max1 11890 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (((𝐵 +
if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ) → 1 ≤ if(1 ≤
(((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) |
50 | 19, 18, 49 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → 1 ≤ if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) |
51 | 50, 1 | syl6breqr 4625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 1 ≤ 𝑋) |
52 | 8, 22, 48, 51 | lemulge11d 10840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → if(0 ≤ 𝐶, 𝐶, 0) ≤ (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋)) |
53 | 5, 8, 44, 46, 52 | letrd 10073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐶 ≤ (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋)) |
54 | 5, 44, 38, 53 | leadd2dd 10521 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) |
55 | 40, 3 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + 𝐵) ∈ ℝ) |
56 | 55 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + 𝐵) ∈ ℂ) |
57 | 8 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ) |
58 | 22 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝑋 ∈ ℂ) |
59 | 56, 57, 58 | adddird 9944 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · 𝑋) + 𝐵) + if(0 ≤ 𝐶, 𝐶, 0)) · 𝑋) = ((((𝐴 · 𝑋) + 𝐵) · 𝑋) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) |
60 | 40 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · 𝑋) ∈ ℂ) |
61 | 3 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐵 ∈ ℂ) |
62 | 60, 61, 57 | addassd 9941 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + 𝐵) + if(0 ≤ 𝐶, 𝐶, 0)) = ((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)))) |
63 | 62 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · 𝑋) + 𝐵) + if(0 ≤ 𝐶, 𝐶, 0)) · 𝑋) = (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋)) |
64 | 60, 61, 58 | adddird 9944 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + 𝐵) · 𝑋) = (((𝐴 · 𝑋) · 𝑋) + (𝐵 · 𝑋))) |
65 | 13 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝐴 ∈ ℂ) |
66 | 65, 58, 58 | mulassd 9942 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) · 𝑋) = (𝐴 · (𝑋 · 𝑋))) |
67 | | sqval 12784 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋↑2) = (𝑋 · 𝑋)) |
68 | 58, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝑋↑2) = (𝑋 · 𝑋)) |
69 | 68 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐴 · (𝑋↑2)) = (𝐴 · (𝑋 · 𝑋))) |
70 | 66, 69 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) · 𝑋) = (𝐴 · (𝑋↑2))) |
71 | 70 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) · 𝑋) + (𝐵 · 𝑋)) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋))) |
72 | 64, 71 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + 𝐵) · 𝑋) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋))) |
73 | 72 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · 𝑋) + 𝐵) · 𝑋) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) |
74 | 59, 63, 73 | 3eqtr3d 2652 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + (if(0 ≤ 𝐶, 𝐶, 0) · 𝑋))) |
75 | 54, 74 | breqtrrd 4611 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ≤ (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋)) |
76 | 14, 22 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → (-𝐴 · 𝑋) ∈ ℝ) |
77 | 9 | ltp1d 10833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1)) |
78 | | max2 11892 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ (((𝐵 +
if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ∈ ℝ) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) |
79 | 19, 18, 78 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1)) |
80 | 79, 1 | syl6breqr 4625 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ 𝑋) |
81 | | ledivmul 10778 |
. . . . . . . . . . . 12
⊢ ((((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ (-𝐴 ∈ ℝ ∧ 0 <
-𝐴)) → ((((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ 𝑋 ↔ ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ≤ (-𝐴 · 𝑋))) |
82 | 11, 22, 14, 16, 81 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴) ≤ 𝑋 ↔ ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ≤ (-𝐴 · 𝑋))) |
83 | 80, 82 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) ≤ (-𝐴 · 𝑋)) |
84 | 9, 11, 76, 77, 83 | ltletrd 10076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < (-𝐴 · 𝑋)) |
85 | 65, 58 | mulneg1d 10362 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0) → (-𝐴 · 𝑋) = -(𝐴 · 𝑋)) |
86 | | df-neg 10148 |
. . . . . . . . . 10
⊢ -(𝐴 · 𝑋) = (0 − (𝐴 · 𝑋)) |
87 | 85, 86 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → (-𝐴 · 𝑋) = (0 − (𝐴 · 𝑋))) |
88 | 84, 87 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < (0 − (𝐴 · 𝑋))) |
89 | 40, 9, 43 | ltaddsub2d 10507 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0 ↔ (𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) < (0 − (𝐴 · 𝑋)))) |
90 | 88, 89 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0) |
91 | 19 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 1 ∈
ℝ) |
92 | | 0lt1 10429 |
. . . . . . . . . 10
⊢ 0 <
1 |
93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 1) |
94 | 43, 91, 22, 93, 51 | ltletrd 10076 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 𝑋) |
95 | | ltmul1 10752 |
. . . . . . . 8
⊢ ((((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) ∈ ℝ ∧ 0 ∈ ℝ
∧ (𝑋 ∈ ℝ
∧ 0 < 𝑋)) →
(((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0 ↔ (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < (0 · 𝑋))) |
96 | 41, 43, 22, 94, 95 | syl112anc 1322 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) < 0 ↔ (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < (0 · 𝑋))) |
97 | 90, 96 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < (0 · 𝑋)) |
98 | 58 | mul02d 10113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < 0) → (0 · 𝑋) = 0) |
99 | 97, 98 | breqtrd 4609 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · 𝑋) + (𝐵 + if(0 ≤ 𝐶, 𝐶, 0))) · 𝑋) < 0) |
100 | 39, 42, 43, 75, 99 | lelttrd 10074 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) < 0) |
101 | | ltnle 9996 |
. . . . 5
⊢
(((((𝐴 ·
(𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((((𝐴 ·
(𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) < 0 ↔ ¬ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) |
102 | 39, 6, 101 | sylancl 693 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < 0) → ((((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) < 0 ↔ ¬ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶))) |
103 | 100, 102 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 0) → ¬ 0 ≤ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶)) |
104 | 33, 103 | pm2.65da 598 |
. 2
⊢ (𝜑 → ¬ 𝐴 < 0) |
105 | | lelttric 10023 |
. . . 4
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ∨ 𝐴 < 0)) |
106 | 6, 12, 105 | sylancr 694 |
. . 3
⊢ (𝜑 → (0 ≤ 𝐴 ∨ 𝐴 < 0)) |
107 | 106 | ord 391 |
. 2
⊢ (𝜑 → (¬ 0 ≤ 𝐴 → 𝐴 < 0)) |
108 | 104, 107 | mt3d 139 |
1
⊢ (𝜑 → 0 ≤ 𝐴) |