Step | Hyp | Ref
| Expression |
1 | | df-4 12225 |
. . . 4
โข 4 = (3 +
1) |
2 | 1 | oveq2i 7373 |
. . 3
โข ((๐ด + ๐ต)โ4) = ((๐ด + ๐ต)โ(3 + 1)) |
3 | | addcl 11140 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
4 | | 3nn0 12438 |
. . . 4
โข 3 โ
โ0 |
5 | | expp1 13981 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง 3 โ
โ0) โ ((๐ด + ๐ต)โ(3 + 1)) = (((๐ด + ๐ต)โ3) ยท (๐ด + ๐ต))) |
6 | 3, 4, 5 | sylancl 587 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ(3 + 1)) = (((๐ด + ๐ต)โ3) ยท (๐ด + ๐ต))) |
7 | 2, 6 | eqtrid 2789 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ4) = (((๐ด + ๐ต)โ3) ยท (๐ด + ๐ต))) |
8 | | binom3 14134 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ3) = (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)))) |
9 | 8 | oveq1d 7377 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต)โ3) ยท (๐ด + ๐ต)) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท (๐ด + ๐ต))) |
10 | | simpl 484 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
11 | | expcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ3) โ โ) |
12 | 10, 4, 11 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ3) โ
โ) |
13 | | 3cn 12241 |
. . . . . . 7
โข 3 โ
โ |
14 | 10 | sqcld 14056 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) โ
โ) |
15 | | simpr 486 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
16 | 14, 15 | mulcld 11182 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) ยท ๐ต) โ
โ) |
17 | | mulcl 11142 |
. . . . . . 7
โข ((3
โ โ โง ((๐ดโ2) ยท ๐ต) โ โ) โ (3 ยท ((๐ดโ2) ยท ๐ต)) โ
โ) |
18 | 13, 16, 17 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท ((๐ดโ2)
ยท ๐ต)) โ
โ) |
19 | 12, 18 | addcld 11181 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) โ
โ) |
20 | 15 | sqcld 14056 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) โ
โ) |
21 | 10, 20 | mulcld 11182 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท (๐ตโ2)) โ โ) |
22 | | mulcl 11142 |
. . . . . . 7
โข ((3
โ โ โง (๐ด
ยท (๐ตโ2)) โ
โ) โ (3 ยท (๐ด ยท (๐ตโ2))) โ โ) |
23 | 13, 21, 22 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท (๐ด ยท (๐ตโ2))) โ
โ) |
24 | | expcl 13992 |
. . . . . . 7
โข ((๐ต โ โ โง 3 โ
โ0) โ (๐ตโ3) โ โ) |
25 | 15, 4, 24 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ3) โ
โ) |
26 | 23, 25 | addcld 11181 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)) โ โ) |
27 | 19, 26 | addcld 11181 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) โ โ) |
28 | 27, 10, 15 | adddid 11186 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท (๐ด + ๐ต)) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ด) + ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ต))) |
29 | 1 | oveq2i 7373 |
. . . . . . . . 9
โข (๐ดโ4) = (๐ดโ(3 + 1)) |
30 | | expp1 13981 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ(3 + 1)) = ((๐ดโ3) ยท ๐ด)) |
31 | 10, 4, 30 | sylancl 587 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ(3 + 1)) = ((๐ดโ3) ยท ๐ด)) |
32 | 29, 31 | eqtr2id 2790 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ3) ยท ๐ด) = (๐ดโ4)) |
33 | 13 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ 3 โ
โ) |
34 | 33, 16, 10 | mulassd 11185 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ2)
ยท ๐ต)) ยท ๐ด) = (3 ยท (((๐ดโ2) ยท ๐ต) ยท ๐ด))) |
35 | 14, 15, 10 | mul32d 11372 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) ยท ๐ต) ยท ๐ด) = (((๐ดโ2) ยท ๐ด) ยท ๐ต)) |
36 | | df-3 12224 |
. . . . . . . . . . . . . 14
โข 3 = (2 +
1) |
37 | 36 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข (๐ดโ3) = (๐ดโ(2 + 1)) |
38 | | 2nn0 12437 |
. . . . . . . . . . . . . 14
โข 2 โ
โ0 |
39 | | expp1 13981 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 2 โ
โ0) โ (๐ดโ(2 + 1)) = ((๐ดโ2) ยท ๐ด)) |
40 | 10, 38, 39 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ(2 + 1)) = ((๐ดโ2) ยท ๐ด)) |
41 | 37, 40 | eqtr2id 2790 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) ยท ๐ด) = (๐ดโ3)) |
42 | 41 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) ยท ๐ด) ยท ๐ต) = ((๐ดโ3) ยท ๐ต)) |
43 | 35, 42 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) ยท ๐ต) ยท ๐ด) = ((๐ดโ3) ยท ๐ต)) |
44 | 43 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท (((๐ดโ2)
ยท ๐ต) ยท ๐ด)) = (3 ยท ((๐ดโ3) ยท ๐ต))) |
45 | 34, 44 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ2)
ยท ๐ต)) ยท ๐ด) = (3 ยท ((๐ดโ3) ยท ๐ต))) |
46 | 32, 45 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ3) ยท ๐ด) + ((3 ยท ((๐ดโ2) ยท ๐ต)) ยท ๐ด)) = ((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต)))) |
47 | 12, 10, 18, 46 | joinlmuladdmuld 11189 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) ยท ๐ด) = ((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต)))) |
48 | 33, 21, 10 | mulassd 11185 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท (๐ด ยท (๐ตโ2))) ยท ๐ด) = (3 ยท ((๐ด ยท (๐ตโ2)) ยท ๐ด))) |
49 | 10, 20, 10 | mul32d 11372 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท (๐ตโ2)) ยท ๐ด) = ((๐ด ยท ๐ด) ยท (๐ตโ2))) |
50 | 10 | sqvald 14055 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) = (๐ด ยท ๐ด)) |
51 | 50 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) ยท (๐ตโ2)) = ((๐ด ยท ๐ด) ยท (๐ตโ2))) |
52 | 49, 51 | eqtr4d 2780 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท (๐ตโ2)) ยท ๐ด) = ((๐ดโ2) ยท (๐ตโ2))) |
53 | 52 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท ((๐ด ยท
(๐ตโ2)) ยท ๐ด)) = (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) |
54 | 48, 53 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท (๐ด ยท (๐ตโ2))) ยท ๐ด) = (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) |
55 | 25, 10 | mulcomd 11183 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ตโ3) ยท ๐ด) = (๐ด ยท (๐ตโ3))) |
56 | 54, 55 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((3
ยท (๐ด ยท (๐ตโ2))) ยท ๐ด) + ((๐ตโ3) ยท ๐ด)) = ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3)))) |
57 | 23, 10, 25, 56 | joinlmuladdmuld 11189 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((3
ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)) ยท ๐ด) = ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3)))) |
58 | 47, 57 | oveq12d 7380 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) ยท ๐ด) + (((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)) ยท ๐ด)) = (((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3))))) |
59 | 19, 10, 26, 58 | joinlmuladdmuld 11189 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ด) = (((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3))))) |
60 | 19, 26, 15 | adddird 11187 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ต) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) ยท ๐ต) + (((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)) ยท ๐ต))) |
61 | 33, 16, 15 | mulassd 11185 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ2)
ยท ๐ต)) ยท ๐ต) = (3 ยท (((๐ดโ2) ยท ๐ต) ยท ๐ต))) |
62 | 14, 15, 15 | mulassd 11185 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) ยท ๐ต) ยท ๐ต) = ((๐ดโ2) ยท (๐ต ยท ๐ต))) |
63 | 15 | sqvald 14055 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) = (๐ต ยท ๐ต)) |
64 | 63 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) ยท (๐ตโ2)) = ((๐ดโ2) ยท (๐ต ยท ๐ต))) |
65 | 62, 64 | eqtr4d 2780 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) ยท ๐ต) ยท ๐ต) = ((๐ดโ2) ยท (๐ตโ2))) |
66 | 65 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท (((๐ดโ2)
ยท ๐ต) ยท ๐ต)) = (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) |
67 | 61, 66 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ2)
ยท ๐ต)) ยท ๐ต) = (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) |
68 | 67 | oveq2d 7378 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ3) ยท ๐ต) + ((3 ยท ((๐ดโ2) ยท ๐ต)) ยท ๐ต)) = (((๐ดโ3) ยท ๐ต) + (3 ยท ((๐ดโ2) ยท (๐ตโ2))))) |
69 | 12, 15, 18, 68 | joinlmuladdmuld 11189 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) ยท ๐ต) = (((๐ดโ3) ยท ๐ต) + (3 ยท ((๐ดโ2) ยท (๐ตโ2))))) |
70 | 33, 21, 15 | mulassd 11185 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท (๐ด ยท (๐ตโ2))) ยท ๐ต) = (3 ยท ((๐ด ยท (๐ตโ2)) ยท ๐ต))) |
71 | 10, 20, 15 | mulassd 11185 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท (๐ตโ2)) ยท ๐ต) = (๐ด ยท ((๐ตโ2) ยท ๐ต))) |
72 | 36 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข (๐ตโ3) = (๐ตโ(2 + 1)) |
73 | | expp1 13981 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ โง 2 โ
โ0) โ (๐ตโ(2 + 1)) = ((๐ตโ2) ยท ๐ต)) |
74 | 15, 38, 73 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ(2 + 1)) = ((๐ตโ2) ยท ๐ต)) |
75 | 72, 74 | eqtr2id 2790 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ตโ2) ยท ๐ต) = (๐ตโ3)) |
76 | 75 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ((๐ตโ2) ยท ๐ต)) = (๐ด ยท (๐ตโ3))) |
77 | 71, 76 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท (๐ตโ2)) ยท ๐ต) = (๐ด ยท (๐ตโ3))) |
78 | 77 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท ((๐ด ยท
(๐ตโ2)) ยท ๐ต)) = (3 ยท (๐ด ยท (๐ตโ3)))) |
79 | 70, 78 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท (๐ด ยท (๐ตโ2))) ยท ๐ต) = (3 ยท (๐ด ยท (๐ตโ3)))) |
80 | 1 | oveq2i 7373 |
. . . . . . . . 9
โข (๐ตโ4) = (๐ตโ(3 + 1)) |
81 | | expp1 13981 |
. . . . . . . . . 10
โข ((๐ต โ โ โง 3 โ
โ0) โ (๐ตโ(3 + 1)) = ((๐ตโ3) ยท ๐ต)) |
82 | 15, 4, 81 | sylancl 587 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ(3 + 1)) = ((๐ตโ3) ยท ๐ต)) |
83 | 80, 82 | eqtr2id 2790 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ตโ3) ยท ๐ต) = (๐ตโ4)) |
84 | 79, 83 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((3
ยท (๐ด ยท (๐ตโ2))) ยท ๐ต) + ((๐ตโ3) ยท ๐ต)) = ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))) |
85 | 23, 15, 25, 84 | joinlmuladdmuld 11189 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((3
ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)) ยท ๐ต) = ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))) |
86 | 69, 85 | oveq12d 7380 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) ยท ๐ต) + (((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)) ยท ๐ต)) = ((((๐ดโ3) ยท ๐ต) + (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))) |
87 | 12, 15 | mulcld 11182 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ3) ยท ๐ต) โ
โ) |
88 | 14, 20 | mulcld 11182 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) ยท (๐ตโ2)) โ
โ) |
89 | | mulcl 11142 |
. . . . . . 7
โข ((3
โ โ โง ((๐ดโ2) ยท (๐ตโ2)) โ โ) โ (3 ยท
((๐ดโ2) ยท (๐ตโ2))) โ
โ) |
90 | 13, 88, 89 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท ((๐ดโ2)
ยท (๐ตโ2)))
โ โ) |
91 | 10, 25 | mulcld 11182 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท (๐ตโ3)) โ โ) |
92 | | mulcl 11142 |
. . . . . . . 8
โข ((3
โ โ โง (๐ด
ยท (๐ตโ3)) โ
โ) โ (3 ยท (๐ด ยท (๐ตโ3))) โ โ) |
93 | 13, 91, 92 | sylancr 588 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท (๐ด ยท (๐ตโ3))) โ
โ) |
94 | | 4nn0 12439 |
. . . . . . . 8
โข 4 โ
โ0 |
95 | | expcl 13992 |
. . . . . . . 8
โข ((๐ต โ โ โง 4 โ
โ0) โ (๐ตโ4) โ โ) |
96 | 15, 94, 95 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ4) โ
โ) |
97 | 93, 96 | addcld 11181 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)) โ โ) |
98 | 87, 90, 97 | addassd 11184 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) ยท
๐ต) + (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) + ((3 ยท
(๐ด ยท (๐ตโ3))) + (๐ตโ4))) = (((๐ดโ3) ยท ๐ต) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
99 | 60, 86, 98 | 3eqtrd 2781 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ต) = (((๐ดโ3) ยท ๐ต) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
100 | 59, 99 | oveq12d 7380 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((((๐ดโ3) + (3
ยท ((๐ดโ2)
ยท ๐ต))) + ((3
ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ด) + ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท ๐ต)) = ((((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3)))) + (((๐ดโ3) ยท ๐ต) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))))) |
101 | | expcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง 4 โ
โ0) โ (๐ดโ4) โ โ) |
102 | 10, 94, 101 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ4) โ
โ) |
103 | | mulcl 11142 |
. . . . . . 7
โข ((3
โ โ โง ((๐ดโ3) ยท ๐ต) โ โ) โ (3 ยท ((๐ดโ3) ยท ๐ต)) โ
โ) |
104 | 13, 87, 103 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (3
ยท ((๐ดโ3)
ยท ๐ต)) โ
โ) |
105 | 102, 104 | addcld 11181 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) โ
โ) |
106 | 90, 91 | addcld 11181 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ2)
ยท (๐ตโ2))) +
(๐ด ยท (๐ตโ3))) โ
โ) |
107 | 90, 97 | addcld 11181 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ2)
ยท (๐ตโ2))) + ((3
ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))) โ โ) |
108 | 105, 106,
87, 107 | add4d 11390 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ4) + (3 ยท
((๐ดโ3) ยท ๐ต))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3)))) + (((๐ดโ3) ยท ๐ต) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) = ((((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) + ((๐ดโ3) ยท ๐ต)) + (((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))))) |
109 | 102, 104,
87 | addassd 11184 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) + ((๐ดโ3) ยท ๐ต)) = ((๐ดโ4) + ((3 ยท ((๐ดโ3) ยท ๐ต)) + ((๐ดโ3) ยท ๐ต)))) |
110 | 1 | oveq1i 7372 |
. . . . . . . . 9
โข (4
ยท ((๐ดโ3)
ยท ๐ต)) = ((3 + 1)
ยท ((๐ดโ3)
ยท ๐ต)) |
111 | | ax-1cn 11116 |
. . . . . . . . . . 11
โข 1 โ
โ |
112 | 111 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ 1 โ
โ) |
113 | 33, 112, 87 | adddird 11187 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3 + 1)
ยท ((๐ดโ3)
ยท ๐ต)) = ((3 ยท
((๐ดโ3) ยท ๐ต)) + (1 ยท ((๐ดโ3) ยท ๐ต)))) |
114 | 110, 113 | eqtrid 2789 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (4
ยท ((๐ดโ3)
ยท ๐ต)) = ((3 ยท
((๐ดโ3) ยท ๐ต)) + (1 ยท ((๐ดโ3) ยท ๐ต)))) |
115 | 87 | mulid2d 11180 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ((๐ดโ3)
ยท ๐ต)) = ((๐ดโ3) ยท ๐ต)) |
116 | 115 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3
ยท ((๐ดโ3)
ยท ๐ต)) + (1 ยท
((๐ดโ3) ยท ๐ต))) = ((3 ยท ((๐ดโ3) ยท ๐ต)) + ((๐ดโ3) ยท ๐ต))) |
117 | 114, 116 | eqtrd 2777 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (4
ยท ((๐ดโ3)
ยท ๐ต)) = ((3 ยท
((๐ดโ3) ยท ๐ต)) + ((๐ดโ3) ยท ๐ต))) |
118 | 117 | oveq2d 7378 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ4) + (4 ยท ((๐ดโ3) ยท ๐ต))) = ((๐ดโ4) + ((3 ยท ((๐ดโ3) ยท ๐ต)) + ((๐ดโ3) ยท ๐ต)))) |
119 | 109, 118 | eqtr4d 2780 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ4) + (3 ยท ((๐ดโ3) ยท ๐ต))) + ((๐ดโ3) ยท ๐ต)) = ((๐ดโ4) + (4 ยท ((๐ดโ3) ยท ๐ต)))) |
120 | 90, 91, 90, 97 | add4d 11390 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((3
ยท ((๐ดโ2)
ยท (๐ตโ2))) +
(๐ด ยท (๐ตโ3))) + ((3 ยท
((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))) = (((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) + ((๐ด ยท (๐ตโ3)) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
121 | | 3p3e6 12312 |
. . . . . . . . 9
โข (3 + 3) =
6 |
122 | 121 | oveq1i 7372 |
. . . . . . . 8
โข ((3 + 3)
ยท ((๐ดโ2)
ยท (๐ตโ2))) = (6
ยท ((๐ดโ2)
ยท (๐ตโ2))) |
123 | 33, 33, 88 | adddird 11187 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((3 + 3)
ยท ((๐ดโ2)
ยท (๐ตโ2))) = ((3
ยท ((๐ดโ2)
ยท (๐ตโ2))) + (3
ยท ((๐ดโ2)
ยท (๐ตโ2))))) |
124 | 122, 123 | eqtr3id 2791 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (6
ยท ((๐ดโ2)
ยท (๐ตโ2))) = ((3
ยท ((๐ดโ2)
ยท (๐ตโ2))) + (3
ยท ((๐ดโ2)
ยท (๐ตโ2))))) |
125 | | 3p1e4 12305 |
. . . . . . . . . . . . 13
โข (3 + 1) =
4 |
126 | 13, 111, 125 | addcomli 11354 |
. . . . . . . . . . . 12
โข (1 + 3) =
4 |
127 | 126 | oveq1i 7372 |
. . . . . . . . . . 11
โข ((1 + 3)
ยท (๐ด ยท (๐ตโ3))) = (4 ยท (๐ด ยท (๐ตโ3))) |
128 | 112, 33, 91 | adddird 11187 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 + 3)
ยท (๐ด ยท (๐ตโ3))) = ((1 ยท (๐ด ยท (๐ตโ3))) + (3 ยท (๐ด ยท (๐ตโ3))))) |
129 | 127, 128 | eqtr3id 2791 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (4
ยท (๐ด ยท (๐ตโ3))) = ((1 ยท (๐ด ยท (๐ตโ3))) + (3 ยท (๐ด ยท (๐ตโ3))))) |
130 | 91 | mulid2d 11180 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท (๐ด ยท (๐ตโ3))) = (๐ด ยท (๐ตโ3))) |
131 | 130 | oveq1d 7377 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1
ยท (๐ด ยท (๐ตโ3))) + (3 ยท (๐ด ยท (๐ตโ3)))) = ((๐ด ยท (๐ตโ3)) + (3 ยท (๐ด ยท (๐ตโ3))))) |
132 | 129, 131 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (4
ยท (๐ด ยท (๐ตโ3))) = ((๐ด ยท (๐ตโ3)) + (3 ยท (๐ด ยท (๐ตโ3))))) |
133 | 132 | oveq1d 7377 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((4
ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)) = (((๐ด ยท (๐ตโ3)) + (3 ยท (๐ด ยท (๐ตโ3)))) + (๐ตโ4))) |
134 | 91, 93, 96 | addassd 11184 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด ยท (๐ตโ3)) + (3 ยท (๐ด ยท (๐ตโ3)))) + (๐ตโ4)) = ((๐ด ยท (๐ตโ3)) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))) |
135 | 133, 134 | eqtrd 2777 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((4
ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)) = ((๐ด ยท (๐ตโ3)) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))) |
136 | 124, 135 | oveq12d 7380 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((6
ยท ((๐ดโ2)
ยท (๐ตโ2))) + ((4
ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))) = (((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (3 ยท ((๐ดโ2) ยท (๐ตโ2)))) + ((๐ด ยท (๐ตโ3)) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
137 | 120, 136 | eqtr4d 2780 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((3
ยท ((๐ดโ2)
ยท (๐ตโ2))) +
(๐ด ยท (๐ตโ3))) + ((3 ยท
((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))) = ((6 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((4 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4)))) |
138 | 119, 137 | oveq12d 7380 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ4) + (3 ยท
((๐ดโ3) ยท ๐ต))) + ((๐ดโ3) ยท ๐ต)) + (((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) = (((๐ดโ4) + (4 ยท ((๐ดโ3) ยท ๐ต))) + ((6 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((4 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
139 | 108, 138 | eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ4) + (3 ยท
((๐ดโ3) ยท ๐ต))) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + (๐ด ยท (๐ตโ3)))) + (((๐ดโ3) ยท ๐ต) + ((3 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((3 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) = (((๐ดโ4) + (4 ยท ((๐ดโ3) ยท ๐ต))) + ((6 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((4 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
140 | 28, 100, 139 | 3eqtrd 2781 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ดโ3) + (3 ยท
((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) ยท (๐ด + ๐ต)) = (((๐ดโ4) + (4 ยท ((๐ดโ3) ยท ๐ต))) + ((6 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((4 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |
141 | 7, 9, 140 | 3eqtrd 2781 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ4) = (((๐ดโ4) + (4 ยท ((๐ดโ3) ยท ๐ต))) + ((6 ยท ((๐ดโ2) ยท (๐ตโ2))) + ((4 ยท (๐ด ยท (๐ตโ3))) + (๐ตโ4))))) |