Step | Hyp | Ref
| Expression |
1 | | dquart.x |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
2 | 1 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ โ) |
3 | | dquart.m |
. . . . . . . . . . 11
โข (๐ โ ๐ = ((2 ยท ๐)โ2)) |
4 | | 2cn 12235 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
5 | | dquart.s |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
6 | | mulcl 11142 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ
โ) |
8 | 7 | sqcld 14056 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐)โ2) โ
โ) |
9 | 3, 8 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
10 | | dquart.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
11 | 9, 10 | addcld 11181 |
. . . . . . . . 9
โข (๐ โ (๐ + ๐ต) โ โ) |
12 | 11 | halfcld 12405 |
. . . . . . . 8
โข (๐ โ ((๐ + ๐ต) / 2) โ โ) |
13 | | binom2 14128 |
. . . . . . . 8
โข (((๐โ2) โ โ โง
((๐ + ๐ต) / 2) โ โ) โ (((๐โ2) + ((๐ + ๐ต) / 2))โ2) = ((((๐โ2)โ2) + (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2)))) + (((๐ + ๐ต) / 2)โ2))) |
14 | 2, 12, 13 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2))โ2) = ((((๐โ2)โ2) + (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2)))) + (((๐ + ๐ต) / 2)โ2))) |
15 | | 2nn0 12437 |
. . . . . . . . . . . . 13
โข 2 โ
โ0 |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ0) |
17 | 1, 16, 16 | expmuld 14061 |
. . . . . . . . . . 11
โข (๐ โ (๐โ(2 ยท 2)) = ((๐โ2)โ2)) |
18 | | 2t2e4 12324 |
. . . . . . . . . . . 12
โข (2
ยท 2) = 4 |
19 | 18 | oveq2i 7373 |
. . . . . . . . . . 11
โข (๐โ(2 ยท 2)) = (๐โ4) |
20 | 17, 19 | eqtr3di 2792 |
. . . . . . . . . 10
โข (๐ โ ((๐โ2)โ2) = (๐โ4)) |
21 | 4 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
22 | 21, 2, 12 | mul12d 11371 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2))) = ((๐โ2) ยท (2 ยท ((๐ + ๐ต) / 2)))) |
23 | | 2ne0 12264 |
. . . . . . . . . . . . . . 15
โข 2 โ
0 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ 0) |
25 | 11, 21, 24 | divcan2d 11940 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท ((๐ + ๐ต) / 2)) = (๐ + ๐ต)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) ยท (2 ยท ((๐ + ๐ต) / 2))) = ((๐โ2) ยท (๐ + ๐ต))) |
27 | 2, 11 | mulcomd 11183 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) ยท (๐ + ๐ต)) = ((๐ + ๐ต) ยท (๐โ2))) |
28 | 26, 27 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ ((๐โ2) ยท (2 ยท ((๐ + ๐ต) / 2))) = ((๐ + ๐ต) ยท (๐โ2))) |
29 | 9, 10, 2 | adddird 11187 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + ๐ต) ยท (๐โ2)) = ((๐ ยท (๐โ2)) + (๐ต ยท (๐โ2)))) |
30 | 22, 28, 29 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2))) = ((๐ ยท (๐โ2)) + (๐ต ยท (๐โ2)))) |
31 | 20, 30 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ (((๐โ2)โ2) + (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2)))) = ((๐โ4) + ((๐ ยท (๐โ2)) + (๐ต ยท (๐โ2))))) |
32 | | 4nn0 12439 |
. . . . . . . . . . 11
โข 4 โ
โ0 |
33 | | expcl 13992 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 4 โ
โ0) โ (๐โ4) โ โ) |
34 | 1, 32, 33 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ (๐โ4) โ โ) |
35 | 9, 2 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท (๐โ2)) โ โ) |
36 | 10, 2 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ (๐ต ยท (๐โ2)) โ โ) |
37 | 34, 35, 36 | add12d 11388 |
. . . . . . . . 9
โข (๐ โ ((๐โ4) + ((๐ ยท (๐โ2)) + (๐ต ยท (๐โ2)))) = ((๐ ยท (๐โ2)) + ((๐โ4) + (๐ต ยท (๐โ2))))) |
38 | 31, 37 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((๐โ2)โ2) + (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2)))) = ((๐ ยท (๐โ2)) + ((๐โ4) + (๐ต ยท (๐โ2))))) |
39 | 38 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((((๐โ2)โ2) + (2 ยท ((๐โ2) ยท ((๐ + ๐ต) / 2)))) + (((๐ + ๐ต) / 2)โ2)) = (((๐ ยท (๐โ2)) + ((๐โ4) + (๐ต ยท (๐โ2)))) + (((๐ + ๐ต) / 2)โ2))) |
40 | 34, 36 | addcld 11181 |
. . . . . . . 8
โข (๐ โ ((๐โ4) + (๐ต ยท (๐โ2))) โ โ) |
41 | 12 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (((๐ + ๐ต) / 2)โ2) โ
โ) |
42 | 35, 40, 41 | addassd 11184 |
. . . . . . 7
โข (๐ โ (((๐ ยท (๐โ2)) + ((๐โ4) + (๐ต ยท (๐โ2)))) + (((๐ + ๐ต) / 2)โ2)) = ((๐ ยท (๐โ2)) + (((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)))) |
43 | 14, 39, 42 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2))โ2) = ((๐ ยท (๐โ2)) + (((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)))) |
44 | 9 | halfcld 12405 |
. . . . . . . . . . . 12
โข (๐ โ (๐ / 2) โ โ) |
45 | 44, 1 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ ((๐ / 2) ยท ๐) โ โ) |
46 | | dquart.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
47 | | 4cn 12245 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 4 โ
โ) |
49 | | 4ne0 12268 |
. . . . . . . . . . . . 13
โข 4 โ
0 |
50 | 49 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 4 โ 0) |
51 | 46, 48, 50 | divcld 11938 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ / 4) โ โ) |
52 | 45, 51 | subcld 11519 |
. . . . . . . . . 10
โข (๐ โ (((๐ / 2) ยท ๐) โ (๐ถ / 4)) โ โ) |
53 | | dquart.m0 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ 0) |
54 | 3, 53 | eqnetrrd 3013 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐)โ2) โ
0) |
55 | | sqne0 14035 |
. . . . . . . . . . . . . 14
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐)โ2) โ 0 โ (2 ยท ๐) โ 0)) |
56 | 7, 55 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท ๐)โ2) โ 0 โ (2
ยท ๐) โ
0)) |
57 | 54, 56 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ 0) |
58 | | mulne0b 11803 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง ๐
โ โ) โ ((2 โ 0 โง ๐ โ 0) โ (2 ยท ๐) โ 0)) |
59 | 4, 5, 58 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ ((2 โ 0 โง ๐ โ 0) โ (2 ยท
๐) โ
0)) |
60 | 57, 59 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ (2 โ 0 โง ๐ โ 0)) |
61 | 60 | simprd 497 |
. . . . . . . . . 10
โข (๐ โ ๐ โ 0) |
62 | 52, 5, 21, 61, 24 | divcan5d 11964 |
. . . . . . . . 9
โข (๐ โ ((2 ยท (((๐ / 2) ยท ๐) โ (๐ถ / 4))) / (2 ยท ๐)) = ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) |
63 | 21, 45, 51 | subdid 11618 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (((๐ / 2) ยท ๐) โ (๐ถ / 4))) = ((2 ยท ((๐ / 2) ยท ๐)) โ (2 ยท (๐ถ / 4)))) |
64 | 21, 44, 1 | mulassd 11185 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท (๐ / 2)) ยท ๐) = (2 ยท ((๐ / 2) ยท ๐))) |
65 | 9, 21, 24 | divcan2d 11940 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 ยท (๐ / 2)) = ๐) |
66 | 65 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท (๐ / 2)) ยท ๐) = (๐ ยท ๐)) |
67 | 64, 66 | eqtr3d 2779 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ((๐ / 2) ยท ๐)) = (๐ ยท ๐)) |
68 | 21, 46, 48, 50 | divassd 11973 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐ถ) / 4) = (2 ยท (๐ถ / 4))) |
69 | 18 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข ((2
ยท ๐ถ) / (2 ยท
2)) = ((2 ยท ๐ถ) /
4) |
70 | 46, 21, 21, 24, 24 | divcan5d 11964 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท ๐ถ) / (2 ยท 2)) = (๐ถ / 2)) |
71 | 69, 70 | eqtr3id 2791 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐ถ) / 4) = (๐ถ / 2)) |
72 | 68, 71 | eqtr3d 2779 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท (๐ถ / 4)) = (๐ถ / 2)) |
73 | 67, 72 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ((๐ / 2) ยท ๐)) โ (2 ยท (๐ถ / 4))) = ((๐ ยท ๐) โ (๐ถ / 2))) |
74 | 63, 73 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (2 ยท (((๐ / 2) ยท ๐) โ (๐ถ / 4))) = ((๐ ยท ๐) โ (๐ถ / 2))) |
75 | 74 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ ((2 ยท (((๐ / 2) ยท ๐) โ (๐ถ / 4))) / (2 ยท ๐)) = (((๐ ยท ๐) โ (๐ถ / 2)) / (2 ยท ๐))) |
76 | 62, 75 | eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) = (((๐ ยท ๐) โ (๐ถ / 2)) / (2 ยท ๐))) |
77 | 76 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)โ2) = ((((๐ ยท ๐) โ (๐ถ / 2)) / (2 ยท ๐))โ2)) |
78 | 9, 1 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (๐ ยท ๐) โ โ) |
79 | 46 | halfcld 12405 |
. . . . . . . . 9
โข (๐ โ (๐ถ / 2) โ โ) |
80 | 78, 79 | subcld 11519 |
. . . . . . . 8
โข (๐ โ ((๐ ยท ๐) โ (๐ถ / 2)) โ โ) |
81 | 80, 7, 57 | sqdivd 14071 |
. . . . . . 7
โข (๐ โ ((((๐ ยท ๐) โ (๐ถ / 2)) / (2 ยท ๐))โ2) = ((((๐ ยท ๐) โ (๐ถ / 2))โ2) / ((2 ยท ๐)โ2))) |
82 | 9 | sqcld 14056 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) โ โ) |
83 | 82, 2 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((๐โ2) ยท (๐โ2)) โ โ) |
84 | 78, 46 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐) ยท ๐ถ) โ โ) |
85 | 83, 84 | subcld 11519 |
. . . . . . . . 9
โข (๐ โ (((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) โ โ) |
86 | 46 | sqcld 14056 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ2) โ โ) |
87 | 86, 48, 50 | divcld 11938 |
. . . . . . . . 9
โข (๐ โ ((๐ถโ2) / 4) โ
โ) |
88 | 85, 87, 9, 53 | divdird 11976 |
. . . . . . . 8
โข (๐ โ (((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) + ((๐ถโ2) / 4)) / ๐) = (((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) / ๐) + (((๐ถโ2) / 4) / ๐))) |
89 | | binom2sub 14130 |
. . . . . . . . . . 11
โข (((๐ ยท ๐) โ โ โง (๐ถ / 2) โ โ) โ (((๐ ยท ๐) โ (๐ถ / 2))โ2) = ((((๐ ยท ๐)โ2) โ (2 ยท ((๐ ยท ๐) ยท (๐ถ / 2)))) + ((๐ถ / 2)โ2))) |
90 | 78, 79, 89 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ (((๐ ยท ๐) โ (๐ถ / 2))โ2) = ((((๐ ยท ๐)โ2) โ (2 ยท ((๐ ยท ๐) ยท (๐ถ / 2)))) + ((๐ถ / 2)โ2))) |
91 | 9, 1 | sqmuld 14070 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ๐)โ2) = ((๐โ2) ยท (๐โ2))) |
92 | 21, 78, 79 | mul12d 11371 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท ((๐ ยท ๐) ยท (๐ถ / 2))) = ((๐ ยท ๐) ยท (2 ยท (๐ถ / 2)))) |
93 | 46, 21, 24 | divcan2d 11940 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 ยท (๐ถ / 2)) = ๐ถ) |
94 | 93 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ ยท ๐) ยท (2 ยท (๐ถ / 2))) = ((๐ ยท ๐) ยท ๐ถ)) |
95 | 92, 94 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ((๐ ยท ๐) ยท (๐ถ / 2))) = ((๐ ยท ๐) ยท ๐ถ)) |
96 | 91, 95 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ โ (((๐ ยท ๐)โ2) โ (2 ยท ((๐ ยท ๐) ยท (๐ถ / 2)))) = (((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ))) |
97 | 46, 21, 24 | sqdivd 14071 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ / 2)โ2) = ((๐ถโ2) / (2โ2))) |
98 | | sq2 14108 |
. . . . . . . . . . . . 13
โข
(2โ2) = 4 |
99 | 98 | oveq2i 7373 |
. . . . . . . . . . . 12
โข ((๐ถโ2) / (2โ2)) = ((๐ถโ2) / 4) |
100 | 97, 99 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ / 2)โ2) = ((๐ถโ2) / 4)) |
101 | 96, 100 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ โ ((((๐ ยท ๐)โ2) โ (2 ยท ((๐ ยท ๐) ยท (๐ถ / 2)))) + ((๐ถ / 2)โ2)) = ((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) + ((๐ถโ2) / 4))) |
102 | 90, 101 | eqtr2d 2778 |
. . . . . . . . 9
โข (๐ โ ((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) + ((๐ถโ2) / 4)) = (((๐ ยท ๐) โ (๐ถ / 2))โ2)) |
103 | 102, 3 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ (((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) + ((๐ถโ2) / 4)) / ๐) = ((((๐ ยท ๐) โ (๐ถ / 2))โ2) / ((2 ยท ๐)โ2))) |
104 | 83, 84, 9, 53 | divsubdird 11977 |
. . . . . . . . . . 11
โข (๐ โ ((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) / ๐) = ((((๐โ2) ยท (๐โ2)) / ๐) โ (((๐ ยท ๐) ยท ๐ถ) / ๐))) |
105 | 82, 2, 9, 53 | div23d 11975 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐โ2) ยท (๐โ2)) / ๐) = (((๐โ2) / ๐) ยท (๐โ2))) |
106 | 9 | sqvald 14055 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
107 | 106 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐โ2) / ๐) = ((๐ ยท ๐) / ๐)) |
108 | 9, 9, 53 | divcan3d 11943 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ ยท ๐) / ๐) = ๐) |
109 | 107, 108 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐โ2) / ๐) = ๐) |
110 | 109 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐โ2) / ๐) ยท (๐โ2)) = (๐ ยท (๐โ2))) |
111 | 105, 110 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (((๐โ2) ยท (๐โ2)) / ๐) = (๐ ยท (๐โ2))) |
112 | 9, 1, 46 | mul32d 11372 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ ยท ๐) ยท ๐ถ) = ((๐ ยท ๐ถ) ยท ๐)) |
113 | 9, 46, 1 | mulassd 11185 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ ยท ๐ถ) ยท ๐) = (๐ ยท (๐ถ ยท ๐))) |
114 | 112, 113 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ ยท ๐) ยท ๐ถ) = (๐ ยท (๐ถ ยท ๐))) |
115 | 114 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ ยท ๐) ยท ๐ถ) / ๐) = ((๐ ยท (๐ถ ยท ๐)) / ๐)) |
116 | 46, 1 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ถ ยท ๐) โ โ) |
117 | 116, 9, 53 | divcan3d 11943 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ ยท (๐ถ ยท ๐)) / ๐) = (๐ถ ยท ๐)) |
118 | 115, 117 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ ยท ๐) ยท ๐ถ) / ๐) = (๐ถ ยท ๐)) |
119 | 111, 118 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ โ ((((๐โ2) ยท (๐โ2)) / ๐) โ (((๐ ยท ๐) ยท ๐ถ) / ๐)) = ((๐ ยท (๐โ2)) โ (๐ถ ยท ๐))) |
120 | 104, 119 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ ((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) / ๐) = ((๐ ยท (๐โ2)) โ (๐ถ ยท ๐))) |
121 | 120 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ (((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) / ๐) + (((๐ถโ2) / 4) / ๐)) = (((๐ ยท (๐โ2)) โ (๐ถ ยท ๐)) + (((๐ถโ2) / 4) / ๐))) |
122 | 87, 9, 53 | divcld 11938 |
. . . . . . . . . 10
โข (๐ โ (((๐ถโ2) / 4) / ๐) โ โ) |
123 | 35, 116, 122 | subsubd 11547 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท (๐โ2)) โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐))) = (((๐ ยท (๐โ2)) โ (๐ถ ยท ๐)) + (((๐ถโ2) / 4) / ๐))) |
124 | 121, 123 | eqtr4d 2780 |
. . . . . . . 8
โข (๐ โ (((((๐โ2) ยท (๐โ2)) โ ((๐ ยท ๐) ยท ๐ถ)) / ๐) + (((๐ถโ2) / 4) / ๐)) = ((๐ ยท (๐โ2)) โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)))) |
125 | 88, 103, 124 | 3eqtr3d 2785 |
. . . . . . 7
โข (๐ โ ((((๐ ยท ๐) โ (๐ถ / 2))โ2) / ((2 ยท ๐)โ2)) = ((๐ ยท (๐โ2)) โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)))) |
126 | 77, 81, 125 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ (((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)โ2) = ((๐ ยท (๐โ2)) โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)))) |
127 | 43, 126 | oveq12d 7380 |
. . . . 5
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2))โ2) โ (((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)โ2)) = (((๐ ยท (๐โ2)) + (((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2))) โ ((๐ ยท (๐โ2)) โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐))))) |
128 | 40, 41 | addcld 11181 |
. . . . . 6
โข (๐ โ (((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)) โ
โ) |
129 | 116, 122 | subcld 11519 |
. . . . . 6
โข (๐ โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)) โ โ) |
130 | 35, 128, 129 | pnncand 11558 |
. . . . 5
โข (๐ โ (((๐ ยท (๐โ2)) + (((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2))) โ ((๐ ยท (๐โ2)) โ ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)))) = ((((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)) + ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)))) |
131 | 122 | negcld 11506 |
. . . . . . 7
โข (๐ โ -(((๐ถโ2) / 4) / ๐) โ โ) |
132 | 40, 41, 116, 131 | add4d 11390 |
. . . . . 6
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)) + ((๐ถ ยท ๐) + -(((๐ถโ2) / 4) / ๐))) = ((((๐โ4) + (๐ต ยท (๐โ2))) + (๐ถ ยท ๐)) + ((((๐ + ๐ต) / 2)โ2) + -(((๐ถโ2) / 4) / ๐)))) |
133 | 116, 122 | negsubd 11525 |
. . . . . . 7
โข (๐ โ ((๐ถ ยท ๐) + -(((๐ถโ2) / 4) / ๐)) = ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐))) |
134 | 133 | oveq2d 7378 |
. . . . . 6
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)) + ((๐ถ ยท ๐) + -(((๐ถโ2) / 4) / ๐))) = ((((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)) + ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐)))) |
135 | 41, 122 | negsubd 11525 |
. . . . . . . . 9
โข (๐ โ ((((๐ + ๐ต) / 2)โ2) + -(((๐ถโ2) / 4) / ๐)) = ((((๐ + ๐ต) / 2)โ2) โ (((๐ถโ2) / 4) / ๐))) |
136 | | dquart.i |
. . . . . . . . . 10
โข (๐ โ ๐ผ โ โ) |
137 | | dquart.i2 |
. . . . . . . . . 10
โข (๐ โ (๐ผโ2) = ((-(๐โ2) โ (๐ต / 2)) + ((๐ถ / 4) / ๐))) |
138 | | dquart.d |
. . . . . . . . . 10
โข (๐ โ ๐ท โ โ) |
139 | | dquart.3 |
. . . . . . . . . 10
โข (๐ โ (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐) + -(๐ถโ2))) = 0) |
140 | 10, 46, 1, 5, 3, 53,
136, 137, 138, 139 | dquartlem2 26218 |
. . . . . . . . 9
โข (๐ โ ((((๐ + ๐ต) / 2)โ2) โ (((๐ถโ2) / 4) / ๐)) = ๐ท) |
141 | 135, 140 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((((๐ + ๐ต) / 2)โ2) + -(((๐ถโ2) / 4) / ๐)) = ๐ท) |
142 | 141 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + (๐ถ ยท ๐)) + ((((๐ + ๐ต) / 2)โ2) + -(((๐ถโ2) / 4) / ๐))) = ((((๐โ4) + (๐ต ยท (๐โ2))) + (๐ถ ยท ๐)) + ๐ท)) |
143 | 40, 116, 138 | addassd 11184 |
. . . . . . 7
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + (๐ถ ยท ๐)) + ๐ท) = (((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท))) |
144 | 142, 143 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + (๐ถ ยท ๐)) + ((((๐ + ๐ต) / 2)โ2) + -(((๐ถโ2) / 4) / ๐))) = (((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท))) |
145 | 132, 134,
144 | 3eqtr3d 2785 |
. . . . 5
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + (((๐ + ๐ต) / 2)โ2)) + ((๐ถ ยท ๐) โ (((๐ถโ2) / 4) / ๐))) = (((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท))) |
146 | 127, 130,
145 | 3eqtrd 2781 |
. . . 4
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2))โ2) โ (((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)โ2)) = (((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท))) |
147 | 2, 12 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐โ2) + ((๐ + ๐ต) / 2)) โ โ) |
148 | 52, 5, 61 | divcld 11938 |
. . . . 5
โข (๐ โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) โ โ) |
149 | | subsq 14121 |
. . . . 5
โข ((((๐โ2) + ((๐ + ๐ต) / 2)) โ โ โง ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) โ โ) โ ((((๐โ2) + ((๐ + ๐ต) / 2))โ2) โ (((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)โ2)) = ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) ยท (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)))) |
150 | 147, 148,
149 | syl2anc 585 |
. . . 4
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2))โ2) โ (((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)โ2)) = ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) ยท (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)))) |
151 | 146, 150 | eqtr3d 2779 |
. . 3
โข (๐ โ (((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) ยท (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)))) |
152 | 151 | eqeq1d 2739 |
. 2
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0 โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) ยท (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐))) = 0)) |
153 | 147, 148 | addcld 11181 |
. . 3
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) โ โ) |
154 | 147, 148 | subcld 11519 |
. . 3
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) โ โ) |
155 | 153, 154 | mul0ord 11812 |
. 2
โข (๐ โ (((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) ยท (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐))) = 0 โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0 โจ (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0))) |
156 | 10, 46, 1, 5, 3, 53,
136, 137 | dquartlem1 26217 |
. . 3
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0 โ (๐ = (-๐ + ๐ผ) โจ ๐ = (-๐ โ ๐ผ)))) |
157 | 5 | negcld 11506 |
. . . . 5
โข (๐ โ -๐ โ โ) |
158 | | sqneg 14028 |
. . . . . . . 8
โข ((2
ยท ๐) โ โ
โ (-(2 ยท ๐)โ2) = ((2 ยท ๐)โ2)) |
159 | 7, 158 | syl 17 |
. . . . . . 7
โข (๐ โ (-(2 ยท ๐)โ2) = ((2 ยท ๐)โ2)) |
160 | 3, 159 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ ๐ = (-(2 ยท ๐)โ2)) |
161 | | mulneg2 11599 |
. . . . . . . 8
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท -๐) = -(2 ยท ๐)) |
162 | 4, 5, 161 | sylancr 588 |
. . . . . . 7
โข (๐ โ (2 ยท -๐) = -(2 ยท ๐)) |
163 | 162 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((2 ยท -๐)โ2) = (-(2 ยท ๐)โ2)) |
164 | 160, 163 | eqtr4d 2780 |
. . . . 5
โข (๐ โ ๐ = ((2 ยท -๐)โ2)) |
165 | | dquart.j |
. . . . 5
โข (๐ โ ๐ฝ โ โ) |
166 | | dquart.j2 |
. . . . . 6
โข (๐ โ (๐ฝโ2) = ((-(๐โ2) โ (๐ต / 2)) โ ((๐ถ / 4) / ๐))) |
167 | 5 | sqcld 14056 |
. . . . . . . . 9
โข (๐ โ (๐โ2) โ โ) |
168 | 167 | negcld 11506 |
. . . . . . . 8
โข (๐ โ -(๐โ2) โ โ) |
169 | 10 | halfcld 12405 |
. . . . . . . 8
โข (๐ โ (๐ต / 2) โ โ) |
170 | 168, 169 | subcld 11519 |
. . . . . . 7
โข (๐ โ (-(๐โ2) โ (๐ต / 2)) โ โ) |
171 | 51, 5, 61 | divcld 11938 |
. . . . . . 7
โข (๐ โ ((๐ถ / 4) / ๐) โ โ) |
172 | 170, 171 | negsubd 11525 |
. . . . . 6
โข (๐ โ ((-(๐โ2) โ (๐ต / 2)) + -((๐ถ / 4) / ๐)) = ((-(๐โ2) โ (๐ต / 2)) โ ((๐ถ / 4) / ๐))) |
173 | | sqneg 14028 |
. . . . . . . . . . 11
โข (๐ โ โ โ (-๐โ2) = (๐โ2)) |
174 | 5, 173 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (-๐โ2) = (๐โ2)) |
175 | 174 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ (๐โ2) = (-๐โ2)) |
176 | 175 | negeqd 11402 |
. . . . . . . 8
โข (๐ โ -(๐โ2) = -(-๐โ2)) |
177 | 176 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (-(๐โ2) โ (๐ต / 2)) = (-(-๐โ2) โ (๐ต / 2))) |
178 | 51, 5, 61 | divneg2d 11952 |
. . . . . . 7
โข (๐ โ -((๐ถ / 4) / ๐) = ((๐ถ / 4) / -๐)) |
179 | 177, 178 | oveq12d 7380 |
. . . . . 6
โข (๐ โ ((-(๐โ2) โ (๐ต / 2)) + -((๐ถ / 4) / ๐)) = ((-(-๐โ2) โ (๐ต / 2)) + ((๐ถ / 4) / -๐))) |
180 | 166, 172,
179 | 3eqtr2d 2783 |
. . . . 5
โข (๐ โ (๐ฝโ2) = ((-(-๐โ2) โ (๐ต / 2)) + ((๐ถ / 4) / -๐))) |
181 | 10, 46, 1, 157, 164, 53, 165, 180 | dquartlem1 26217 |
. . . 4
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / -๐)) = 0 โ (๐ = (--๐ + ๐ฝ) โจ ๐ = (--๐ โ ๐ฝ)))) |
182 | 52, 5, 61 | divneg2d 11952 |
. . . . . . 7
โข (๐ โ -((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐) = ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / -๐)) |
183 | 182 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) + -((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = (((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / -๐))) |
184 | 147, 148 | negsubd 11525 |
. . . . . 6
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) + -((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐))) |
185 | 183, 184 | eqtr3d 2779 |
. . . . 5
โข (๐ โ (((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / -๐)) = (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐))) |
186 | 185 | eqeq1d 2739 |
. . . 4
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / -๐)) = 0 โ (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0)) |
187 | 5 | negnegd 11510 |
. . . . . . 7
โข (๐ โ --๐ = ๐) |
188 | 187 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (--๐ + ๐ฝ) = (๐ + ๐ฝ)) |
189 | 188 | eqeq2d 2748 |
. . . . 5
โข (๐ โ (๐ = (--๐ + ๐ฝ) โ ๐ = (๐ + ๐ฝ))) |
190 | 187 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (--๐ โ ๐ฝ) = (๐ โ ๐ฝ)) |
191 | 190 | eqeq2d 2748 |
. . . . 5
โข (๐ โ (๐ = (--๐ โ ๐ฝ) โ ๐ = (๐ โ ๐ฝ))) |
192 | 189, 191 | orbi12d 918 |
. . . 4
โข (๐ โ ((๐ = (--๐ + ๐ฝ) โจ ๐ = (--๐ โ ๐ฝ)) โ (๐ = (๐ + ๐ฝ) โจ ๐ = (๐ โ ๐ฝ)))) |
193 | 181, 186,
192 | 3bitr3d 309 |
. . 3
โข (๐ โ ((((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0 โ (๐ = (๐ + ๐ฝ) โจ ๐ = (๐ โ ๐ฝ)))) |
194 | 156, 193 | orbi12d 918 |
. 2
โข (๐ โ (((((๐โ2) + ((๐ + ๐ต) / 2)) + ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0 โจ (((๐โ2) + ((๐ + ๐ต) / 2)) โ ((((๐ / 2) ยท ๐) โ (๐ถ / 4)) / ๐)) = 0) โ ((๐ = (-๐ + ๐ผ) โจ ๐ = (-๐ โ ๐ผ)) โจ (๐ = (๐ + ๐ฝ) โจ ๐ = (๐ โ ๐ฝ))))) |
195 | 152, 155,
194 | 3bitrd 305 |
1
โข (๐ โ ((((๐โ4) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0 โ ((๐ = (-๐ + ๐ผ) โจ ๐ = (-๐ โ ๐ผ)) โจ (๐ = (๐ + ๐ฝ) โจ ๐ = (๐ โ ๐ฝ))))) |