Proof of Theorem quad2
Step | Hyp | Ref
| Expression |
1 | | 2cn 11455 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
2 | | quad.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | mulcl 10358 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → (2 · 𝐴) ∈ ℂ) |
4 | 1, 2, 3 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐴) ∈
ℂ) |
5 | | quad.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℂ) |
6 | 4, 5 | mulcld 10399 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ) |
7 | | quad.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
8 | 6, 7 | addcld 10398 |
. . . . 5
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ) |
9 | 8 | sqcld 13330 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ) |
10 | | quad2.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) |
11 | 10 | sqcld 13330 |
. . . 4
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
12 | 9, 11 | subeq0ad 10746 |
. . 3
⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2))) |
13 | 5 | sqcld 13330 |
. . . . . . 7
⊢ (𝜑 → (𝑋↑2) ∈ ℂ) |
14 | 2, 13 | mulcld 10399 |
. . . . . 6
⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ) |
15 | 7, 5 | mulcld 10399 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ) |
16 | | quad.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
17 | 15, 16 | addcld 10398 |
. . . . . 6
⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ) |
18 | 14, 17 | addcld 10398 |
. . . . 5
⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ) |
19 | | 0cnd 10371 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℂ) |
20 | | 4cn 11466 |
. . . . . 6
⊢ 4 ∈
ℂ |
21 | | mulcl 10358 |
. . . . . 6
⊢ ((4
∈ ℂ ∧ 𝐴
∈ ℂ) → (4 · 𝐴) ∈ ℂ) |
22 | 20, 2, 21 | sylancr 581 |
. . . . 5
⊢ (𝜑 → (4 · 𝐴) ∈
ℂ) |
23 | 20 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 4 ∈
ℂ) |
24 | | 4ne0 11495 |
. . . . . . 7
⊢ 4 ≠
0 |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 4 ≠ 0) |
26 | | quad.z |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 0) |
27 | 23, 2, 25, 26 | mulne0d 11030 |
. . . . 5
⊢ (𝜑 → (4 · 𝐴) ≠ 0) |
28 | 18, 19, 22, 27 | mulcand 11011 |
. . . 4
⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)) |
29 | 6 | sqcld 13330 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ) |
30 | 6, 7 | mulcld 10399 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) |
31 | | mulcl 10358 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2
· 𝐴) · 𝑋) · 𝐵)) ∈ ℂ) |
32 | 1, 30, 31 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → (2 · (((2 ·
𝐴) · 𝑋) · 𝐵)) ∈ ℂ) |
33 | 2, 16 | mulcld 10399 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
34 | | mulcl 10358 |
. . . . . . . . 9
⊢ ((4
∈ ℂ ∧ (𝐴
· 𝐶) ∈ ℂ)
→ (4 · (𝐴
· 𝐶)) ∈
ℂ) |
35 | 20, 33, 34 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ) |
36 | 29, 32, 35 | addassd 10401 |
. . . . . . 7
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))) |
37 | 7 | sqcld 13330 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
38 | 29, 32 | addcld 10398 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ) |
39 | 37, 38, 35 | pnncand 10775 |
. . . . . . 7
⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶)))) |
40 | 4, 5 | sqmuld 13344 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2))) |
41 | | sq2 13284 |
. . . . . . . . . . . . 13
⊢
(2↑2) = 4 |
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2↑2) =
4) |
43 | 2 | sqvald 13329 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
44 | 42, 43 | oveq12d 6942 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2↑2) ·
(𝐴↑2)) = (4 ·
(𝐴 · 𝐴))) |
45 | | sqmul 13249 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2))) |
46 | 1, 2, 45 | sylancr 581 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) ·
(𝐴↑2))) |
47 | 23, 2, 2 | mulassd 10402 |
. . . . . . . . . . 11
⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴))) |
48 | 44, 46, 47 | 3eqtr4d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴)) |
49 | 48 | oveq1d 6939 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2))) |
50 | 22, 2, 13 | mulassd 10402 |
. . . . . . . . 9
⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2)))) |
51 | 40, 49, 50 | 3eqtrrd 2819 |
. . . . . . . 8
⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2)) |
52 | 22, 15, 16 | adddid 10403 |
. . . . . . . . 9
⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶))) |
53 | | 2t2e4 11551 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· 2) = 4 |
54 | 53 | oveq1i 6934 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 2) · 𝐴) =
(4 · 𝐴) |
55 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) |
56 | 55, 55, 2 | mulassd 10402 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 2) ·
𝐴) = (2 · (2
· 𝐴))) |
57 | 54, 56 | syl5eqr 2828 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (4 · 𝐴) = (2 · (2 ·
𝐴))) |
58 | 57 | oveq1d 6939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵)) |
59 | 55, 4, 7 | mulassd 10402 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (2 ·
𝐴)) · 𝐵) = (2 · ((2 ·
𝐴) · 𝐵))) |
60 | 58, 59 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵))) |
61 | 60 | oveq1d 6939 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋)) |
62 | 4, 7 | mulcld 10399 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ) |
63 | 55, 62, 5 | mulassd 10402 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · ((2 ·
𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋))) |
64 | 61, 63 | eqtrd 2814 |
. . . . . . . . . . 11
⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋))) |
65 | 22, 7, 5 | mulassd 10402 |
. . . . . . . . . . 11
⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋))) |
66 | 4, 7, 5 | mul32d 10588 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵)) |
67 | 66 | oveq2d 6940 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · (((2 ·
𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) |
68 | 64, 65, 67 | 3eqtr3d 2822 |
. . . . . . . . . 10
⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) |
69 | 23, 2, 16 | mulassd 10402 |
. . . . . . . . . 10
⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶))) |
70 | 68, 69 | oveq12d 6942 |
. . . . . . . . 9
⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))) |
71 | 52, 70 | eqtrd 2814 |
. . . . . . . 8
⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))) |
72 | 51, 71 | oveq12d 6942 |
. . . . . . 7
⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))) |
73 | 36, 39, 72 | 3eqtr4rd 2825 |
. . . . . 6
⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
74 | 22, 14, 17 | adddid 10403 |
. . . . . 6
⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)))) |
75 | | binom2 13303 |
. . . . . . . . 9
⊢ ((((2
· 𝐴) · 𝑋) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((2
· 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2))) |
76 | 6, 7, 75 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2))) |
77 | 38, 37 | addcomd 10580 |
. . . . . . . 8
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))))) |
78 | 76, 77 | eqtrd 2814 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))))) |
79 | | quad2.2 |
. . . . . . 7
⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) |
80 | 78, 79 | oveq12d 6942 |
. . . . . 6
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
81 | 73, 74, 80 | 3eqtr4d 2824 |
. . . . 5
⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2))) |
82 | 22 | mul01d 10577 |
. . . . 5
⊢ (𝜑 → ((4 · 𝐴) · 0) =
0) |
83 | 81, 82 | eqeq12d 2793 |
. . . 4
⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0)) |
84 | 28, 83 | bitr3d 273 |
. . 3
⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0)) |
85 | 6, 7 | subnegd 10743 |
. . . . 5
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵)) |
86 | 85 | oveq1d 6939 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2)) |
87 | 86 | eqeq1d 2780 |
. . 3
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2))) |
88 | 12, 84, 87 | 3bitr4d 303 |
. 2
⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2))) |
89 | 7 | negcld 10723 |
. . . 4
⊢ (𝜑 → -𝐵 ∈ ℂ) |
90 | 6, 89 | subcld 10736 |
. . 3
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ) |
91 | | sqeqor 13302 |
. . 3
⊢ (((((2
· 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 ·
𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷))) |
92 | 90, 10, 91 | syl2anc 579 |
. 2
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷))) |
93 | 6, 89, 10 | subaddd 10754 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋))) |
94 | 89, 10 | addcld 10398 |
. . . . . 6
⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ) |
95 | | 2ne0 11491 |
. . . . . . . 8
⊢ 2 ≠
0 |
96 | 95 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ≠ 0) |
97 | 55, 2, 96, 26 | mulne0d 11030 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐴) ≠ 0) |
98 | 94, 4, 5, 97 | divmuld 11176 |
. . . . 5
⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))) |
99 | | eqcom 2785 |
. . . . 5
⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋) |
100 | | eqcom 2785 |
. . . . 5
⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)) |
101 | 98, 99, 100 | 3bitr4g 306 |
. . . 4
⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋))) |
102 | 93, 101 | bitr4d 274 |
. . 3
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)))) |
103 | 89, 10 | negsubd 10742 |
. . . . 5
⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷)) |
104 | 103 | eqeq1d 2780 |
. . . 4
⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋))) |
105 | 10 | negcld 10723 |
. . . . 5
⊢ (𝜑 → -𝐷 ∈ ℂ) |
106 | 6, 89, 105 | subaddd 10754 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋))) |
107 | 89, 10 | subcld 10736 |
. . . . . 6
⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ) |
108 | 107, 4, 5, 97 | divmuld 11176 |
. . . . 5
⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷))) |
109 | | eqcom 2785 |
. . . . 5
⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋) |
110 | | eqcom 2785 |
. . . . 5
⊢ ((-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)) |
111 | 108, 109,
110 | 3bitr4g 306 |
. . . 4
⊢ (𝜑 → (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋))) |
112 | 104, 106,
111 | 3bitr4d 303 |
. . 3
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))) |
113 | 102, 112 | orbi12d 905 |
. 2
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷) ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))) |
114 | 88, 92, 113 | 3bitrd 297 |
1
⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))) |