Proof of Theorem quad2
Step | Hyp | Ref
| Expression |
1 | | 2cn 12048 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
2 | | quad.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | mulcl 10956 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → (2 · 𝐴) ∈ ℂ) |
4 | 1, 2, 3 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐴) ∈
ℂ) |
5 | | quad.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℂ) |
6 | 4, 5 | mulcld 10996 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ) |
7 | | quad.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
8 | 6, 7 | addcld 10995 |
. . . . 5
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ) |
9 | 8 | sqcld 13860 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ) |
10 | | quad2.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) |
11 | 10 | sqcld 13860 |
. . . 4
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
12 | 9, 11 | subeq0ad 11342 |
. . 3
⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2))) |
13 | 5 | sqcld 13860 |
. . . . . . 7
⊢ (𝜑 → (𝑋↑2) ∈ ℂ) |
14 | 2, 13 | mulcld 10996 |
. . . . . 6
⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ) |
15 | 7, 5 | mulcld 10996 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ) |
16 | | quad.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
17 | 15, 16 | addcld 10995 |
. . . . . 6
⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ) |
18 | 14, 17 | addcld 10995 |
. . . . 5
⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ) |
19 | | 0cnd 10969 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℂ) |
20 | | 4cn 12058 |
. . . . . 6
⊢ 4 ∈
ℂ |
21 | | mulcl 10956 |
. . . . . 6
⊢ ((4
∈ ℂ ∧ 𝐴
∈ ℂ) → (4 · 𝐴) ∈ ℂ) |
22 | 20, 2, 21 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (4 · 𝐴) ∈
ℂ) |
23 | 20 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 4 ∈
ℂ) |
24 | | 4ne0 12081 |
. . . . . . 7
⊢ 4 ≠
0 |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 4 ≠ 0) |
26 | | quad.z |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 0) |
27 | 23, 2, 25, 26 | mulne0d 11627 |
. . . . 5
⊢ (𝜑 → (4 · 𝐴) ≠ 0) |
28 | 18, 19, 22, 27 | mulcand 11608 |
. . . 4
⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)) |
29 | 6 | sqcld 13860 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ) |
30 | 6, 7 | mulcld 10996 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) |
31 | | mulcl 10956 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2
· 𝐴) · 𝑋) · 𝐵)) ∈ ℂ) |
32 | 1, 30, 31 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (2 · (((2 ·
𝐴) · 𝑋) · 𝐵)) ∈ ℂ) |
33 | 2, 16 | mulcld 10996 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
34 | | mulcl 10956 |
. . . . . . . . 9
⊢ ((4
∈ ℂ ∧ (𝐴
· 𝐶) ∈ ℂ)
→ (4 · (𝐴
· 𝐶)) ∈
ℂ) |
35 | 20, 33, 34 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ) |
36 | 29, 32, 35 | addassd 10998 |
. . . . . . 7
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))) |
37 | 7 | sqcld 13860 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
38 | 29, 32 | addcld 10995 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ) |
39 | 37, 38, 35 | pnncand 11371 |
. . . . . . 7
⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶)))) |
40 | 4, 5 | sqmuld 13874 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2))) |
41 | | sq2 13912 |
. . . . . . . . . . . . 13
⊢
(2↑2) = 4 |
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2↑2) =
4) |
43 | 2 | sqvald 13859 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
44 | 42, 43 | oveq12d 7289 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2↑2) ·
(𝐴↑2)) = (4 ·
(𝐴 · 𝐴))) |
45 | | sqmul 13837 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2))) |
46 | 1, 2, 45 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) ·
(𝐴↑2))) |
47 | 23, 2, 2 | mulassd 10999 |
. . . . . . . . . . 11
⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴))) |
48 | 44, 46, 47 | 3eqtr4d 2790 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴)) |
49 | 48 | oveq1d 7286 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2))) |
50 | 22, 2, 13 | mulassd 10999 |
. . . . . . . . 9
⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2)))) |
51 | 40, 49, 50 | 3eqtrrd 2785 |
. . . . . . . 8
⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2)) |
52 | 22, 15, 16 | adddid 11000 |
. . . . . . . . 9
⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶))) |
53 | | 2t2e4 12137 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· 2) = 4 |
54 | 53 | oveq1i 7281 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 2) · 𝐴) =
(4 · 𝐴) |
55 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) |
56 | 55, 55, 2 | mulassd 10999 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 2) ·
𝐴) = (2 · (2
· 𝐴))) |
57 | 54, 56 | eqtr3id 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (4 · 𝐴) = (2 · (2 ·
𝐴))) |
58 | 57 | oveq1d 7286 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵)) |
59 | 55, 4, 7 | mulassd 10999 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (2 ·
𝐴)) · 𝐵) = (2 · ((2 ·
𝐴) · 𝐵))) |
60 | 58, 59 | eqtrd 2780 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵))) |
61 | 60 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋)) |
62 | 4, 7 | mulcld 10996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ) |
63 | 55, 62, 5 | mulassd 10999 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · ((2 ·
𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋))) |
64 | 61, 63 | eqtrd 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋))) |
65 | 22, 7, 5 | mulassd 10999 |
. . . . . . . . . . 11
⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋))) |
66 | 4, 7, 5 | mul32d 11185 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵)) |
67 | 66 | oveq2d 7287 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · (((2 ·
𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) |
68 | 64, 65, 67 | 3eqtr3d 2788 |
. . . . . . . . . 10
⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) |
69 | 23, 2, 16 | mulassd 10999 |
. . . . . . . . . 10
⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶))) |
70 | 68, 69 | oveq12d 7289 |
. . . . . . . . 9
⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))) |
71 | 52, 70 | eqtrd 2780 |
. . . . . . . 8
⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))) |
72 | 51, 71 | oveq12d 7289 |
. . . . . . 7
⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))) |
73 | 36, 39, 72 | 3eqtr4rd 2791 |
. . . . . 6
⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
74 | 22, 14, 17 | adddid 11000 |
. . . . . 6
⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)))) |
75 | | binom2 13931 |
. . . . . . . . 9
⊢ ((((2
· 𝐴) · 𝑋) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((2
· 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2))) |
76 | 6, 7, 75 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2))) |
77 | 38, 37, 76 | comraddd 11189 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))))) |
78 | | quad2.2 |
. . . . . . 7
⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) |
79 | 77, 78 | oveq12d 7289 |
. . . . . 6
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
80 | 73, 74, 79 | 3eqtr4d 2790 |
. . . . 5
⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2))) |
81 | 22 | mul01d 11174 |
. . . . 5
⊢ (𝜑 → ((4 · 𝐴) · 0) =
0) |
82 | 80, 81 | eqeq12d 2756 |
. . . 4
⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0)) |
83 | 28, 82 | bitr3d 280 |
. . 3
⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0)) |
84 | 6, 7 | subnegd 11339 |
. . . . 5
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵)) |
85 | 84 | oveq1d 7286 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2)) |
86 | 85 | eqeq1d 2742 |
. . 3
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2))) |
87 | 12, 83, 86 | 3bitr4d 311 |
. 2
⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2))) |
88 | 7 | negcld 11319 |
. . . 4
⊢ (𝜑 → -𝐵 ∈ ℂ) |
89 | 6, 88 | subcld 11332 |
. . 3
⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ) |
90 | | sqeqor 13930 |
. . 3
⊢ (((((2
· 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 ·
𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷))) |
91 | 89, 10, 90 | syl2anc 584 |
. 2
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷))) |
92 | 6, 88, 10 | subaddd 11350 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋))) |
93 | 88, 10 | addcld 10995 |
. . . . . 6
⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ) |
94 | | 2ne0 12077 |
. . . . . . . 8
⊢ 2 ≠
0 |
95 | 94 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ≠ 0) |
96 | 55, 2, 95, 26 | mulne0d 11627 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐴) ≠ 0) |
97 | 93, 4, 5, 96 | divmuld 11773 |
. . . . 5
⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))) |
98 | | eqcom 2747 |
. . . . 5
⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋) |
99 | | eqcom 2747 |
. . . . 5
⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)) |
100 | 97, 98, 99 | 3bitr4g 314 |
. . . 4
⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋))) |
101 | 92, 100 | bitr4d 281 |
. . 3
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)))) |
102 | 88, 10 | negsubd 11338 |
. . . . 5
⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷)) |
103 | 102 | eqeq1d 2742 |
. . . 4
⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋))) |
104 | 10 | negcld 11319 |
. . . . 5
⊢ (𝜑 → -𝐷 ∈ ℂ) |
105 | 6, 88, 104 | subaddd 11350 |
. . . 4
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋))) |
106 | 88, 10 | subcld 11332 |
. . . . . 6
⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ) |
107 | 106, 4, 5, 96 | divmuld 11773 |
. . . . 5
⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷))) |
108 | | eqcom 2747 |
. . . . 5
⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋) |
109 | | eqcom 2747 |
. . . . 5
⊢ ((-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)) |
110 | 107, 108,
109 | 3bitr4g 314 |
. . . 4
⊢ (𝜑 → (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋))) |
111 | 103, 105,
110 | 3bitr4d 311 |
. . 3
⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))) |
112 | 101, 111 | orbi12d 916 |
. 2
⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷) ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))) |
113 | 87, 91, 112 | 3bitrd 305 |
1
⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))) |