Step | Hyp | Ref
| Expression |
1 | | quad1.a |
. . . . 5
โข (๐ โ ๐ด โ โ) |
2 | 1 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ โ) |
3 | | quad1.z |
. . . . 5
โข (๐ โ ๐ด โ 0) |
4 | 3 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ 0) |
5 | | quad1.b |
. . . . 5
โข (๐ โ ๐ต โ โ) |
6 | 5 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ต โ โ) |
7 | | quad1.c |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
8 | 7 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ถ โ โ) |
9 | | simpr 486 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
10 | | quad1.d |
. . . . 5
โข (๐ โ ๐ท = ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) |
11 | 10 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ท = ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) |
12 | 2, 4, 6, 8, 9, 11 | quad 26345 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ (((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))))) |
13 | 12 | reubidva 3393 |
. 2
โข (๐ โ (โ!๐ฅ โ โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ โ!๐ฅ โ โ (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))))) |
14 | 5 | negcld 11558 |
. . . . 5
โข (๐ โ -๐ต โ โ) |
15 | 5 | sqcld 14109 |
. . . . . . . 8
โข (๐ โ (๐ตโ2) โ โ) |
16 | | 4cn 12297 |
. . . . . . . . . 10
โข 4 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 4 โ
โ) |
18 | 1, 7 | mulcld 11234 |
. . . . . . . . 9
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
19 | 17, 18 | mulcld 11234 |
. . . . . . . 8
โข (๐ โ (4 ยท (๐ด ยท ๐ถ)) โ โ) |
20 | 15, 19 | subcld 11571 |
. . . . . . 7
โข (๐ โ ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ))) โ โ) |
21 | 10, 20 | eqeltrd 2834 |
. . . . . 6
โข (๐ โ ๐ท โ โ) |
22 | 21 | sqrtcld 15384 |
. . . . 5
โข (๐ โ (โโ๐ท) โ
โ) |
23 | 14, 22 | addcld 11233 |
. . . 4
โข (๐ โ (-๐ต + (โโ๐ท)) โ โ) |
24 | | 2cnd 12290 |
. . . . 5
โข (๐ โ 2 โ
โ) |
25 | 24, 1 | mulcld 11234 |
. . . 4
โข (๐ โ (2 ยท ๐ด) โ
โ) |
26 | | 2ne0 12316 |
. . . . . 6
โข 2 โ
0 |
27 | 26 | a1i 11 |
. . . . 5
โข (๐ โ 2 โ 0) |
28 | 24, 1, 27, 3 | mulne0d 11866 |
. . . 4
โข (๐ โ (2 ยท ๐ด) โ 0) |
29 | 23, 25, 28 | divcld 11990 |
. . 3
โข (๐ โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
30 | 14, 22 | subcld 11571 |
. . . 4
โข (๐ โ (-๐ต โ (โโ๐ท)) โ โ) |
31 | 30, 25, 28 | divcld 11990 |
. . 3
โข (๐ โ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
32 | | euoreqb 45817 |
. . 3
โข
((((-๐ต +
(โโ๐ท)) / (2
ยท ๐ด)) โ โ
โง ((-๐ต โ
(โโ๐ท)) / (2
ยท ๐ด)) โ
โ) โ (โ!๐ฅ
โ โ (๐ฅ =
((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)))) |
33 | 29, 31, 32 | syl2anc 585 |
. 2
โข (๐ โ (โ!๐ฅ โ โ (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)))) |
34 | 14, 22, 25, 28 | divdird 12028 |
. . . 4
โข (๐ โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต / (2 ยท ๐ด)) + ((โโ๐ท) / (2 ยท ๐ด)))) |
35 | 14, 22, 25, 28 | divsubdird 12029 |
. . . . 5
โข (๐ โ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต / (2 ยท ๐ด)) โ ((โโ๐ท) / (2 ยท ๐ด)))) |
36 | 14, 25, 28 | divcld 11990 |
. . . . . 6
โข (๐ โ (-๐ต / (2 ยท ๐ด)) โ โ) |
37 | 22, 25, 28 | divcld 11990 |
. . . . . 6
โข (๐ โ ((โโ๐ท) / (2 ยท ๐ด)) โ
โ) |
38 | 36, 37 | negsubd 11577 |
. . . . 5
โข (๐ โ ((-๐ต / (2 ยท ๐ด)) + -((โโ๐ท) / (2 ยท ๐ด))) = ((-๐ต / (2 ยท ๐ด)) โ ((โโ๐ท) / (2 ยท ๐ด)))) |
39 | 22, 25, 28 | divnegd 12003 |
. . . . . 6
โข (๐ โ -((โโ๐ท) / (2 ยท ๐ด)) = (-(โโ๐ท) / (2 ยท ๐ด))) |
40 | 39 | oveq2d 7425 |
. . . . 5
โข (๐ โ ((-๐ต / (2 ยท ๐ด)) + -((โโ๐ท) / (2 ยท ๐ด))) = ((-๐ต / (2 ยท ๐ด)) + (-(โโ๐ท) / (2 ยท ๐ด)))) |
41 | 35, 38, 40 | 3eqtr2d 2779 |
. . . 4
โข (๐ โ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต / (2 ยท ๐ด)) + (-(โโ๐ท) / (2 ยท ๐ด)))) |
42 | 34, 41 | eqeq12d 2749 |
. . 3
โข (๐ โ (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ ((-๐ต / (2 ยท ๐ด)) + ((โโ๐ท) / (2 ยท ๐ด))) = ((-๐ต / (2 ยท ๐ด)) + (-(โโ๐ท) / (2 ยท ๐ด))))) |
43 | 22 | negcld 11558 |
. . . . . 6
โข (๐ โ -(โโ๐ท) โ
โ) |
44 | 43, 25, 28 | divcld 11990 |
. . . . 5
โข (๐ โ (-(โโ๐ท) / (2 ยท ๐ด)) โ
โ) |
45 | 36, 37, 44 | addcand 11417 |
. . . 4
โข (๐ โ (((-๐ต / (2 ยท ๐ด)) + ((โโ๐ท) / (2 ยท ๐ด))) = ((-๐ต / (2 ยท ๐ด)) + (-(โโ๐ท) / (2 ยท ๐ด))) โ ((โโ๐ท) / (2 ยท ๐ด)) = (-(โโ๐ท) / (2 ยท ๐ด)))) |
46 | | div11 11900 |
. . . . 5
โข
(((โโ๐ท)
โ โ โง -(โโ๐ท) โ โ โง ((2 ยท ๐ด) โ โ โง (2
ยท ๐ด) โ 0)) โ
(((โโ๐ท) / (2
ยท ๐ด)) =
(-(โโ๐ท) / (2
ยท ๐ด)) โ
(โโ๐ท) =
-(โโ๐ท))) |
47 | 22, 43, 25, 28, 46 | syl112anc 1375 |
. . . 4
โข (๐ โ (((โโ๐ท) / (2 ยท ๐ด)) = (-(โโ๐ท) / (2 ยท ๐ด)) โ (โโ๐ท) = -(โโ๐ท))) |
48 | 22 | eqnegd 11935 |
. . . . 5
โข (๐ โ ((โโ๐ท) = -(โโ๐ท) โ (โโ๐ท) = 0)) |
49 | | cnsqrt00 15339 |
. . . . . 6
โข (๐ท โ โ โ
((โโ๐ท) = 0
โ ๐ท =
0)) |
50 | 21, 49 | syl 17 |
. . . . 5
โข (๐ โ ((โโ๐ท) = 0 โ ๐ท = 0)) |
51 | 48, 50 | bitrd 279 |
. . . 4
โข (๐ โ ((โโ๐ท) = -(โโ๐ท) โ ๐ท = 0)) |
52 | 45, 47, 51 | 3bitrd 305 |
. . 3
โข (๐ โ (((-๐ต / (2 ยท ๐ด)) + ((โโ๐ท) / (2 ยท ๐ด))) = ((-๐ต / (2 ยท ๐ด)) + (-(โโ๐ท) / (2 ยท ๐ด))) โ ๐ท = 0)) |
53 | 42, 52 | bitrd 279 |
. 2
โข (๐ โ (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ ๐ท = 0)) |
54 | 13, 33, 53 | 3bitrd 305 |
1
โข (๐ โ (โ!๐ฅ โ โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ ๐ท = 0)) |