Step | Hyp | Ref
| Expression |
1 | | 3nn 12240 |
. . . . . . . . . 10
โข 3 โ
โ |
2 | 1 | a1i 11 |
. . . . . . . . 9
โข (ยฌ
(3โ3) โ โ โ 3 โ โ) |
3 | | 3nn0 12439 |
. . . . . . . . . 10
โข 3 โ
โ0 |
4 | 3 | a1i 11 |
. . . . . . . . 9
โข (ยฌ
(3โ3) โ โ โ 3 โ โ0) |
5 | 2, 4 | nnexpcld 14157 |
. . . . . . . 8
โข (ยฌ
(3โ3) โ โ โ (3โ3) โ โ) |
6 | 5 | pm2.18i 129 |
. . . . . . 7
โข
(3โ3) โ โ |
7 | | nnq 12895 |
. . . . . . 7
โข
((3โ3) โ โ โ (3โ3) โ
โ) |
8 | 6, 7 | mp1i 13 |
. . . . . 6
โข (๐ด โ โ โ
(3โ3) โ โ) |
9 | | qexpcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ3) โ โ) |
10 | 3, 9 | mpan2 690 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ3) โ
โ) |
11 | | qmulcl 12900 |
. . . . . 6
โข
(((3โ3) โ โ โง (๐ดโ3) โ โ) โ ((3โ3)
ยท (๐ดโ3)) โ
โ) |
12 | 8, 10, 11 | syl2anc 585 |
. . . . 5
โข (๐ด โ โ โ
((3โ3) ยท (๐ดโ3)) โ โ) |
13 | | 1nn 12172 |
. . . . . 6
โข 1 โ
โ |
14 | | nnq 12895 |
. . . . . 6
โข (1 โ
โ โ 1 โ โ) |
15 | 13, 14 | ax-mp 5 |
. . . . 5
โข 1 โ
โ |
16 | | qsubcl 12901 |
. . . . 5
โข
((((3โ3) ยท (๐ดโ3)) โ โ โง 1 โ
โ) โ (((3โ3) ยท (๐ดโ3)) โ 1) โ
โ) |
17 | 12, 15, 16 | sylancl 587 |
. . . 4
โข (๐ด โ โ โ
(((3โ3) ยท (๐ดโ3)) โ 1) โ
โ) |
18 | | qsqcl 14044 |
. . . . . . 7
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
19 | | qmulcl 12900 |
. . . . . . 7
โข
(((3โ3) โ โ โง (๐ดโ2) โ โ) โ ((3โ3)
ยท (๐ดโ2)) โ
โ) |
20 | 8, 18, 19 | syl2anc 585 |
. . . . . 6
โข (๐ด โ โ โ
((3โ3) ยท (๐ดโ2)) โ โ) |
21 | | nnq 12895 |
. . . . . . . . 9
โข (3 โ
โ โ 3 โ โ) |
22 | 1, 21 | ax-mp 5 |
. . . . . . . 8
โข 3 โ
โ |
23 | | qsqcl 14044 |
. . . . . . . 8
โข (3 โ
โ โ (3โ2) โ โ) |
24 | 22, 23 | mp1i 13 |
. . . . . . 7
โข (๐ด โ โ โ
(3โ2) โ โ) |
25 | | qmulcl 12900 |
. . . . . . 7
โข
(((3โ2) โ โ โง ๐ด โ โ) โ ((3โ2) ยท
๐ด) โ
โ) |
26 | 24, 25 | mpancom 687 |
. . . . . 6
โข (๐ด โ โ โ
((3โ2) ยท ๐ด)
โ โ) |
27 | | qaddcl 12898 |
. . . . . 6
โข
((((3โ3) ยท (๐ดโ2)) โ โ โง ((3โ2)
ยท ๐ด) โ โ)
โ (((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) โ
โ) |
28 | 20, 26, 27 | syl2anc 585 |
. . . . 5
โข (๐ด โ โ โ
(((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) โ
โ) |
29 | | qaddcl 12898 |
. . . . 5
โข
(((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) โ โ โง 3 โ
โ) โ ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ
โ) |
30 | 28, 22, 29 | sylancl 587 |
. . . 4
โข (๐ด โ โ โ
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ
โ) |
31 | | id 22 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
32 | 31 | 3cubeslem2 41055 |
. . . . 5
โข (๐ด โ โ โ ยฌ
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) = 0) |
33 | 32 | neqned 2947 |
. . . 4
โข (๐ด โ โ โ
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ 0) |
34 | | qdivcl 12903 |
. . . 4
โข
(((((3โ3) ยท (๐ดโ3)) โ 1) โ โ โง
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ โ โง
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ 0) โ
((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3)) โ โ) |
35 | 17, 30, 33, 34 | syl3anc 1372 |
. . 3
โข (๐ด โ โ โ
((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3)) โ โ) |
36 | | qnegcl 12899 |
. . . . . . 7
โข
(((3โ3) ยท (๐ดโ3)) โ โ โ -((3โ3)
ยท (๐ดโ3)) โ
โ) |
37 | 12, 36 | syl 17 |
. . . . . 6
โข (๐ด โ โ โ
-((3โ3) ยท (๐ดโ3)) โ โ) |
38 | | qaddcl 12898 |
. . . . . 6
โข
((-((3โ3) ยท (๐ดโ3)) โ โ โง ((3โ2)
ยท ๐ด) โ โ)
โ (-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) โ
โ) |
39 | 37, 26, 38 | syl2anc 585 |
. . . . 5
โข (๐ด โ โ โ
(-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) โ
โ) |
40 | | qaddcl 12898 |
. . . . 5
โข
(((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) โ โ โง 1 โ
โ) โ ((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) โ
โ) |
41 | 39, 15, 40 | sylancl 587 |
. . . 4
โข (๐ด โ โ โ
((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) โ
โ) |
42 | | qdivcl 12903 |
. . . 4
โข
((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) โ โ โง
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ โ โง
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ 0) โ
(((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3)) โ
โ) |
43 | 41, 30, 33, 42 | syl3anc 1372 |
. . 3
โข (๐ด โ โ โ
(((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3)) โ
โ) |
44 | | qdivcl 12903 |
. . . 4
โข
(((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) โ โ โง
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ โ โง
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) โ 0) โ
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3)) โ
โ) |
45 | 28, 30, 33, 44 | syl3anc 1372 |
. . 3
โข (๐ด โ โ โ
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3)) โ
โ) |
46 | 31 | 3cubeslem4 41059 |
. . 3
โข (๐ด โ โ โ ๐ด = (((((((3โ3) ยท
(๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) +
((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) +
3))โ3))) |
47 | | oveq1 7368 |
. . . . . . 7
โข (๐ = ((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ (๐โ3) = (((((3โ3)
ยท (๐ดโ3))
โ 1) / ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) +
3))โ3)) |
48 | 47 | oveq1d 7376 |
. . . . . 6
โข (๐ = ((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ ((๐โ3) + (๐โ3)) = ((((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) + (๐โ3))) |
49 | 48 | oveq1d 7376 |
. . . . 5
โข (๐ = ((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ (((๐โ3) + (๐โ3)) + (๐โ3)) = (((((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) + (๐โ3)) + (๐โ3))) |
50 | 49 | eqeq2d 2744 |
. . . 4
โข (๐ = ((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ (๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด = (((((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) + (๐โ3)) + (๐โ3)))) |
51 | | oveq1 7368 |
. . . . . . 7
โข (๐ = (((-((3โ3) ยท
(๐ดโ3)) + ((3โ2)
ยท ๐ด)) + 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ (๐โ3) = ((((-((3โ3)
ยท (๐ดโ3)) +
((3โ2) ยท ๐ด)) +
1) / ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) +
3))โ3)) |
52 | 51 | oveq2d 7377 |
. . . . . 6
โข (๐ = (((-((3โ3) ยท
(๐ดโ3)) + ((3โ2)
ยท ๐ด)) + 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ ((((((3โ3)
ยท (๐ดโ3))
โ 1) / ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) + (๐โ3)) = ((((((3โ3)
ยท (๐ดโ3))
โ 1) / ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) +
((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) +
3))โ3))) |
53 | 52 | oveq1d 7376 |
. . . . 5
โข (๐ = (((-((3โ3) ยท
(๐ดโ3)) + ((3โ2)
ยท ๐ด)) + 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ (((((((3โ3)
ยท (๐ดโ3))
โ 1) / ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) + (๐โ3)) + (๐โ3)) = (((((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) +
((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (๐โ3))) |
54 | 53 | eqeq2d 2744 |
. . . 4
โข (๐ = (((-((3โ3) ยท
(๐ดโ3)) + ((3โ2)
ยท ๐ด)) + 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) โ (๐ด = (((((((3โ3) ยท
(๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) + (๐โ3)) + (๐โ3)) โ ๐ด = (((((((3โ3) ยท (๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) +
((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (๐โ3)))) |
55 | | oveq1 7368 |
. . . . . 6
โข (๐ = ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท
๐ด)) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3)) โ (๐โ3) =
(((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) +
3))โ3)) |
56 | 55 | oveq2d 7377 |
. . . . 5
โข (๐ = ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท
๐ด)) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3)) โ (((((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3))โ3) + ((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (๐โ3)) =
(((((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3))โ3) + ((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) +
3))โ3))) |
57 | 56 | eqeq2d 2744 |
. . . 4
โข (๐ = ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท
๐ด)) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3)) โ (๐ด =
(((((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3))โ3) + ((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (๐โ3)) โ ๐ด = (((((((3โ3) ยท
(๐ดโ3)) โ 1) /
((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3))โ3) +
((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) +
3))โ3)))) |
58 | 50, 54, 57 | rspc3ev 3596 |
. . 3
โข
(((((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3)) โ โ โง (((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3)) โ
โ โง ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3)) โ
โ) โง ๐ด =
(((((((3โ3) ยท (๐ดโ3)) โ 1) / ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3))โ3) + ((((-((3โ3) ยท (๐ดโ3)) + ((3โ2) ยท ๐ด)) + 1) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3))โ3))
+ (((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) / ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) +
3))โ3))) โ โ๐ โ โ โ๐ โ โ โ๐ โ โ ๐ด = (((๐โ3) + (๐โ3)) + (๐โ3))) |
59 | 35, 43, 45, 46, 58 | syl31anc 1374 |
. 2
โข (๐ด โ โ โ
โ๐ โ โ
โ๐ โ โ
โ๐ โ โ
๐ด = (((๐โ3) + (๐โ3)) + (๐โ3))) |
60 | | 3anass 1096 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐ โ โ โง (๐ โ โ โง ๐ โ
โ))) |
61 | | qexpcl 13992 |
. . . . . . . . . 10
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
62 | 3, 61 | mpan2 690 |
. . . . . . . . 9
โข (๐ โ โ โ (๐โ3) โ
โ) |
63 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
64 | | qexpcl 13992 |
. . . . . . . . . 10
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
65 | 63, 3, 64 | sylancl 587 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ3) โ
โ) |
66 | | qaddcl 12898 |
. . . . . . . . 9
โข (((๐โ3) โ โ โง
(๐โ3) โ โ)
โ ((๐โ3) + (๐โ3)) โ
โ) |
67 | 62, 65, 66 | syl2an2r 684 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ3) + (๐โ3)) โ โ) |
68 | | simprr 772 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
69 | | qexpcl 13992 |
. . . . . . . . 9
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
70 | 68, 3, 69 | sylancl 587 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ3) โ
โ) |
71 | | qaddcl 12898 |
. . . . . . . 8
โข ((((๐โ3) + (๐โ3)) โ โ โง (๐โ3) โ โ) โ
(((๐โ3) + (๐โ3)) + (๐โ3)) โ โ) |
72 | 67, 70, 71 | syl2anc 585 |
. . . . . . 7
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ
(((๐โ3) + (๐โ3)) + (๐โ3)) โ โ) |
73 | | eleq1a 2829 |
. . . . . . 7
โข ((((๐โ3) + (๐โ3)) + (๐โ3)) โ โ โ (๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด โ โ)) |
74 | 72, 73 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ โ)) โ (๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด โ โ)) |
75 | 74 | a1i 11 |
. . . . 5
โข (โค
โ ((๐ โ โ
โง (๐ โ โ
โง ๐ โ โ))
โ (๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด โ โ))) |
76 | 60, 75 | biimtrid 241 |
. . . 4
โข (โค
โ ((๐ โ โ
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด โ โ))) |
77 | 76 | rexlimdv3d 41053 |
. . 3
โข (โค
โ (โ๐ โ
โ โ๐ โ
โ โ๐ โ
โ ๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด โ โ)) |
78 | 77 | mptru 1549 |
. 2
โข
(โ๐ โ
โ โ๐ โ
โ โ๐ โ
โ ๐ด = (((๐โ3) + (๐โ3)) + (๐โ3)) โ ๐ด โ โ) |
79 | 59, 78 | impbii 208 |
1
โข (๐ด โ โ โ
โ๐ โ โ
โ๐ โ โ
โ๐ โ โ
๐ด = (((๐โ3) + (๐โ3)) + (๐โ3))) |