Step | Hyp | Ref
| Expression |
1 | | cu3addd.1 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ โ) |
2 | | cu3addd.2 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ โ) |
3 | 1, 2 | addcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด + ๐ต) โ โ) |
4 | | cu3addd.3 |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
5 | 3, 4 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด + ๐ต) โ โ โง ๐ถ โ โ)) |
6 | | binom3 14136 |
. . . . . . . . . . . 12
โข (((๐ด + ๐ต) โ โ โง ๐ถ โ โ) โ (((๐ด + ๐ต) + ๐ถ)โ3) = ((((๐ด + ๐ต)โ3) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (((๐ด + ๐ต) โ โ โง ๐ถ โ โ) โ (((๐ด + ๐ต) + ๐ถ)โ3) = ((((๐ด + ๐ต)โ3) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))))) |
8 | 5, 7 | mpd 15 |
. . . . . . . . . 10
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = ((((๐ด + ๐ต)โ3) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
9 | | binom3 14136 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ3) = (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)))) |
10 | 1, 2, 9 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ด + ๐ต)โ3) = (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)))) |
11 | 10 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ โ (((๐ด + ๐ต)โ3) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ)))) |
12 | 11 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ ((((๐ด + ๐ต)โ3) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
13 | 8, 12 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
14 | 1, 2 | binom2d 41049 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
15 | 14 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด + ๐ต)โ2) ยท ๐ถ) = ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ)) |
16 | 15 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ โ (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ)) = (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ))) |
17 | 16 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ)))) |
18 | 17 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท (((๐ด + ๐ต)โ2) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
19 | 13, 18 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
20 | 1 | sqcld 14058 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ดโ2) โ โ) |
21 | | 2cnd 12239 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ
โ) |
22 | 1, 2 | mulcld 11183 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
23 | 21, 22 | mulcld 11183 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท (๐ด ยท ๐ต)) โ โ) |
24 | 20, 23 | addcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ โ) |
25 | 2 | sqcld 14058 |
. . . . . . . . . . . 12
โข (๐ โ (๐ตโ2) โ โ) |
26 | 24, 25, 4 | adddird 11188 |
. . . . . . . . . . 11
โข (๐ โ ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ) = ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ))) |
27 | 26 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ)) = (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ)))) |
28 | 27 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ))))) |
29 | 28 | oveq1d 7376 |
. . . . . . . 8
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) ยท ๐ถ))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
30 | 19, 29 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
31 | 20, 23, 4 | adddird 11188 |
. . . . . . . . . . 11
โข (๐ โ (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) = (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) |
32 | 31 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ)) = ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ))) |
33 | 32 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ))) = (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ)))) |
34 | 33 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ)))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ))))) |
35 | 34 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ) + ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
36 | 30, 35 | eqtrd 2773 |
. . . . . 6
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
37 | | 3cn 12242 |
. . . . . . . . . 10
โข 3 โ
โ |
38 | 37 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 3 โ
โ) |
39 | 20, 4 | mulcld 11183 |
. . . . . . . . . 10
โข (๐ โ ((๐ดโ2) ยท ๐ถ) โ โ) |
40 | 23, 4 | mulcld 11183 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ) โ โ) |
41 | 39, 40 | addcld 11182 |
. . . . . . . . 9
โข (๐ โ (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) โ โ) |
42 | 25, 4 | mulcld 11183 |
. . . . . . . . 9
โข (๐ โ ((๐ตโ2) ยท ๐ถ) โ โ) |
43 | 38, 41, 42 | adddid 11187 |
. . . . . . . 8
โข (๐ โ (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ))) = ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) |
44 | 43 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ)))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ))))) |
45 | 44 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (3 ยท ((((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)) + ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
46 | 36, 45 | eqtrd 2773 |
. . . . 5
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
47 | 38, 39, 40 | adddid 11187 |
. . . . . . . 8
โข (๐ โ (3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) = ((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)))) |
48 | 47 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ))) = (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) |
49 | 48 | oveq2d 7377 |
. . . . . 6
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท
(๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ))))) |
50 | 49 | oveq1d 7376 |
. . . . 5
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + ((3 ยท (((๐ดโ2) ยท ๐ถ) + ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท
(๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
51 | 46, 50 | eqtrd 2773 |
. . . 4
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท
(๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
52 | 38, 21, 22 | mulassd 11186 |
. . . . . . . . . . 11
โข (๐ โ ((3 ยท 2) ยท
(๐ด ยท ๐ต)) = (3 ยท (2 ยท
(๐ด ยท ๐ต)))) |
53 | 52 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ) = ((3 ยท (2 ยท (๐ด ยท ๐ต))) ยท ๐ถ)) |
54 | 38, 23, 4 | mulassd 11186 |
. . . . . . . . . 10
โข (๐ โ ((3 ยท (2 ยท
(๐ด ยท ๐ต))) ยท ๐ถ) = (3 ยท ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) |
55 | 53, 54 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ) = (3 ยท ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) |
56 | 55 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) = ((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ)))) |
57 | 56 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ))) = (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท (๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) |
58 | 57 | oveq2d 7377 |
. . . . . 6
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท
(๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ))))) |
59 | 58 | eqcomd 2739 |
. . . . 5
โข (๐ โ ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท
(๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) = ((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ))))) |
60 | 59 | oveq1d 7376 |
. . . 4
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (3 ยท ((2 ยท
(๐ด ยท ๐ต)) ยท ๐ถ))) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
61 | 51, 60 | eqtrd 2773 |
. . 3
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)))) |
62 | 4 | sqcld 14058 |
. . . . . . 7
โข (๐ โ (๐ถโ2) โ โ) |
63 | 1, 2, 62 | adddird 11188 |
. . . . . 6
โข (๐ โ ((๐ด + ๐ต) ยท (๐ถโ2)) = ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) |
64 | 63 | oveq2d 7377 |
. . . . 5
โข (๐ โ (3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) = (3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2))))) |
65 | 64 | oveq1d 7376 |
. . . 4
โข (๐ โ ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3)) = ((3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) + (๐ถโ3))) |
66 | 65 | oveq2d 7377 |
. . 3
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด + ๐ต) ยท (๐ถโ2))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) + (๐ถโ3)))) |
67 | 61, 66 | eqtrd 2773 |
. 2
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) + (๐ถโ3)))) |
68 | 1, 62 | mulcld 11183 |
. . . . 5
โข (๐ โ (๐ด ยท (๐ถโ2)) โ โ) |
69 | 2, 62 | mulcld 11183 |
. . . . 5
โข (๐ โ (๐ต ยท (๐ถโ2)) โ โ) |
70 | 38, 68, 69 | adddid 11187 |
. . . 4
โข (๐ โ (3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) = ((3 ยท (๐ด ยท (๐ถโ2))) + (3 ยท (๐ต ยท (๐ถโ2))))) |
71 | 70 | oveq1d 7376 |
. . 3
โข (๐ โ ((3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) + (๐ถโ3)) = (((3 ยท (๐ด ยท (๐ถโ2))) + (3 ยท (๐ต ยท (๐ถโ2)))) + (๐ถโ3))) |
72 | 71 | oveq2d 7377 |
. 2
โข (๐ โ (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + ((3 ยท ((๐ด ยท (๐ถโ2)) + (๐ต ยท (๐ถโ2)))) + (๐ถโ3))) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + (((3 ยท (๐ด ยท (๐ถโ2))) + (3 ยท (๐ต ยท (๐ถโ2)))) + (๐ถโ3)))) |
73 | 67, 72 | eqtrd 2773 |
1
โข (๐ โ (((๐ด + ๐ต) + ๐ถ)โ3) = (((((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3))) + (((3 ยท ((๐ดโ2) ยท ๐ถ)) + (((3 ยท 2) ยท
(๐ด ยท ๐ต)) ยท ๐ถ)) + (3 ยท ((๐ตโ2) ยท ๐ถ)))) + (((3 ยท (๐ด ยท (๐ถโ2))) + (3 ยท (๐ต ยท (๐ถโ2)))) + (๐ถโ3)))) |