Proof of Theorem discr
Step | Hyp | Ref
| Expression |
1 | | discr.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐵 ∈ ℝ) |
3 | | resqcl 12793 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → (𝐵↑2) ∈
ℝ) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵↑2) ∈ ℝ) |
5 | 4 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵↑2) ∈ ℂ) |
6 | | 4re 10974 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
7 | | discr.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ∈ ℝ) |
9 | | discr.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐶 ∈ ℝ) |
11 | 8, 10 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · 𝐶) ∈ ℝ) |
12 | | remulcl 9900 |
. . . . . . . . 9
⊢ ((4
∈ ℝ ∧ (𝐴
· 𝐶) ∈ ℝ)
→ (4 · (𝐴
· 𝐶)) ∈
ℝ) |
13 | 6, 11, 12 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (4 · (𝐴 · 𝐶)) ∈ ℝ) |
14 | 13 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (4 · (𝐴 · 𝐶)) ∈ ℂ) |
15 | | 4pos 10993 |
. . . . . . . . . 10
⊢ 0 <
4 |
16 | 6, 15 | elrpii 11711 |
. . . . . . . . 9
⊢ 4 ∈
ℝ+ |
17 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → 0 < 𝐴) |
18 | 8, 17 | elrpd 11745 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ∈
ℝ+) |
19 | | rpmulcl 11731 |
. . . . . . . . 9
⊢ ((4
∈ ℝ+ ∧ 𝐴 ∈ ℝ+) → (4
· 𝐴) ∈
ℝ+) |
20 | 16, 18, 19 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (4 · 𝐴) ∈
ℝ+) |
21 | 20 | rpcnd 11750 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (4 · 𝐴) ∈ ℂ) |
22 | 20 | rpne0d 11753 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (4 · 𝐴) ≠ 0) |
23 | 5, 14, 21, 22 | divsubdird 10719 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / (4 · 𝐴)) = (((𝐵↑2) / (4 · 𝐴)) − ((4 · (𝐴 · 𝐶)) / (4 · 𝐴)))) |
24 | 11 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · 𝐶) ∈ ℂ) |
25 | 8 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ∈ ℂ) |
26 | | 4cn 10975 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 4 ∈ ℂ) |
28 | 18 | rpne0d 11753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ≠ 0) |
29 | | 4ne0 10994 |
. . . . . . . . . 10
⊢ 4 ≠
0 |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 4 ≠ 0) |
31 | 24, 25, 27, 28, 30 | divcan5d 10706 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → ((4 · (𝐴 · 𝐶)) / (4 · 𝐴)) = ((𝐴 · 𝐶) / 𝐴)) |
32 | 10 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐶 ∈ ℂ) |
33 | 32, 25, 28 | divcan3d 10685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐴 · 𝐶) / 𝐴) = 𝐶) |
34 | 31, 33 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → ((4 · (𝐴 · 𝐶)) / (4 · 𝐴)) = 𝐶) |
35 | 34 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) − ((4 · (𝐴 · 𝐶)) / (4 · 𝐴))) = (((𝐵↑2) / (4 · 𝐴)) − 𝐶)) |
36 | 23, 35 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / (4 · 𝐴)) = (((𝐵↑2) / (4 · 𝐴)) − 𝐶)) |
37 | 4, 20 | rerpdivcld 11779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (4 · 𝐴)) ∈ ℝ) |
38 | 37 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (4 · 𝐴)) ∈ ℂ) |
39 | 38 | 2timesd 11152 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (2 · ((𝐵↑2) / (4 · 𝐴))) = (((𝐵↑2) / (4 · 𝐴)) + ((𝐵↑2) / (4 · 𝐴)))) |
40 | | 2t2e4 11054 |
. . . . . . . . . . . . 13
⊢ (2
· 2) = 4 |
41 | 40 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ ((2
· 2) · 𝐴) =
(4 · 𝐴) |
42 | | 2cnd 10970 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < 𝐴) → 2 ∈ ℂ) |
43 | 42, 42, 25 | mulassd 9942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · 2) · 𝐴) = (2 · (2 ·
𝐴))) |
44 | 41, 43 | syl5eqr 2658 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → (4 · 𝐴) = (2 · (2 · 𝐴))) |
45 | 44 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · (𝐵↑2)) / (4 · 𝐴)) = ((2 · (𝐵↑2)) / (2 · (2 · 𝐴)))) |
46 | 42, 5, 21, 22 | divassd 10715 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · (𝐵↑2)) / (4 · 𝐴)) = (2 · ((𝐵↑2) / (4 · 𝐴)))) |
47 | | 2rp 11713 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
48 | | rpmulcl 11731 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ+ ∧ 𝐴 ∈ ℝ+) → (2
· 𝐴) ∈
ℝ+) |
49 | 47, 18, 48 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < 𝐴) → (2 · 𝐴) ∈
ℝ+) |
50 | 49 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → (2 · 𝐴) ∈ ℂ) |
51 | 49 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → (2 · 𝐴) ≠ 0) |
52 | | 2ne0 10990 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
53 | 52 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → 2 ≠ 0) |
54 | 5, 50, 42, 51, 53 | divcan5d 10706 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · (𝐵↑2)) / (2 · (2 · 𝐴))) = ((𝐵↑2) / (2 · 𝐴))) |
55 | 45, 46, 54 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (2 · ((𝐵↑2) / (4 · 𝐴))) = ((𝐵↑2) / (2 · 𝐴))) |
56 | 39, 55 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) + ((𝐵↑2) / (4 · 𝐴))) = ((𝐵↑2) / (2 · 𝐴))) |
57 | 2, 49 | rerpdivcld 11779 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵 / (2 · 𝐴)) ∈ ℝ) |
58 | 57 | renegcld 10336 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → -(𝐵 / (2 · 𝐴)) ∈ ℝ) |
59 | | discr.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
60 | 59 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
61 | 60 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
62 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = -(𝐵 / (2 · 𝐴)) → (𝑥↑2) = (-(𝐵 / (2 · 𝐴))↑2)) |
63 | 62 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = -(𝐵 / (2 · 𝐴)) → (𝐴 · (𝑥↑2)) = (𝐴 · (-(𝐵 / (2 · 𝐴))↑2))) |
64 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = -(𝐵 / (2 · 𝐴)) → (𝐵 · 𝑥) = (𝐵 · -(𝐵 / (2 · 𝐴)))) |
65 | 63, 64 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = -(𝐵 / (2 · 𝐴)) → ((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) = ((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴))))) |
66 | 65 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑥 = -(𝐵 / (2 · 𝐴)) → (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) = (((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) + 𝐶)) |
67 | 66 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑥 = -(𝐵 / (2 · 𝐴)) → (0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) ↔ 0 ≤ (((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) + 𝐶))) |
68 | 67 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (-(𝐵 / (2 · 𝐴)) ∈ ℝ → (∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) → 0 ≤ (((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) + 𝐶))) |
69 | 58, 61, 68 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → 0 ≤ (((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) + 𝐶)) |
70 | 57 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵 / (2 · 𝐴)) ∈ ℂ) |
71 | | sqneg 12785 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 / (2 · 𝐴)) ∈ ℂ → (-(𝐵 / (2 · 𝐴))↑2) = ((𝐵 / (2 · 𝐴))↑2)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 0 < 𝐴) → (-(𝐵 / (2 · 𝐴))↑2) = ((𝐵 / (2 · 𝐴))↑2)) |
73 | 2 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐵 ∈ ℂ) |
74 | | sqdiv 12790 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℂ ∧ (2
· 𝐴) ∈ ℂ
∧ (2 · 𝐴) ≠
0) → ((𝐵 / (2 ·
𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2))) |
75 | 73, 50, 51, 74 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2))) |
76 | | sqval 12784 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 𝐴) ∈ ℂ
→ ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴))) |
77 | 50, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴))) |
78 | 50, 42, 25 | mulassd 9942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 0 < 𝐴) → (((2 · 𝐴) · 2) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴))) |
79 | 42, 25, 42 | mul32d 10125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · 𝐴) · 2) = ((2 · 2) ·
𝐴)) |
80 | 79, 41 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · 𝐴) · 2) = (4 · 𝐴)) |
81 | 80 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 0 < 𝐴) → (((2 · 𝐴) · 2) · 𝐴) = ((4 · 𝐴) · 𝐴)) |
82 | 77, 78, 81 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 0 < 𝐴) → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴)) |
83 | 82 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / ((2 · 𝐴)↑2)) = ((𝐵↑2) / ((4 · 𝐴) · 𝐴))) |
84 | 72, 75, 83 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 0 < 𝐴) → (-(𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((4 · 𝐴) · 𝐴))) |
85 | 5, 21, 25, 22, 28 | divdiv1d 10711 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) / 𝐴) = ((𝐵↑2) / ((4 · 𝐴) · 𝐴))) |
86 | 84, 85 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 0 < 𝐴) → (-(𝐵 / (2 · 𝐴))↑2) = (((𝐵↑2) / (4 · 𝐴)) / 𝐴)) |
87 | 86 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) = (𝐴 · (((𝐵↑2) / (4 · 𝐴)) / 𝐴))) |
88 | 38, 25, 28 | divcan2d 10682 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · (((𝐵↑2) / (4 · 𝐴)) / 𝐴)) = ((𝐵↑2) / (4 · 𝐴))) |
89 | 87, 88 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) = ((𝐵↑2) / (4 · 𝐴))) |
90 | 73, 70 | mulneg2d 10363 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵 · -(𝐵 / (2 · 𝐴))) = -(𝐵 · (𝐵 / (2 · 𝐴)))) |
91 | | sqval 12784 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ ℂ → (𝐵↑2) = (𝐵 · 𝐵)) |
92 | 73, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵↑2) = (𝐵 · 𝐵)) |
93 | 92 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (2 · 𝐴)) = ((𝐵 · 𝐵) / (2 · 𝐴))) |
94 | 73, 73, 50, 51 | divassd 10715 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵 · 𝐵) / (2 · 𝐴)) = (𝐵 · (𝐵 / (2 · 𝐴)))) |
95 | 93, 94 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (2 · 𝐴)) = (𝐵 · (𝐵 / (2 · 𝐴)))) |
96 | 95 | negeqd 10154 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 0 < 𝐴) → -((𝐵↑2) / (2 · 𝐴)) = -(𝐵 · (𝐵 / (2 · 𝐴)))) |
97 | 90, 96 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐵 · -(𝐵 / (2 · 𝐴))) = -((𝐵↑2) / (2 · 𝐴))) |
98 | 89, 97 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) = (((𝐵↑2) / (4 · 𝐴)) + -((𝐵↑2) / (2 · 𝐴)))) |
99 | 4, 49 | rerpdivcld 11779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (2 · 𝐴)) ∈ ℝ) |
100 | 99 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (2 · 𝐴)) ∈ ℂ) |
101 | 38, 100 | negsubd 10277 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) + -((𝐵↑2) / (2 · 𝐴))) = (((𝐵↑2) / (4 · 𝐴)) − ((𝐵↑2) / (2 · 𝐴)))) |
102 | 98, 101 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) = (((𝐵↑2) / (4 · 𝐴)) − ((𝐵↑2) / (2 · 𝐴)))) |
103 | 102 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) + 𝐶) = ((((𝐵↑2) / (4 · 𝐴)) − ((𝐵↑2) / (2 · 𝐴))) + 𝐶)) |
104 | 38, 32, 100 | addsubd 10292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → ((((𝐵↑2) / (4 · 𝐴)) + 𝐶) − ((𝐵↑2) / (2 · 𝐴))) = ((((𝐵↑2) / (4 · 𝐴)) − ((𝐵↑2) / (2 · 𝐴))) + 𝐶)) |
105 | 103, 104 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐴 · (-(𝐵 / (2 · 𝐴))↑2)) + (𝐵 · -(𝐵 / (2 · 𝐴)))) + 𝐶) = ((((𝐵↑2) / (4 · 𝐴)) + 𝐶) − ((𝐵↑2) / (2 · 𝐴)))) |
106 | 69, 105 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → 0 ≤ ((((𝐵↑2) / (4 · 𝐴)) + 𝐶) − ((𝐵↑2) / (2 · 𝐴)))) |
107 | 37, 10 | readdcld 9948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) + 𝐶) ∈ ℝ) |
108 | 107, 99 | subge0d 10496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (0 ≤ ((((𝐵↑2) / (4 · 𝐴)) + 𝐶) − ((𝐵↑2) / (2 · 𝐴))) ↔ ((𝐵↑2) / (2 · 𝐴)) ≤ (((𝐵↑2) / (4 · 𝐴)) + 𝐶))) |
109 | 106, 108 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (2 · 𝐴)) ≤ (((𝐵↑2) / (4 · 𝐴)) + 𝐶)) |
110 | 56, 109 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) + ((𝐵↑2) / (4 · 𝐴))) ≤ (((𝐵↑2) / (4 · 𝐴)) + 𝐶)) |
111 | 37, 10, 37 | leadd2d 10501 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) ≤ 𝐶 ↔ (((𝐵↑2) / (4 · 𝐴)) + ((𝐵↑2) / (4 · 𝐴))) ≤ (((𝐵↑2) / (4 · 𝐴)) + 𝐶))) |
112 | 110, 111 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) / (4 · 𝐴)) ≤ 𝐶) |
113 | 37, 10 | suble0d 10497 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → ((((𝐵↑2) / (4 · 𝐴)) − 𝐶) ≤ 0 ↔ ((𝐵↑2) / (4 · 𝐴)) ≤ 𝐶)) |
114 | 112, 113 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) / (4 · 𝐴)) − 𝐶) ≤ 0) |
115 | 36, 114 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / (4 · 𝐴)) ≤ 0) |
116 | 4, 13 | resubcld 10337 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℝ) |
117 | | 0red 9920 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → 0 ∈ ℝ) |
118 | 116, 117,
20 | ledivmuld 11801 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → ((((𝐵↑2) − (4 · (𝐴 · 𝐶))) / (4 · 𝐴)) ≤ 0 ↔ ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ ((4 · 𝐴) · 0))) |
119 | 115, 118 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ ((4 · 𝐴) · 0)) |
120 | 21 | mul01d 10114 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐴) → ((4 · 𝐴) · 0) = 0) |
121 | 119, 120 | breqtrd 4609 |
. 2
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ 0) |
122 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 𝐶 ∈ ℝ) |
123 | 122 | ltp1d 10833 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 𝐶 < (𝐶 + 1)) |
124 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℝ → (𝐶 + 1) ∈
ℝ) |
125 | 122, 124 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (𝐶 + 1) ∈ ℝ) |
126 | 122, 125 | ltnegd 10484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (𝐶 < (𝐶 + 1) ↔ -(𝐶 + 1) < -𝐶)) |
127 | 123, 126 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → -(𝐶 + 1) < -𝐶) |
128 | | df-neg 10148 |
. . . . . . . . . 10
⊢ -𝐶 = (0 − 𝐶) |
129 | 127, 128 | syl6breq 4624 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → -(𝐶 + 1) < (0 − 𝐶)) |
130 | 125 | renegcld 10336 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → -(𝐶 + 1) ∈ ℝ) |
131 | | 0red 9920 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 0 ∈
ℝ) |
132 | 130, 122,
131 | ltaddsubd 10506 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → ((-(𝐶 + 1) + 𝐶) < 0 ↔ -(𝐶 + 1) < (0 − 𝐶))) |
133 | 129, 132 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (-(𝐶 + 1) + 𝐶) < 0) |
134 | 133 | expr 641 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 = 𝐴) → (𝐵 ≠ 0 → (-(𝐶 + 1) + 𝐶) < 0)) |
135 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℝ) |
136 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 𝐵 ≠ 0) |
137 | 130, 135,
136 | redivcld 10732 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (-(𝐶 + 1) / 𝐵) ∈ ℝ) |
138 | 60 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → ∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) |
139 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (-(𝐶 + 1) / 𝐵) → (𝑥↑2) = ((-(𝐶 + 1) / 𝐵)↑2)) |
140 | 139 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (-(𝐶 + 1) / 𝐵) → (𝐴 · (𝑥↑2)) = (𝐴 · ((-(𝐶 + 1) / 𝐵)↑2))) |
141 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (-(𝐶 + 1) / 𝐵) → (𝐵 · 𝑥) = (𝐵 · (-(𝐶 + 1) / 𝐵))) |
142 | 140, 141 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (-(𝐶 + 1) / 𝐵) → ((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) = ((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵)))) |
143 | 142 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (-(𝐶 + 1) / 𝐵) → (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) = (((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) + 𝐶)) |
144 | 143 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑥 = (-(𝐶 + 1) / 𝐵) → (0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) ↔ 0 ≤ (((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) + 𝐶))) |
145 | 144 | rspcv 3278 |
. . . . . . . . . . 11
⊢ ((-(𝐶 + 1) / 𝐵) ∈ ℝ → (∀𝑥 ∈ ℝ 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶) → 0 ≤ (((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) + 𝐶))) |
146 | 137, 138,
145 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 0 ≤ (((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) + 𝐶)) |
147 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 0 = 𝐴) |
148 | 147 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (0 · ((-(𝐶 + 1) / 𝐵)↑2)) = (𝐴 · ((-(𝐶 + 1) / 𝐵)↑2))) |
149 | 137 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (-(𝐶 + 1) / 𝐵) ∈ ℂ) |
150 | | sqcl 12787 |
. . . . . . . . . . . . . . . 16
⊢ ((-(𝐶 + 1) / 𝐵) ∈ ℂ → ((-(𝐶 + 1) / 𝐵)↑2) ∈ ℂ) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → ((-(𝐶 + 1) / 𝐵)↑2) ∈ ℂ) |
152 | 151 | mul02d 10113 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (0 · ((-(𝐶 + 1) / 𝐵)↑2)) = 0) |
153 | 148, 152 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) = 0) |
154 | 130 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → -(𝐶 + 1) ∈ ℂ) |
155 | 135 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℂ) |
156 | 154, 155,
136 | divcan2d 10682 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (𝐵 · (-(𝐶 + 1) / 𝐵)) = -(𝐶 + 1)) |
157 | 153, 156 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → ((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) = (0 + -(𝐶 + 1))) |
158 | 154 | addid2d 10116 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (0 + -(𝐶 + 1)) = -(𝐶 + 1)) |
159 | 157, 158 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → ((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) = -(𝐶 + 1)) |
160 | 159 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (((𝐴 · ((-(𝐶 + 1) / 𝐵)↑2)) + (𝐵 · (-(𝐶 + 1) / 𝐵))) + 𝐶) = (-(𝐶 + 1) + 𝐶)) |
161 | 146, 160 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → 0 ≤ (-(𝐶 + 1) + 𝐶)) |
162 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
163 | 130, 122 | readdcld 9948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (-(𝐶 + 1) + 𝐶) ∈ ℝ) |
164 | | lenlt 9995 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (-(𝐶 +
1) + 𝐶) ∈ ℝ)
→ (0 ≤ (-(𝐶 + 1) +
𝐶) ↔ ¬ (-(𝐶 + 1) + 𝐶) < 0)) |
165 | 162, 163,
164 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → (0 ≤ (-(𝐶 + 1) + 𝐶) ↔ ¬ (-(𝐶 + 1) + 𝐶) < 0)) |
166 | 161, 165 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (0 = 𝐴 ∧ 𝐵 ≠ 0)) → ¬ (-(𝐶 + 1) + 𝐶) < 0) |
167 | 166 | expr 641 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 = 𝐴) → (𝐵 ≠ 0 → ¬ (-(𝐶 + 1) + 𝐶) < 0)) |
168 | 134, 167 | pm2.65d 186 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = 𝐴) → ¬ 𝐵 ≠ 0) |
169 | | nne 2786 |
. . . . . 6
⊢ (¬
𝐵 ≠ 0 ↔ 𝐵 = 0) |
170 | 168, 169 | sylib 207 |
. . . . 5
⊢ ((𝜑 ∧ 0 = 𝐴) → 𝐵 = 0) |
171 | 170 | sq0id 12819 |
. . . 4
⊢ ((𝜑 ∧ 0 = 𝐴) → (𝐵↑2) = 0) |
172 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 = 𝐴) → 0 = 𝐴) |
173 | 172 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 = 𝐴) → (0 · 𝐶) = (𝐴 · 𝐶)) |
174 | 9 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
175 | 174 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 = 𝐴) → 𝐶 ∈ ℂ) |
176 | 175 | mul02d 10113 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 = 𝐴) → (0 · 𝐶) = 0) |
177 | 173, 176 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = 𝐴) → (𝐴 · 𝐶) = 0) |
178 | 177 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 0 = 𝐴) → (4 · (𝐴 · 𝐶)) = (4 · 0)) |
179 | 26 | mul01i 10105 |
. . . . 5
⊢ (4
· 0) = 0 |
180 | 178, 179 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ 0 = 𝐴) → (4 · (𝐴 · 𝐶)) = 0) |
181 | 171, 180 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ 0 = 𝐴) → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) = (0 − 0)) |
182 | | 0m0e0 11007 |
. . . 4
⊢ (0
− 0) = 0 |
183 | | 0le0 10987 |
. . . 4
⊢ 0 ≤
0 |
184 | 182, 183 | eqbrtri 4604 |
. . 3
⊢ (0
− 0) ≤ 0 |
185 | 181, 184 | syl6eqbr 4622 |
. 2
⊢ ((𝜑 ∧ 0 = 𝐴) → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ 0) |
186 | | eqid 2610 |
. . . 4
⊢ if(1 ≤
(((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) = if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) |
187 | 7, 1, 9, 59, 186 | discr1 12862 |
. . 3
⊢ (𝜑 → 0 ≤ 𝐴) |
188 | | leloe 10003 |
. . . 4
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
189 | 162, 7, 188 | sylancr 694 |
. . 3
⊢ (𝜑 → (0 ≤ 𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
190 | 187, 189 | mpbid 221 |
. 2
⊢ (𝜑 → (0 < 𝐴 ∨ 0 = 𝐴)) |
191 | 121, 185,
190 | mpjaodan 823 |
1
⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ 0) |