Step | Hyp | Ref
| Expression |
1 | | 2cn 12235 |
. . . . . . . 8
โข 2 โ
โ |
2 | | quad.a |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
3 | | mulcl 11142 |
. . . . . . . 8
โข ((2
โ โ โง ๐ด
โ โ) โ (2 ยท ๐ด) โ โ) |
4 | 1, 2, 3 | sylancr 588 |
. . . . . . 7
โข (๐ โ (2 ยท ๐ด) โ
โ) |
5 | | quad.x |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
6 | 4, 5 | mulcld 11182 |
. . . . . 6
โข (๐ โ ((2 ยท ๐ด) ยท ๐) โ โ) |
7 | | quad.b |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
8 | 6, 7 | addcld 11181 |
. . . . 5
โข (๐ โ (((2 ยท ๐ด) ยท ๐) + ๐ต) โ โ) |
9 | 8 | sqcld 14056 |
. . . 4
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) โ โ) |
10 | | quad2.d |
. . . . 5
โข (๐ โ ๐ท โ โ) |
11 | 10 | sqcld 14056 |
. . . 4
โข (๐ โ (๐ทโ2) โ โ) |
12 | 9, 11 | subeq0ad 11529 |
. . 3
โข (๐ โ ((((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) โ (๐ทโ2)) = 0 โ ((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) = (๐ทโ2))) |
13 | 5 | sqcld 14056 |
. . . . . . 7
โข (๐ โ (๐โ2) โ โ) |
14 | 2, 13 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ด ยท (๐โ2)) โ โ) |
15 | 7, 5 | mulcld 11182 |
. . . . . . 7
โข (๐ โ (๐ต ยท ๐) โ โ) |
16 | | quad.c |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
17 | 15, 16 | addcld 11181 |
. . . . . 6
โข (๐ โ ((๐ต ยท ๐) + ๐ถ) โ โ) |
18 | 14, 17 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ)) โ โ) |
19 | | 0cnd 11155 |
. . . . 5
โข (๐ โ 0 โ
โ) |
20 | | 4cn 12245 |
. . . . . 6
โข 4 โ
โ |
21 | | mulcl 11142 |
. . . . . 6
โข ((4
โ โ โง ๐ด
โ โ) โ (4 ยท ๐ด) โ โ) |
22 | 20, 2, 21 | sylancr 588 |
. . . . 5
โข (๐ โ (4 ยท ๐ด) โ
โ) |
23 | 20 | a1i 11 |
. . . . . 6
โข (๐ โ 4 โ
โ) |
24 | | 4ne0 12268 |
. . . . . . 7
โข 4 โ
0 |
25 | 24 | a1i 11 |
. . . . . 6
โข (๐ โ 4 โ 0) |
26 | | quad.z |
. . . . . 6
โข (๐ โ ๐ด โ 0) |
27 | 23, 2, 25, 26 | mulne0d 11814 |
. . . . 5
โข (๐ โ (4 ยท ๐ด) โ 0) |
28 | 18, 19, 22, 27 | mulcand 11795 |
. . . 4
โข (๐ โ (((4 ยท ๐ด) ยท ((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ))) = ((4 ยท ๐ด) ยท 0) โ ((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ)) = 0)) |
29 | 6 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐ด) ยท ๐)โ2) โ โ) |
30 | 6, 7 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐ด) ยท ๐) ยท ๐ต) โ โ) |
31 | | mulcl 11142 |
. . . . . . . . 9
โข ((2
โ โ โง (((2 ยท ๐ด) ยท ๐) ยท ๐ต) โ โ) โ (2 ยท (((2
ยท ๐ด) ยท ๐) ยท ๐ต)) โ โ) |
32 | 1, 30, 31 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (2 ยท (((2 ยท
๐ด) ยท ๐) ยท ๐ต)) โ โ) |
33 | 2, 16 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
34 | | mulcl 11142 |
. . . . . . . . 9
โข ((4
โ โ โง (๐ด
ยท ๐ถ) โ โ)
โ (4 ยท (๐ด
ยท ๐ถ)) โ
โ) |
35 | 20, 33, 34 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (4 ยท (๐ด ยท ๐ถ)) โ โ) |
36 | 29, 32, 35 | addassd 11184 |
. . . . . . 7
โข (๐ โ (((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) + (4 ยท (๐ด ยท ๐ถ))) = ((((2 ยท ๐ด) ยท ๐)โ2) + ((2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)) + (4 ยท (๐ด ยท ๐ถ))))) |
37 | 7 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (๐ตโ2) โ โ) |
38 | 29, 32 | addcld 11181 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) โ โ) |
39 | 37, 38, 35 | pnncand 11558 |
. . . . . . 7
โข (๐ โ (((๐ตโ2) + ((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)))) โ ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) = (((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) + (4 ยท (๐ด ยท ๐ถ)))) |
40 | 4, 5 | sqmuld 14070 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐ด) ยท ๐)โ2) = (((2 ยท ๐ด)โ2) ยท (๐โ2))) |
41 | | sq2 14108 |
. . . . . . . . . . . . 13
โข
(2โ2) = 4 |
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (2โ2) =
4) |
43 | 2 | sqvald 14055 |
. . . . . . . . . . . 12
โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
44 | 42, 43 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ โ ((2โ2) ยท
(๐ดโ2)) = (4 ยท
(๐ด ยท ๐ด))) |
45 | | sqmul 14031 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐ด
โ โ) โ ((2 ยท ๐ด)โ2) = ((2โ2) ยท (๐ดโ2))) |
46 | 1, 2, 45 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐ด)โ2) = ((2โ2) ยท
(๐ดโ2))) |
47 | 23, 2, 2 | mulassd 11185 |
. . . . . . . . . . 11
โข (๐ โ ((4 ยท ๐ด) ยท ๐ด) = (4 ยท (๐ด ยท ๐ด))) |
48 | 44, 46, 47 | 3eqtr4d 2787 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐ด)โ2) = ((4 ยท ๐ด) ยท ๐ด)) |
49 | 48 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐ด)โ2) ยท (๐โ2)) = (((4 ยท ๐ด) ยท ๐ด) ยท (๐โ2))) |
50 | 22, 2, 13 | mulassd 11185 |
. . . . . . . . 9
โข (๐ โ (((4 ยท ๐ด) ยท ๐ด) ยท (๐โ2)) = ((4 ยท ๐ด) ยท (๐ด ยท (๐โ2)))) |
51 | 40, 49, 50 | 3eqtrrd 2782 |
. . . . . . . 8
โข (๐ โ ((4 ยท ๐ด) ยท (๐ด ยท (๐โ2))) = (((2 ยท ๐ด) ยท ๐)โ2)) |
52 | 22, 15, 16 | adddid 11186 |
. . . . . . . . 9
โข (๐ โ ((4 ยท ๐ด) ยท ((๐ต ยท ๐) + ๐ถ)) = (((4 ยท ๐ด) ยท (๐ต ยท ๐)) + ((4 ยท ๐ด) ยท ๐ถ))) |
53 | | 2t2e4 12324 |
. . . . . . . . . . . . . . . . 17
โข (2
ยท 2) = 4 |
54 | 53 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท 2) ยท ๐ด) =
(4 ยท ๐ด) |
55 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ
โ) |
56 | 55, 55, 2 | mulassd 11185 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2 ยท 2) ยท
๐ด) = (2 ยท (2
ยท ๐ด))) |
57 | 54, 56 | eqtr3id 2791 |
. . . . . . . . . . . . . . 15
โข (๐ โ (4 ยท ๐ด) = (2 ยท (2 ยท
๐ด))) |
58 | 57 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ โ ((4 ยท ๐ด) ยท ๐ต) = ((2 ยท (2 ยท ๐ด)) ยท ๐ต)) |
59 | 55, 4, 7 | mulassd 11185 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท (2 ยท
๐ด)) ยท ๐ต) = (2 ยท ((2 ยท
๐ด) ยท ๐ต))) |
60 | 58, 59 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ ((4 ยท ๐ด) ยท ๐ต) = (2 ยท ((2 ยท ๐ด) ยท ๐ต))) |
61 | 60 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (((4 ยท ๐ด) ยท ๐ต) ยท ๐) = ((2 ยท ((2 ยท ๐ด) ยท ๐ต)) ยท ๐)) |
62 | 4, 7 | mulcld 11182 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐ด) ยท ๐ต) โ โ) |
63 | 55, 62, 5 | mulassd 11185 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ((2 ยท
๐ด) ยท ๐ต)) ยท ๐) = (2 ยท (((2 ยท ๐ด) ยท ๐ต) ยท ๐))) |
64 | 61, 63 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ (((4 ยท ๐ด) ยท ๐ต) ยท ๐) = (2 ยท (((2 ยท ๐ด) ยท ๐ต) ยท ๐))) |
65 | 22, 7, 5 | mulassd 11185 |
. . . . . . . . . . 11
โข (๐ โ (((4 ยท ๐ด) ยท ๐ต) ยท ๐) = ((4 ยท ๐ด) ยท (๐ต ยท ๐))) |
66 | 4, 7, 5 | mul32d 11372 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐ด) ยท ๐ต) ยท ๐) = (((2 ยท ๐ด) ยท ๐) ยท ๐ต)) |
67 | 66 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (((2 ยท
๐ด) ยท ๐ต) ยท ๐)) = (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) |
68 | 64, 65, 67 | 3eqtr3d 2785 |
. . . . . . . . . 10
โข (๐ โ ((4 ยท ๐ด) ยท (๐ต ยท ๐)) = (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) |
69 | 23, 2, 16 | mulassd 11185 |
. . . . . . . . . 10
โข (๐ โ ((4 ยท ๐ด) ยท ๐ถ) = (4 ยท (๐ด ยท ๐ถ))) |
70 | 68, 69 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ (((4 ยท ๐ด) ยท (๐ต ยท ๐)) + ((4 ยท ๐ด) ยท ๐ถ)) = ((2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)) + (4 ยท (๐ด ยท ๐ถ)))) |
71 | 52, 70 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((4 ยท ๐ด) ยท ((๐ต ยท ๐) + ๐ถ)) = ((2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)) + (4 ยท (๐ด ยท ๐ถ)))) |
72 | 51, 71 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ (((4 ยท ๐ด) ยท (๐ด ยท (๐โ2))) + ((4 ยท ๐ด) ยท ((๐ต ยท ๐) + ๐ถ))) = ((((2 ยท ๐ด) ยท ๐)โ2) + ((2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)) + (4 ยท (๐ด ยท ๐ถ))))) |
73 | 36, 39, 72 | 3eqtr4rd 2788 |
. . . . . 6
โข (๐ โ (((4 ยท ๐ด) ยท (๐ด ยท (๐โ2))) + ((4 ยท ๐ด) ยท ((๐ต ยท ๐) + ๐ถ))) = (((๐ตโ2) + ((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)))) โ ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ))))) |
74 | 22, 14, 17 | adddid 11186 |
. . . . . 6
โข (๐ โ ((4 ยท ๐ด) ยท ((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ))) = (((4 ยท ๐ด) ยท (๐ด ยท (๐โ2))) + ((4 ยท ๐ด) ยท ((๐ต ยท ๐) + ๐ถ)))) |
75 | | binom2 14128 |
. . . . . . . . 9
โข ((((2
ยท ๐ด) ยท ๐) โ โ โง ๐ต โ โ) โ ((((2
ยท ๐ด) ยท ๐) + ๐ต)โ2) = (((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) + (๐ตโ2))) |
76 | 6, 7, 75 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) = (((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))) + (๐ตโ2))) |
77 | 38, 37, 76 | comraddd 11376 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) = ((๐ตโ2) + ((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต))))) |
78 | | quad2.2 |
. . . . . . 7
โข (๐ โ (๐ทโ2) = ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) |
79 | 77, 78 | oveq12d 7380 |
. . . . . 6
โข (๐ โ (((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) โ (๐ทโ2)) = (((๐ตโ2) + ((((2 ยท ๐ด) ยท ๐)โ2) + (2 ยท (((2 ยท ๐ด) ยท ๐) ยท ๐ต)))) โ ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ))))) |
80 | 73, 74, 79 | 3eqtr4d 2787 |
. . . . 5
โข (๐ โ ((4 ยท ๐ด) ยท ((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ))) = (((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) โ (๐ทโ2))) |
81 | 22 | mul01d 11361 |
. . . . 5
โข (๐ โ ((4 ยท ๐ด) ยท 0) =
0) |
82 | 80, 81 | eqeq12d 2753 |
. . . 4
โข (๐ โ (((4 ยท ๐ด) ยท ((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ))) = ((4 ยท ๐ด) ยท 0) โ (((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) โ (๐ทโ2)) = 0)) |
83 | 28, 82 | bitr3d 281 |
. . 3
โข (๐ โ (((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ)) = 0 โ (((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) โ (๐ทโ2)) = 0)) |
84 | 6, 7 | subnegd 11526 |
. . . . 5
โข (๐ โ (((2 ยท ๐ด) ยท ๐) โ -๐ต) = (((2 ยท ๐ด) ยท ๐) + ๐ต)) |
85 | 84 | oveq1d 7377 |
. . . 4
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต)โ2) = ((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2)) |
86 | 85 | eqeq1d 2739 |
. . 3
โข (๐ โ (((((2 ยท ๐ด) ยท ๐) โ -๐ต)โ2) = (๐ทโ2) โ ((((2 ยท ๐ด) ยท ๐) + ๐ต)โ2) = (๐ทโ2))) |
87 | 12, 83, 86 | 3bitr4d 311 |
. 2
โข (๐ โ (((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ)) = 0 โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต)โ2) = (๐ทโ2))) |
88 | 7 | negcld 11506 |
. . . 4
โข (๐ โ -๐ต โ โ) |
89 | 6, 88 | subcld 11519 |
. . 3
โข (๐ โ (((2 ยท ๐ด) ยท ๐) โ -๐ต) โ โ) |
90 | | sqeqor 14127 |
. . 3
โข (((((2
ยท ๐ด) ยท ๐) โ -๐ต) โ โ โง ๐ท โ โ) โ (((((2 ยท
๐ด) ยท ๐) โ -๐ต)โ2) = (๐ทโ2) โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต) = ๐ท โจ (((2 ยท ๐ด) ยท ๐) โ -๐ต) = -๐ท))) |
91 | 89, 10, 90 | syl2anc 585 |
. 2
โข (๐ โ (((((2 ยท ๐ด) ยท ๐) โ -๐ต)โ2) = (๐ทโ2) โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต) = ๐ท โจ (((2 ยท ๐ด) ยท ๐) โ -๐ต) = -๐ท))) |
92 | 6, 88, 10 | subaddd 11537 |
. . . 4
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต) = ๐ท โ (-๐ต + ๐ท) = ((2 ยท ๐ด) ยท ๐))) |
93 | 88, 10 | addcld 11181 |
. . . . . 6
โข (๐ โ (-๐ต + ๐ท) โ โ) |
94 | | 2ne0 12264 |
. . . . . . . 8
โข 2 โ
0 |
95 | 94 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ 0) |
96 | 55, 2, 95, 26 | mulne0d 11814 |
. . . . . 6
โข (๐ โ (2 ยท ๐ด) โ 0) |
97 | 93, 4, 5, 96 | divmuld 11960 |
. . . . 5
โข (๐ โ (((-๐ต + ๐ท) / (2 ยท ๐ด)) = ๐ โ ((2 ยท ๐ด) ยท ๐) = (-๐ต + ๐ท))) |
98 | | eqcom 2744 |
. . . . 5
โข (๐ = ((-๐ต + ๐ท) / (2 ยท ๐ด)) โ ((-๐ต + ๐ท) / (2 ยท ๐ด)) = ๐) |
99 | | eqcom 2744 |
. . . . 5
โข ((-๐ต + ๐ท) = ((2 ยท ๐ด) ยท ๐) โ ((2 ยท ๐ด) ยท ๐) = (-๐ต + ๐ท)) |
100 | 97, 98, 99 | 3bitr4g 314 |
. . . 4
โข (๐ โ (๐ = ((-๐ต + ๐ท) / (2 ยท ๐ด)) โ (-๐ต + ๐ท) = ((2 ยท ๐ด) ยท ๐))) |
101 | 92, 100 | bitr4d 282 |
. . 3
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต) = ๐ท โ ๐ = ((-๐ต + ๐ท) / (2 ยท ๐ด)))) |
102 | 88, 10 | negsubd 11525 |
. . . . 5
โข (๐ โ (-๐ต + -๐ท) = (-๐ต โ ๐ท)) |
103 | 102 | eqeq1d 2739 |
. . . 4
โข (๐ โ ((-๐ต + -๐ท) = ((2 ยท ๐ด) ยท ๐) โ (-๐ต โ ๐ท) = ((2 ยท ๐ด) ยท ๐))) |
104 | 10 | negcld 11506 |
. . . . 5
โข (๐ โ -๐ท โ โ) |
105 | 6, 88, 104 | subaddd 11537 |
. . . 4
โข (๐ โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต) = -๐ท โ (-๐ต + -๐ท) = ((2 ยท ๐ด) ยท ๐))) |
106 | 88, 10 | subcld 11519 |
. . . . . 6
โข (๐ โ (-๐ต โ ๐ท) โ โ) |
107 | 106, 4, 5, 96 | divmuld 11960 |
. . . . 5
โข (๐ โ (((-๐ต โ ๐ท) / (2 ยท ๐ด)) = ๐ โ ((2 ยท ๐ด) ยท ๐) = (-๐ต โ ๐ท))) |
108 | | eqcom 2744 |
. . . . 5
โข (๐ = ((-๐ต โ ๐ท) / (2 ยท ๐ด)) โ ((-๐ต โ ๐ท) / (2 ยท ๐ด)) = ๐) |
109 | | eqcom 2744 |
. . . . 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 918 |
. 2
โข (๐ โ (((((2 ยท ๐ด) ยท ๐) โ -๐ต) = ๐ท โจ (((2 ยท ๐ด) ยท ๐) โ -๐ต) = -๐ท) โ (๐ = ((-๐ต + ๐ท) / (2 ยท ๐ด)) โจ ๐ = ((-๐ต โ ๐ท) / (2 ยท ๐ด))))) |
113 | 87, 91, 112 | 3bitrd 305 |
1
โข (๐ โ (((๐ด ยท (๐โ2)) + ((๐ต ยท ๐) + ๐ถ)) = 0 โ (๐ = ((-๐ต + ๐ท) / (2 ยท ๐ด)) โจ ๐ = ((-๐ต โ ๐ท) / (2 ยท ๐ด))))) |