Step | Hyp | Ref
| Expression |
1 | | dquart.m |
. . . . . . 7
โข (๐ โ ๐ = ((2 ยท ๐)โ2)) |
2 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
3 | | dquart.s |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
4 | | mulcl 11142 |
. . . . . . . . 9
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (2 ยท ๐) โ
โ) |
6 | 5 | sqcld 14056 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐)โ2) โ
โ) |
7 | 1, 6 | eqeltrd 2838 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
8 | | dquart.b |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
9 | 7, 8 | addcld 11181 |
. . . . 5
โข (๐ โ (๐ + ๐ต) โ โ) |
10 | 2 | a1i 11 |
. . . . 5
โข (๐ โ 2 โ
โ) |
11 | | 2ne0 12264 |
. . . . . 6
โข 2 โ
0 |
12 | 11 | a1i 11 |
. . . . 5
โข (๐ โ 2 โ 0) |
13 | 9, 10, 12 | sqdivd 14071 |
. . . 4
โข (๐ โ (((๐ + ๐ต) / 2)โ2) = (((๐ + ๐ต)โ2) / (2โ2))) |
14 | | sq2 14108 |
. . . . 5
โข
(2โ2) = 4 |
15 | 14 | oveq2i 7373 |
. . . 4
โข (((๐ + ๐ต)โ2) / (2โ2)) = (((๐ + ๐ต)โ2) / 4) |
16 | 13, 15 | eqtrdi 2793 |
. . 3
โข (๐ โ (((๐ + ๐ต) / 2)โ2) = (((๐ + ๐ต)โ2) / 4)) |
17 | 16 | oveq1d 7377 |
. 2
โข (๐ โ ((((๐ + ๐ต) / 2)โ2) โ (((๐ถโ2) / 4) / ๐)) = ((((๐ + ๐ต)โ2) / 4) โ (((๐ถโ2) / 4) / ๐))) |
18 | 9 | sqcld 14056 |
. . . . 5
โข (๐ โ ((๐ + ๐ต)โ2) โ โ) |
19 | | 4cn 12245 |
. . . . . 6
โข 4 โ
โ |
20 | 19 | a1i 11 |
. . . . 5
โข (๐ โ 4 โ
โ) |
21 | | 4ne0 12268 |
. . . . . 6
โข 4 โ
0 |
22 | 21 | a1i 11 |
. . . . 5
โข (๐ โ 4 โ 0) |
23 | 18, 20, 22 | divcld 11938 |
. . . 4
โข (๐ โ (((๐ + ๐ต)โ2) / 4) โ
โ) |
24 | | dquart.c |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
25 | 24 | sqcld 14056 |
. . . . . 6
โข (๐ โ (๐ถโ2) โ โ) |
26 | 25, 20, 22 | divcld 11938 |
. . . . 5
โข (๐ โ ((๐ถโ2) / 4) โ
โ) |
27 | | dquart.m0 |
. . . . 5
โข (๐ โ ๐ โ 0) |
28 | 26, 7, 27 | divcld 11938 |
. . . 4
โข (๐ โ (((๐ถโ2) / 4) / ๐) โ โ) |
29 | 23, 28 | subcld 11519 |
. . 3
โข (๐ โ ((((๐ + ๐ต)โ2) / 4) โ (((๐ถโ2) / 4) / ๐)) โ โ) |
30 | | dquart.d |
. . 3
โข (๐ โ ๐ท โ โ) |
31 | 23, 28, 7 | subdird 11619 |
. . . 4
โข (๐ โ (((((๐ + ๐ต)โ2) / 4) โ (((๐ถโ2) / 4) / ๐)) ยท ๐) = (((((๐ + ๐ต)โ2) / 4) ยท ๐) โ ((((๐ถโ2) / 4) / ๐) ยท ๐))) |
32 | 18, 7, 20, 22 | div23d 11975 |
. . . . . 6
โข (๐ โ ((((๐ + ๐ต)โ2) ยท ๐) / 4) = ((((๐ + ๐ต)โ2) / 4) ยท ๐)) |
33 | 32 | eqcomd 2743 |
. . . . 5
โข (๐ โ ((((๐ + ๐ต)โ2) / 4) ยท ๐) = ((((๐ + ๐ต)โ2) ยท ๐) / 4)) |
34 | 26, 7, 27 | divcan1d 11939 |
. . . . 5
โข (๐ โ ((((๐ถโ2) / 4) / ๐) ยท ๐) = ((๐ถโ2) / 4)) |
35 | 33, 34 | oveq12d 7380 |
. . . 4
โข (๐ โ (((((๐ + ๐ต)โ2) / 4) ยท ๐) โ ((((๐ถโ2) / 4) / ๐) ยท ๐)) = (((((๐ + ๐ต)โ2) ยท ๐) / 4) โ ((๐ถโ2) / 4))) |
36 | | binom2 14128 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ต โ โ) โ ((๐ + ๐ต)โ2) = (((๐โ2) + (2 ยท (๐ ยท ๐ต))) + (๐ตโ2))) |
37 | 7, 8, 36 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + ๐ต)โ2) = (((๐โ2) + (2 ยท (๐ ยท ๐ต))) + (๐ตโ2))) |
38 | 37 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + ๐ต)โ2) ยท ๐) = ((((๐โ2) + (2 ยท (๐ ยท ๐ต))) + (๐ตโ2)) ยท ๐)) |
39 | 7 | sqcld 14056 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โ2) โ โ) |
40 | 7, 8 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท ๐ต) โ โ) |
41 | | mulcl 11142 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง (๐
ยท ๐ต) โ โ)
โ (2 ยท (๐
ยท ๐ต)) โ
โ) |
42 | 2, 40, 41 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท (๐ ยท ๐ต)) โ โ) |
43 | 39, 42 | addcld 11181 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) + (2 ยท (๐ ยท ๐ต))) โ โ) |
44 | 8 | sqcld 14056 |
. . . . . . . . . . . 12
โข (๐ โ (๐ตโ2) โ โ) |
45 | 43, 44, 7 | adddird 11187 |
. . . . . . . . . . 11
โข (๐ โ ((((๐โ2) + (2 ยท (๐ ยท ๐ต))) + (๐ตโ2)) ยท ๐) = ((((๐โ2) + (2 ยท (๐ ยท ๐ต))) ยท ๐) + ((๐ตโ2) ยท ๐))) |
46 | 39, 42, 7 | adddird 11187 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐โ2) + (2 ยท (๐ ยท ๐ต))) ยท ๐) = (((๐โ2) ยท ๐) + ((2 ยท (๐ ยท ๐ต)) ยท ๐))) |
47 | | df-3 12224 |
. . . . . . . . . . . . . . . 16
โข 3 = (2 +
1) |
48 | 47 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
โข (๐โ3) = (๐โ(2 + 1)) |
49 | | 2nn0 12437 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ0 |
50 | | expp1 13981 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง 2 โ
โ0) โ (๐โ(2 + 1)) = ((๐โ2) ยท ๐)) |
51 | 7, 49, 50 | sylancl 587 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐โ(2 + 1)) = ((๐โ2) ยท ๐)) |
52 | 48, 51 | eqtr2id 2790 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐โ2) ยท ๐) = (๐โ3)) |
53 | | mulcl 11142 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐ต
โ โ) โ (2 ยท ๐ต) โ โ) |
54 | 2, 8, 53 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 ยท ๐ต) โ
โ) |
55 | 54, 7, 7 | mulassd 11185 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท ๐ต) ยท ๐) ยท ๐) = ((2 ยท ๐ต) ยท (๐ ยท ๐))) |
56 | 10, 7, 8 | mulassd 11185 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 ยท ๐) ยท ๐ต) = (2 ยท (๐ ยท ๐ต))) |
57 | 10, 7, 8 | mul32d 11372 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 ยท ๐) ยท ๐ต) = ((2 ยท ๐ต) ยท ๐)) |
58 | 56, 57 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 ยท (๐ ยท ๐ต)) = ((2 ยท ๐ต) ยท ๐)) |
59 | 58 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท (๐ ยท ๐ต)) ยท ๐) = (((2 ยท ๐ต) ยท ๐) ยท ๐)) |
60 | 7 | sqvald 14055 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
61 | 60 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท ๐ต) ยท (๐โ2)) = ((2 ยท ๐ต) ยท (๐ ยท ๐))) |
62 | 55, 59, 61 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท (๐ ยท ๐ต)) ยท ๐) = ((2 ยท ๐ต) ยท (๐โ2))) |
63 | 52, 62 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐โ2) ยท ๐) + ((2 ยท (๐ ยท ๐ต)) ยท ๐)) = ((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2)))) |
64 | 46, 63 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (((๐โ2) + (2 ยท (๐ ยท ๐ต))) ยท ๐) = ((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2)))) |
65 | 64 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((((๐โ2) + (2 ยท (๐ ยท ๐ต))) ยท ๐) + ((๐ตโ2) ยท ๐)) = (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((๐ตโ2) ยท ๐))) |
66 | 38, 45, 65 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (๐ โ (((๐ + ๐ต)โ2) ยท ๐) = (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((๐ตโ2) ยท ๐))) |
67 | 66 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ ((((๐ + ๐ต)โ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐)) = ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((๐ตโ2) ยท ๐)) โ ((4 ยท ๐ท) ยท ๐))) |
68 | | 3nn0 12438 |
. . . . . . . . . . . . 13
โข 3 โ
โ0 |
69 | | expcl 13992 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
70 | 7, 68, 69 | sylancl 587 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ3) โ โ) |
71 | 54, 39 | mulcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐ต) ยท (๐โ2)) โ โ) |
72 | 70, 71 | addcld 11181 |
. . . . . . . . . . 11
โข (๐ โ ((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) โ โ) |
73 | 44, 7 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ ((๐ตโ2) ยท ๐) โ โ) |
74 | | mulcl 11142 |
. . . . . . . . . . . . 13
โข ((4
โ โ โง ๐ท
โ โ) โ (4 ยท ๐ท) โ โ) |
75 | 19, 30, 74 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ (4 ยท ๐ท) โ
โ) |
76 | 75, 7 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ ((4 ยท ๐ท) ยท ๐) โ โ) |
77 | 72, 73, 76 | addsubassd 11539 |
. . . . . . . . . 10
โข (๐ โ ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((๐ตโ2) ยท ๐)) โ ((4 ยท ๐ท) ยท ๐)) = (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐)))) |
78 | 44, 75, 7 | subdird 11619 |
. . . . . . . . . . 11
โข (๐ โ (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐) = (((๐ตโ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐))) |
79 | 78 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) = (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐)))) |
80 | 77, 79 | eqtr4d 2780 |
. . . . . . . . 9
โข (๐ โ ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((๐ตโ2) ยท ๐)) โ ((4 ยท ๐ท) ยท ๐)) = (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐))) |
81 | 44, 75 | subcld 11519 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ตโ2) โ (4 ยท ๐ท)) โ
โ) |
82 | 81, 7 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐) โ โ) |
83 | 72, 82 | addcld 11181 |
. . . . . . . . . 10
โข (๐ โ (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) โ โ) |
84 | 25 | negcld 11506 |
. . . . . . . . . . . 12
โข (๐ โ -(๐ถโ2) โ โ) |
85 | 72, 82, 84 | addassd 11184 |
. . . . . . . . . . 11
โข (๐ โ ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) + -(๐ถโ2)) = (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐) + -(๐ถโ2)))) |
86 | 83, 25 | negsubd 11525 |
. . . . . . . . . . 11
โข (๐ โ ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) + -(๐ถโ2)) = ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) โ (๐ถโ2))) |
87 | | dquart.3 |
. . . . . . . . . . 11
โข (๐ โ (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + ((((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐) + -(๐ถโ2))) = 0) |
88 | 85, 86, 87 | 3eqtr3d 2785 |
. . . . . . . . . 10
โข (๐ โ ((((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) โ (๐ถโ2)) = 0) |
89 | 83, 25, 88 | subeq0d 11527 |
. . . . . . . . 9
โข (๐ โ (((๐โ3) + ((2 ยท ๐ต) ยท (๐โ2))) + (((๐ตโ2) โ (4 ยท ๐ท)) ยท ๐)) = (๐ถโ2)) |
90 | 67, 80, 89 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ ((((๐ + ๐ต)โ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐)) = (๐ถโ2)) |
91 | 18, 7 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (((๐ + ๐ต)โ2) ยท ๐) โ โ) |
92 | | subsub23 11413 |
. . . . . . . . 9
โข
(((((๐ + ๐ต)โ2) ยท ๐) โ โ โง ((4
ยท ๐ท) ยท ๐) โ โ โง (๐ถโ2) โ โ) โ
(((((๐ + ๐ต)โ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐)) = (๐ถโ2) โ ((((๐ + ๐ต)โ2) ยท ๐) โ (๐ถโ2)) = ((4 ยท ๐ท) ยท ๐))) |
93 | 91, 76, 25, 92 | syl3anc 1372 |
. . . . . . . 8
โข (๐ โ (((((๐ + ๐ต)โ2) ยท ๐) โ ((4 ยท ๐ท) ยท ๐)) = (๐ถโ2) โ ((((๐ + ๐ต)โ2) ยท ๐) โ (๐ถโ2)) = ((4 ยท ๐ท) ยท ๐))) |
94 | 90, 93 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((((๐ + ๐ต)โ2) ยท ๐) โ (๐ถโ2)) = ((4 ยท ๐ท) ยท ๐)) |
95 | 20, 30, 7 | mulassd 11185 |
. . . . . . 7
โข (๐ โ ((4 ยท ๐ท) ยท ๐) = (4 ยท (๐ท ยท ๐))) |
96 | 94, 95 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((((๐ + ๐ต)โ2) ยท ๐) โ (๐ถโ2)) = (4 ยท (๐ท ยท ๐))) |
97 | 96 | oveq1d 7377 |
. . . . 5
โข (๐ โ (((((๐ + ๐ต)โ2) ยท ๐) โ (๐ถโ2)) / 4) = ((4 ยท (๐ท ยท ๐)) / 4)) |
98 | 91, 25, 20, 22 | divsubdird 11977 |
. . . . 5
โข (๐ โ (((((๐ + ๐ต)โ2) ยท ๐) โ (๐ถโ2)) / 4) = (((((๐ + ๐ต)โ2) ยท ๐) / 4) โ ((๐ถโ2) / 4))) |
99 | 30, 7 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ท ยท ๐) โ โ) |
100 | 99, 20, 22 | divcan3d 11943 |
. . . . 5
โข (๐ โ ((4 ยท (๐ท ยท ๐)) / 4) = (๐ท ยท ๐)) |
101 | 97, 98, 100 | 3eqtr3d 2785 |
. . . 4
โข (๐ โ (((((๐ + ๐ต)โ2) ยท ๐) / 4) โ ((๐ถโ2) / 4)) = (๐ท ยท ๐)) |
102 | 31, 35, 101 | 3eqtrd 2781 |
. . 3
โข (๐ โ (((((๐ + ๐ต)โ2) / 4) โ (((๐ถโ2) / 4) / ๐)) ยท ๐) = (๐ท ยท ๐)) |
103 | 29, 30, 7, 27, 102 | mulcan2ad 11798 |
. 2
โข (๐ โ ((((๐ + ๐ต)โ2) / 4) โ (((๐ถโ2) / 4) / ๐)) = ๐ท) |
104 | 17, 103 | eqtrd 2777 |
1
โข (๐ โ ((((๐ + ๐ต) / 2)โ2) โ (((๐ถโ2) / 4) / ๐)) = ๐ท) |