Step | Hyp | Ref
| Expression |
1 | | dquart.x |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
2 | 1 | sqcld 14056 |
. . . . . 6
โข (๐ โ (๐โ2) โ โ) |
3 | | dquart.m |
. . . . . . . . 9
โข (๐ โ ๐ = ((2 ยท ๐)โ2)) |
4 | | 2cn 12235 |
. . . . . . . . . . 11
โข 2 โ
โ |
5 | | dquart.s |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
6 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) โ
โ) |
8 | 7 | sqcld 14056 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ2) โ
โ) |
9 | 3, 8 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
10 | | dquart.b |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
11 | 9, 10 | addcld 11181 |
. . . . . . 7
โข (๐ โ (๐ + ๐ต) โ โ) |
12 | 11 | halfcld 12405 |
. . . . . 6
โข (๐ โ ((๐ + ๐ต) / 2) โ โ) |
13 | 2, 12 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐โ2) + ((๐ + ๐ต) / 2)) โ โ) |
14 | 9 | halfcld 12405 |
. . . . . . . 8
โข (๐ โ (๐ / 2) โ โ) |
15 | 14, 1 | mulcld 11182 |
. . . . . . 7
โข (๐ โ ((๐ / 2) ยท ๐) โ โ) |
16 | | dquart.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ โ) |
17 | | 4cn 12245 |
. . . . . . . . 9
โข 4 โ
โ |
18 | 17 | a1i 11 |
. . . . . . . 8
โข (๐ โ 4 โ
โ) |
19 | | 4ne0 12268 |
. . . . . . . . 9
โข 4 โ
0 |
20 | 19 | a1i 11 |
. . . . . . . 8
โข (๐ โ 4 โ 0) |
21 | 16, 18, 20 | divcld 11938 |
. . . . . . 7
โข (๐ โ (๐ถ / 4) โ โ) |
22 | 15, 21 | subcld 11519 |
. . . . . 6
โข (๐ โ (((๐ / 2) ยท ๐) โ (๐ถ / 4)) โ โ) |
23 | | dquart.m0 |
. . . . . . . . . 10
โข (๐ โ ๐ โ 0) |
24 | 3, 23 | eqnetrrd 3013 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ2) โ
0) |
25 | | sqne0 14035 |
. . . . . . . . . 10
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐)โ2) โ 0 โ (2 ยท ๐) โ 0)) |
26 | 7, 25 | syl 17 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐)โ2) โ 0 โ (2
ยท ๐) โ
0)) |
27 | 24, 26 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (2 ยท ๐) โ 0) |
28 | | mulne0b 11803 |
. . . . . . . . 9
โข ((2
โ โ โง ๐
โ โ) โ ((2 โ 0 โง ๐ โ 0) โ (2 ยท ๐) โ 0)) |
29 | 4, 5, 28 | sylancr 588 |
. . . . . . . 8
โข (๐ โ ((2 โ 0 โง ๐ โ 0) โ (2 ยท
๐) โ
0)) |
30 | 27, 29 | mpbird 257 |
. . . . . . 7
โข (๐ โ (2 โ 0 โง ๐ โ 0)) |
31 | 30 | simprd 497 |
. . . . . 6
โข (๐ โ ๐ โ 0) |
32 | 22, 5, 31 | divcld 11938 |
. . . . 5
โข (๐ โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) โ โ) |
33 | 13, 32 | addcld 11181 |
. . . 4
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) โ โ) |
34 | 4 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
35 | | 2ne0 12264 |
. . . . 5
โข 2 โ
0 |
36 | 35 | a1i 11 |
. . . 4
โข (๐ โ 2 โ 0) |
37 | 33, 34, 36 | diveq0ad 11948 |
. . 3
โข (๐ โ (((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2) = 0 โ (((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0)) |
38 | 2, 12, 32 | addassd 11184 |
. . . . . 6
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = ((๐โ2) + (((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)))) |
39 | 38 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2) = (((๐โ2) + (((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐))) / 2)) |
40 | 12, 32 | addcld 11181 |
. . . . . 6
โข (๐ โ (((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) โ โ) |
41 | 2, 40, 34, 36 | divdird 11976 |
. . . . 5
โข (๐ โ (((๐โ2) + (((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐))) / 2) = (((๐โ2) / 2) + ((((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2))) |
42 | 2, 34, 36 | divrec2d 11942 |
. . . . . 6
โข (๐ โ ((๐โ2) / 2) = ((1 / 2) ยท (๐โ2))) |
43 | 15, 21, 5, 31 | divsubdird 11977 |
. . . . . . . . . . 11
โข (๐ โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) = ((((๐ / 2) ยท ๐) / ๐) โ ((๐ถ / 4) / ๐))) |
44 | 14, 1, 5, 31 | div23d 11975 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ / 2) ยท ๐) / ๐) = (((๐ / 2) / ๐) ยท ๐)) |
45 | 5 | sqvald 14055 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
46 | 45 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท (๐โ2)) = (2 ยท (๐ ยท ๐))) |
47 | | sqmul 14031 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((2
โ โ โง ๐
โ โ) โ ((2 ยท ๐)โ2) = ((2โ2) ยท (๐โ2))) |
48 | 4, 5, 47 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((2 ยท ๐)โ2) = ((2โ2) ยท
(๐โ2))) |
49 | 4 | sqvali 14091 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(2โ2) = (2 ยท 2) |
50 | 49 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((2โ2) ยท (๐โ2)) = ((2 ยท 2) ยท (๐โ2)) |
51 | 48, 50 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((2 ยท ๐)โ2) = ((2 ยท 2)
ยท (๐โ2))) |
52 | 5 | sqcld 14056 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐โ2) โ โ) |
53 | 34, 34, 52 | mulassd 11185 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((2 ยท 2) ยท
(๐โ2)) = (2 ยท
(2 ยท (๐โ2)))) |
54 | 3, 51, 53 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ = (2 ยท (2 ยท (๐โ2)))) |
55 | 54 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ / 2) = ((2 ยท (2 ยท (๐โ2))) /
2)) |
56 | | mulcl 11142 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
โ โ โง (๐โ2) โ โ) โ (2 ยท
(๐โ2)) โ
โ) |
57 | 4, 52, 56 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (2 ยท (๐โ2)) โ
โ) |
58 | 57, 34, 36 | divcan3d 11943 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2 ยท (2 ยท
(๐โ2))) / 2) = (2
ยท (๐โ2))) |
59 | 55, 58 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ / 2) = (2 ยท (๐โ2))) |
60 | 34, 5, 5 | mulassd 11185 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 ยท ๐) ยท ๐) = (2 ยท (๐ ยท ๐))) |
61 | 46, 59, 60 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ / 2) = ((2 ยท ๐) ยท ๐)) |
62 | 61 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ / 2) / ๐) = (((2 ยท ๐) ยท ๐) / ๐)) |
63 | 7, 5, 31 | divcan4d 11944 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท ๐) ยท ๐) / ๐) = (2 ยท ๐)) |
64 | 62, 63 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ / 2) / ๐) = (2 ยท ๐)) |
65 | 64 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ / 2) / ๐) ยท ๐) = ((2 ยท ๐) ยท ๐)) |
66 | 44, 65 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ / 2) ยท ๐) / ๐) = ((2 ยท ๐) ยท ๐)) |
67 | 66 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((((๐ / 2) ยท ๐) / ๐) โ ((๐ถ / 4) / ๐)) = (((2 ยท ๐) ยท ๐) โ ((๐ถ / 4) / ๐))) |
68 | 43, 67 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) = (((2 ยท ๐) ยท ๐) โ ((๐ถ / 4) / ๐))) |
69 | 68 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = (((๐ + ๐ต) / 2) + (((2 ยท ๐) ยท ๐) โ ((๐ถ / 4) / ๐)))) |
70 | 7, 1 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) ยท ๐) โ โ) |
71 | 21, 5, 31 | divcld 11938 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ / 4) / ๐) โ โ) |
72 | 12, 70, 71 | addsub12d 11542 |
. . . . . . . . 9
โข (๐ โ (((๐ + ๐ต) / 2) + (((2 ยท ๐) ยท ๐) โ ((๐ถ / 4) / ๐))) = (((2 ยท ๐) ยท ๐) + (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)))) |
73 | 69, 72 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = (((2 ยท ๐) ยท ๐) + (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)))) |
74 | 73 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2) = ((((2 ยท ๐) ยท ๐) + (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐))) / 2)) |
75 | 12, 71 | subcld 11519 |
. . . . . . . 8
โข (๐ โ (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)) โ โ) |
76 | 70, 75, 34, 36 | divdird 11976 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐) ยท ๐) + (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐))) / 2) = ((((2 ยท ๐) ยท ๐) / 2) + ((((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)) / 2))) |
77 | 34, 5, 1 | mulassd 11185 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) ยท ๐) = (2 ยท (๐ ยท ๐))) |
78 | 77 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) ยท ๐) / 2) = ((2 ยท (๐ ยท ๐)) / 2)) |
79 | 5, 1 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท ๐) โ โ) |
80 | 79, 34, 36 | divcan3d 11943 |
. . . . . . . . 9
โข (๐ โ ((2 ยท (๐ ยท ๐)) / 2) = (๐ ยท ๐)) |
81 | 78, 80 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) ยท ๐) / 2) = (๐ ยท ๐)) |
82 | 52 | negcld 11506 |
. . . . . . . . . . . 12
โข (๐ โ -(๐โ2) โ โ) |
83 | 10 | halfcld 12405 |
. . . . . . . . . . . 12
โข (๐ โ (๐ต / 2) โ โ) |
84 | 82, 83 | subcld 11519 |
. . . . . . . . . . 11
โข (๐ โ (-(๐โ2) โ (๐ต / 2)) โ โ) |
85 | 52, 84, 71 | subsub4d 11550 |
. . . . . . . . . 10
โข (๐ โ (((๐โ2) โ (-(๐โ2) โ (๐ต / 2))) โ ((๐ถ / 4) / ๐)) = ((๐โ2) โ ((-(๐โ2) โ (๐ต / 2)) + ((๐ถ / 4) / ๐)))) |
86 | 9, 10, 34, 36 | divdird 11976 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + ๐ต) / 2) = ((๐ / 2) + (๐ต / 2))) |
87 | 52 | 2timesd 12403 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท (๐โ2)) = ((๐โ2) + (๐โ2))) |
88 | 59, 87 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / 2) = ((๐โ2) + (๐โ2))) |
89 | 88 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ / 2) + (๐ต / 2)) = (((๐โ2) + (๐โ2)) + (๐ต / 2))) |
90 | 86, 89 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + ๐ต) / 2) = (((๐โ2) + (๐โ2)) + (๐ต / 2))) |
91 | 52, 52, 83 | addassd 11184 |
. . . . . . . . . . . 12
โข (๐ โ (((๐โ2) + (๐โ2)) + (๐ต / 2)) = ((๐โ2) + ((๐โ2) + (๐ต / 2)))) |
92 | 52, 83 | addcld 11181 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐โ2) + (๐ต / 2)) โ โ) |
93 | 52, 92 | subnegd 11526 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐โ2) โ -((๐โ2) + (๐ต / 2))) = ((๐โ2) + ((๐โ2) + (๐ต / 2)))) |
94 | 52, 83 | negdi2d 11533 |
. . . . . . . . . . . . . 14
โข (๐ โ -((๐โ2) + (๐ต / 2)) = (-(๐โ2) โ (๐ต / 2))) |
95 | 94 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐โ2) โ -((๐โ2) + (๐ต / 2))) = ((๐โ2) โ (-(๐โ2) โ (๐ต / 2)))) |
96 | 93, 95 | eqtr3d 2779 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) + ((๐โ2) + (๐ต / 2))) = ((๐โ2) โ (-(๐โ2) โ (๐ต / 2)))) |
97 | 90, 91, 96 | 3eqtrd 2781 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + ๐ต) / 2) = ((๐โ2) โ (-(๐โ2) โ (๐ต / 2)))) |
98 | 97 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)) = (((๐โ2) โ (-(๐โ2) โ (๐ต / 2))) โ ((๐ถ / 4) / ๐))) |
99 | | dquart.i2 |
. . . . . . . . . . 11
โข (๐ โ (๐ผโ2) = ((-(๐โ2) โ (๐ต / 2)) + ((๐ถ / 4) / ๐))) |
100 | 99 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ ((๐โ2) โ (๐ผโ2)) = ((๐โ2) โ ((-(๐โ2) โ (๐ต / 2)) + ((๐ถ / 4) / ๐)))) |
101 | 85, 98, 100 | 3eqtr4d 2787 |
. . . . . . . . 9
โข (๐ โ (((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)) = ((๐โ2) โ (๐ผโ2))) |
102 | 101 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ ((((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)) / 2) = (((๐โ2) โ (๐ผโ2)) / 2)) |
103 | 81, 102 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐) ยท ๐) / 2) + ((((๐ + ๐ต) / 2) โ ((๐ถ / 4) / ๐)) / 2)) = ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2))) |
104 | 74, 76, 103 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ ((((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2) = ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2))) |
105 | 42, 104 | oveq12d 7380 |
. . . . 5
โข (๐ โ (((๐โ2) / 2) + ((((๐ + ๐ต) / 2) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2)) = (((1 / 2) ยท (๐โ2)) + ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2)))) |
106 | 39, 41, 105 | 3eqtrd 2781 |
. . . 4
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2) = (((1 / 2) ยท (๐โ2)) + ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2)))) |
107 | 106 | eqeq1d 2739 |
. . 3
โข (๐ โ (((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) / 2) = 0 โ (((1 / 2) ยท (๐โ2)) + ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2))) = 0)) |
108 | 37, 107 | bitr3d 281 |
. 2
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0 โ (((1 / 2) ยท (๐โ2)) + ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2))) = 0)) |
109 | | ax-1cn 11116 |
. . . 4
โข 1 โ
โ |
110 | | halfcl 12385 |
. . . 4
โข (1 โ
โ โ (1 / 2) โ โ) |
111 | 109, 110 | mp1i 13 |
. . 3
โข (๐ โ (1 / 2) โ
โ) |
112 | | ax-1ne0 11127 |
. . . . 5
โข 1 โ
0 |
113 | 109, 4, 112, 35 | divne0i 11910 |
. . . 4
โข (1 / 2)
โ 0 |
114 | 113 | a1i 11 |
. . 3
โข (๐ โ (1 / 2) โ
0) |
115 | | dquart.i |
. . . . . 6
โข (๐ โ ๐ผ โ โ) |
116 | 115 | sqcld 14056 |
. . . . 5
โข (๐ โ (๐ผโ2) โ โ) |
117 | 52, 116 | subcld 11519 |
. . . 4
โข (๐ โ ((๐โ2) โ (๐ผโ2)) โ โ) |
118 | 117 | halfcld 12405 |
. . 3
โข (๐ โ (((๐โ2) โ (๐ผโ2)) / 2) โ
โ) |
119 | 109 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
120 | | 2cnne0 12370 |
. . . . . . . . . 10
โข (2 โ
โ โง 2 โ 0) |
121 | 120 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (2 โ โ โง 2
โ 0)) |
122 | | divmuldiv 11862 |
. . . . . . . . 9
โข (((1
โ โ โง ((๐โ2) โ (๐ผโ2)) โ โ) โง ((2 โ
โ โง 2 โ 0) โง (2 โ โ โง 2 โ 0))) โ ((1 /
2) ยท (((๐โ2)
โ (๐ผโ2)) / 2)) =
((1 ยท ((๐โ2)
โ (๐ผโ2))) / (2
ยท 2))) |
123 | 119, 117,
121, 121, 122 | syl22anc 838 |
. . . . . . . 8
โข (๐ โ ((1 / 2) ยท (((๐โ2) โ (๐ผโ2)) / 2)) = ((1 ยท
((๐โ2) โ (๐ผโ2))) / (2 ยท
2))) |
124 | 117 | mulid2d 11180 |
. . . . . . . . 9
โข (๐ โ (1 ยท ((๐โ2) โ (๐ผโ2))) = ((๐โ2) โ (๐ผโ2))) |
125 | | 2t2e4 12324 |
. . . . . . . . . 10
โข (2
ยท 2) = 4 |
126 | 125 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (2 ยท 2) =
4) |
127 | 124, 126 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ ((1 ยท ((๐โ2) โ (๐ผโ2))) / (2 ยท 2)) =
(((๐โ2) โ (๐ผโ2)) / 4)) |
128 | 123, 127 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ ((1 / 2) ยท (((๐โ2) โ (๐ผโ2)) / 2)) = (((๐โ2) โ (๐ผโ2)) / 4)) |
129 | 128 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (4 ยท ((1 / 2)
ยท (((๐โ2)
โ (๐ผโ2)) / 2)))
= (4 ยท (((๐โ2)
โ (๐ผโ2)) /
4))) |
130 | 117, 18, 20 | divcan2d 11940 |
. . . . . 6
โข (๐ โ (4 ยท (((๐โ2) โ (๐ผโ2)) / 4)) = ((๐โ2) โ (๐ผโ2))) |
131 | 129, 130 | eqtrd 2777 |
. . . . 5
โข (๐ โ (4 ยท ((1 / 2)
ยท (((๐โ2)
โ (๐ผโ2)) / 2)))
= ((๐โ2) โ
(๐ผโ2))) |
132 | 131 | oveq2d 7378 |
. . . 4
โข (๐ โ ((๐โ2) โ (4 ยท ((1 / 2)
ยท (((๐โ2)
โ (๐ผโ2)) / 2))))
= ((๐โ2) โ
((๐โ2) โ (๐ผโ2)))) |
133 | 52, 116 | nncand 11524 |
. . . 4
โข (๐ โ ((๐โ2) โ ((๐โ2) โ (๐ผโ2))) = (๐ผโ2)) |
134 | 132, 133 | eqtr2d 2778 |
. . 3
โข (๐ โ (๐ผโ2) = ((๐โ2) โ (4 ยท ((1 / 2)
ยท (((๐โ2)
โ (๐ผโ2)) /
2))))) |
135 | 111, 114,
5, 118, 1, 115, 134 | quad2 26205 |
. 2
โข (๐ โ ((((1 / 2) ยท (๐โ2)) + ((๐ ยท ๐) + (((๐โ2) โ (๐ผโ2)) / 2))) = 0 โ (๐ = ((-๐ + ๐ผ) / (2 ยท (1 / 2))) โจ ๐ = ((-๐ โ ๐ผ) / (2 ยท (1 /
2)))))) |
136 | 4, 35 | recidi 11893 |
. . . . . 6
โข (2
ยท (1 / 2)) = 1 |
137 | 136 | oveq2i 7373 |
. . . . 5
โข ((-๐ + ๐ผ) / (2 ยท (1 / 2))) = ((-๐ + ๐ผ) / 1) |
138 | 5 | negcld 11506 |
. . . . . . 7
โข (๐ โ -๐ โ โ) |
139 | 138, 115 | addcld 11181 |
. . . . . 6
โข (๐ โ (-๐ + ๐ผ) โ โ) |
140 | 139 | div1d 11930 |
. . . . 5
โข (๐ โ ((-๐ + ๐ผ) / 1) = (-๐ + ๐ผ)) |
141 | 137, 140 | eqtrid 2789 |
. . . 4
โข (๐ โ ((-๐ + ๐ผ) / (2 ยท (1 / 2))) = (-๐ + ๐ผ)) |
142 | 141 | eqeq2d 2748 |
. . 3
โข (๐ โ (๐ = ((-๐ + ๐ผ) / (2 ยท (1 / 2))) โ ๐ = (-๐ + ๐ผ))) |
143 | 136 | oveq2i 7373 |
. . . . 5
โข ((-๐ โ ๐ผ) / (2 ยท (1 / 2))) = ((-๐ โ ๐ผ) / 1) |
144 | 138, 115 | subcld 11519 |
. . . . . 6
โข (๐ โ (-๐ โ ๐ผ) โ โ) |
145 | 144 | div1d 11930 |
. . . . 5
โข (๐ โ ((-๐ โ ๐ผ) / 1) = (-๐ โ ๐ผ)) |
146 | 143, 145 | eqtrid 2789 |
. . . 4
โข (๐ โ ((-๐ โ ๐ผ) / (2 ยท (1 / 2))) = (-๐ โ ๐ผ)) |
147 | 146 | eqeq2d 2748 |
. . 3
โข (๐ โ (๐ = ((-๐ โ ๐ผ) / (2 ยท (1 / 2))) โ ๐ = (-๐ โ ๐ผ))) |
148 | 142, 147 | orbi12d 918 |
. 2
โข (๐ โ ((๐ = ((-๐ + ๐ผ) / (2 ยท (1 / 2))) โจ ๐ = ((-๐ โ ๐ผ) / (2 ยท (1 / 2)))) โ (๐ = (-๐ + ๐ผ) โจ ๐ = (-๐ โ ๐ผ)))) |
149 | 108, 135,
148 | 3bitrd 305 |
1
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0 โ (๐ = (-๐ + ๐ผ) โจ ๐ = (-๐ โ ๐ผ)))) |