Step | Hyp | Ref
| Expression |
1 | | 3re 12241 |
. . . . . . . . 9
โข 3 โ
โ |
2 | 1 | a1i 11 |
. . . . . . . 8
โข (๐ โ 3 โ
โ) |
3 | 2 | recnd 11191 |
. . . . . . 7
โข (๐ โ 3 โ
โ) |
4 | 3 | mulid2d 11181 |
. . . . . 6
โข (๐ โ (1 ยท 3) =
3) |
5 | 4 | oveq2d 7377 |
. . . . 5
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) ยท 3) + (1
ยท 3)) = (((((3โ2) ยท (๐ดโ2)) + (3 ยท ๐ด)) ยท 3) + 3)) |
6 | 3 | sqcld 14058 |
. . . . . . . 8
โข (๐ โ (3โ2) โ
โ) |
7 | | 3cubeslem1.a |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
8 | | qre 12886 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด โ
โ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
10 | 9 | resqcld 14039 |
. . . . . . . . 9
โข (๐ โ (๐ดโ2) โ โ) |
11 | 10 | recnd 11191 |
. . . . . . . 8
โข (๐ โ (๐ดโ2) โ โ) |
12 | 6, 11 | mulcld 11183 |
. . . . . . 7
โข (๐ โ ((3โ2) ยท
(๐ดโ2)) โ
โ) |
13 | 9 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
14 | 3, 13 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (3 ยท ๐ด) โ
โ) |
15 | 12, 14 | addcld 11182 |
. . . . . 6
โข (๐ โ (((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) โ
โ) |
16 | | 1cnd 11158 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
17 | 15, 16, 3 | adddird 11188 |
. . . . 5
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) ยท 3) =
(((((3โ2) ยท (๐ดโ2)) + (3 ยท ๐ด)) ยท 3) + (1 ยท
3))) |
18 | 3, 13, 3 | mulassd 11186 |
. . . . . . . 8
โข (๐ โ ((3 ยท ๐ด) ยท 3) = (3 ยท
(๐ด ยท
3))) |
19 | 18 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) ยท 3) +
((3 ยท ๐ด) ยท
3)) = ((((3โ2) ยท (๐ดโ2)) ยท 3) + (3 ยท (๐ด ยท 3)))) |
20 | 19 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) ยท 3) +
((3 ยท ๐ด) ยท
3)) + 3) = (((((3โ2) ยท (๐ดโ2)) ยท 3) + (3 ยท (๐ด ยท 3))) +
3)) |
21 | 12, 14, 3 | adddird 11188 |
. . . . . . 7
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) ยท 3) =
((((3โ2) ยท (๐ดโ2)) ยท 3) + ((3 ยท ๐ด) ยท 3))) |
22 | 21 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) ยท 3) + 3) =
(((((3โ2) ยท (๐ดโ2)) ยท 3) + ((3 ยท ๐ด) ยท 3)) +
3)) |
23 | 3, 3, 13 | mulassd 11186 |
. . . . . . . . 9
โข (๐ โ ((3 ยท 3) ยท
๐ด) = (3 ยท (3
ยท ๐ด))) |
24 | 23 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) ยท 3) +
((3 ยท 3) ยท ๐ด)) = ((((3โ2) ยท (๐ดโ2)) ยท 3) + (3
ยท (3 ยท ๐ด)))) |
25 | 24 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) ยท 3) +
((3 ยท 3) ยท ๐ด)) + 3) = (((((3โ2) ยท (๐ดโ2)) ยท 3) + (3
ยท (3 ยท ๐ด))) +
3)) |
26 | 11, 3 | mulcomd 11184 |
. . . . . . . . . . 11
โข (๐ โ ((๐ดโ2) ยท 3) = (3 ยท (๐ดโ2))) |
27 | 26 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ ((3โ2) ยท
((๐ดโ2) ยท 3)) =
((3โ2) ยท (3 ยท (๐ดโ2)))) |
28 | 27 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ (((3โ2) ยท
((๐ดโ2) ยท 3)) +
((3 ยท 3) ยท ๐ด)) = (((3โ2) ยท (3 ยท
(๐ดโ2))) + ((3 ยท
3) ยท ๐ด))) |
29 | 28 | oveq1d 7376 |
. . . . . . . 8
โข (๐ โ ((((3โ2) ยท
((๐ดโ2) ยท 3)) +
((3 ยท 3) ยท ๐ด)) + 3) = ((((3โ2) ยท (3 ยท
(๐ดโ2))) + ((3 ยท
3) ยท ๐ด)) +
3)) |
30 | 6, 11, 3 | mulassd 11186 |
. . . . . . . . . 10
โข (๐ โ (((3โ2) ยท
(๐ดโ2)) ยท 3) =
((3โ2) ยท ((๐ดโ2) ยท 3))) |
31 | 30 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) ยท 3) +
((3 ยท 3) ยท ๐ด)) = (((3โ2) ยท ((๐ดโ2) ยท 3)) + ((3
ยท 3) ยท ๐ด))) |
32 | 31 | oveq1d 7376 |
. . . . . . . 8
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) ยท 3) +
((3 ยท 3) ยท ๐ด)) + 3) = ((((3โ2) ยท ((๐ดโ2) ยท 3)) + ((3
ยท 3) ยท ๐ด)) +
3)) |
33 | | df-3 12225 |
. . . . . . . . . . . . . . . 16
โข 3 = (2 +
1) |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 3 = (2 +
1)) |
35 | 34 | oveq2d 7377 |
. . . . . . . . . . . . . 14
โข (๐ โ (3โ3) = (3โ(2 +
1))) |
36 | 35 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ ((3โ3) ยท
(๐ดโ2)) = ((3โ(2 +
1)) ยท (๐ดโ2))) |
37 | 36 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ โ (((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) = (((3โ(2
+ 1)) ยท (๐ดโ2))
+ ((3โ2) ยท ๐ด))) |
38 | 37 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
((((3โ(2 + 1)) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) |
39 | | 2nn0 12438 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ0 |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ0) |
41 | 3, 40 | expp1d 14061 |
. . . . . . . . . . . . . 14
โข (๐ โ (3โ(2 + 1)) =
((3โ2) ยท 3)) |
42 | 41 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ ((3โ(2 + 1)) ยท
(๐ดโ2)) = (((3โ2)
ยท 3) ยท (๐ดโ2))) |
43 | 42 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ โ (((3โ(2 + 1))
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) =
((((3โ2) ยท 3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด))) |
44 | 43 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ โ ((((3โ(2 + 1))
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3) = (((((3โ2) ยท 3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) |
45 | 38, 44 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
(((((3โ2) ยท 3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3)) |
46 | 3 | sqvald 14057 |
. . . . . . . . . . . . 13
โข (๐ โ (3โ2) = (3 ยท
3)) |
47 | 46 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ โ ((3โ2) ยท ๐ด) = ((3 ยท 3) ยท
๐ด)) |
48 | 47 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((((3โ2) ยท 3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) =
((((3โ2) ยท 3) ยท (๐ดโ2)) + ((3 ยท 3) ยท ๐ด))) |
49 | 48 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ (((((3โ2) ยท 3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3) = (((((3โ2) ยท 3) ยท (๐ดโ2)) + ((3 ยท 3) ยท ๐ด)) + 3)) |
50 | 45, 49 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
(((((3โ2) ยท 3) ยท (๐ดโ2)) + ((3 ยท 3) ยท ๐ด)) + 3)) |
51 | 6, 3, 11 | mulassd 11186 |
. . . . . . . . . . 11
โข (๐ โ (((3โ2) ยท 3)
ยท (๐ดโ2)) =
((3โ2) ยท (3 ยท (๐ดโ2)))) |
52 | 51 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ ((((3โ2) ยท 3)
ยท (๐ดโ2)) + ((3
ยท 3) ยท ๐ด)) =
(((3โ2) ยท (3 ยท (๐ดโ2))) + ((3 ยท 3) ยท ๐ด))) |
53 | 52 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ (((((3โ2) ยท 3)
ยท (๐ดโ2)) + ((3
ยท 3) ยท ๐ด)) +
3) = ((((3โ2) ยท (3 ยท (๐ดโ2))) + ((3 ยท 3) ยท ๐ด)) + 3)) |
54 | 50, 53 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
((((3โ2) ยท (3 ยท (๐ดโ2))) + ((3 ยท 3) ยท ๐ด)) + 3)) |
55 | 29, 32, 54 | 3eqtr4rd 2784 |
. . . . . . 7
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
(((((3โ2) ยท (๐ดโ2)) ยท 3) + ((3 ยท 3)
ยท ๐ด)) +
3)) |
56 | 13, 3 | mulcomd 11184 |
. . . . . . . . . 10
โข (๐ โ (๐ด ยท 3) = (3 ยท ๐ด)) |
57 | 56 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (3 ยท (๐ด ยท 3)) = (3 ยท (3
ยท ๐ด))) |
58 | 57 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) ยท 3) +
(3 ยท (๐ด ยท
3))) = ((((3โ2) ยท (๐ดโ2)) ยท 3) + (3 ยท (3
ยท ๐ด)))) |
59 | 58 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) ยท 3) +
(3 ยท (๐ด ยท
3))) + 3) = (((((3โ2) ยท (๐ดโ2)) ยท 3) + (3 ยท (3
ยท ๐ด))) +
3)) |
60 | 25, 55, 59 | 3eqtr4d 2783 |
. . . . . 6
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
(((((3โ2) ยท (๐ดโ2)) ยท 3) + (3 ยท (๐ด ยท 3))) +
3)) |
61 | 20, 22, 60 | 3eqtr4rd 2784 |
. . . . 5
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
(((((3โ2) ยท (๐ดโ2)) + (3 ยท ๐ด)) ยท 3) + 3)) |
62 | 5, 17, 61 | 3eqtr4rd 2784 |
. . . 4
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) =
(((((3โ2) ยท (๐ดโ2)) + (3 ยท ๐ด)) + 1) ยท 3)) |
63 | 14 | mulid1d 11180 |
. . . . . . . . . 10
โข (๐ โ ((3 ยท ๐ด) ยท 1) = (3 ยท
๐ด)) |
64 | 63 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (2 ยท ((3 ยท
๐ด) ยท 1)) = (2
ยท (3 ยท ๐ด))) |
65 | 64 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ (((3 ยท ๐ด)โ2) + (2 ยท ((3
ยท ๐ด) ยท 1))) =
(((3 ยท ๐ด)โ2) +
(2 ยท (3 ยท ๐ด)))) |
66 | 65 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ ((((3 ยท ๐ด)โ2) + (2 ยท ((3
ยท ๐ด) ยท 1))) +
(1โ2)) = ((((3 ยท ๐ด)โ2) + (2 ยท (3 ยท ๐ด))) +
(1โ2))) |
67 | 66 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((((3 ยท ๐ด)โ2) + (2 ยท ((3
ยท ๐ด) ยท 1))) +
(1โ2)) โ (3 ยท ๐ด)) = (((((3 ยท ๐ด)โ2) + (2 ยท (3 ยท ๐ด))) + (1โ2)) โ (3
ยท ๐ด))) |
68 | 14, 16 | binom2d 41049 |
. . . . . . 7
โข (๐ โ (((3 ยท ๐ด) + 1)โ2) = ((((3 ยท
๐ด)โ2) + (2 ยท
((3 ยท ๐ด) ยท
1))) + (1โ2))) |
69 | 68 | oveq1d 7376 |
. . . . . 6
โข (๐ โ ((((3 ยท ๐ด) + 1)โ2) โ (3
ยท ๐ด)) = (((((3
ยท ๐ด)โ2) + (2
ยท ((3 ยท ๐ด)
ยท 1))) + (1โ2)) โ (3 ยท ๐ด))) |
70 | 14 | 2timesd 12404 |
. . . . . . . . . 10
โข (๐ โ (2 ยท (3 ยท
๐ด)) = ((3 ยท ๐ด) + (3 ยท ๐ด))) |
71 | 70 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (((3 ยท ๐ด)โ2) + (2 ยท (3
ยท ๐ด))) = (((3
ยท ๐ด)โ2) + ((3
ยท ๐ด) + (3 ยท
๐ด)))) |
72 | 71 | oveq1d 7376 |
. . . . . . . 8
โข (๐ โ ((((3 ยท ๐ด)โ2) + (2 ยท (3
ยท ๐ด))) + 1) = ((((3
ยท ๐ด)โ2) + ((3
ยท ๐ด) + (3 ยท
๐ด))) + 1)) |
73 | 72 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((((3 ยท ๐ด)โ2) + (2 ยท (3
ยท ๐ด))) + 1) โ
(3 ยท ๐ด)) = (((((3
ยท ๐ด)โ2) + ((3
ยท ๐ด) + (3 ยท
๐ด))) + 1) โ (3
ยท ๐ด))) |
74 | | sq1 14108 |
. . . . . . . . . 10
โข
(1โ2) = 1 |
75 | 74 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (1โ2) =
1) |
76 | 75 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((((3 ยท ๐ด)โ2) + (2 ยท (3
ยท ๐ด))) + (1โ2))
= ((((3 ยท ๐ด)โ2)
+ (2 ยท (3 ยท ๐ด))) + 1)) |
77 | 76 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((((3 ยท ๐ด)โ2) + (2 ยท (3
ยท ๐ด))) + (1โ2))
โ (3 ยท ๐ด)) =
(((((3 ยท ๐ด)โ2)
+ (2 ยท (3 ยท ๐ด))) + 1) โ (3 ยท ๐ด))) |
78 | 14, 16 | addcomd 11365 |
. . . . . . . . . . 11
โข (๐ โ ((3 ยท ๐ด) + 1) = (1 + (3 ยท ๐ด))) |
79 | 78 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ ((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + ((3 ยท ๐ด) + 1)) = ((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (1 + (3 ยท ๐ด)))) |
80 | 79 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + ((3 ยท ๐ด) + 1)) โ (3 ยท
๐ด)) = (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (1 + (3 ยท ๐ด))) โ (3 ยท ๐ด))) |
81 | 3, 13 | sqmuld 14072 |
. . . . . . . . . . . . 13
โข (๐ โ ((3 ยท ๐ด)โ2) = ((3โ2) ยท
(๐ดโ2))) |
82 | 81, 12 | eqeltrd 2834 |
. . . . . . . . . . . 12
โข (๐ โ ((3 ยท ๐ด)โ2) โ
โ) |
83 | 82, 14 | addcld 11182 |
. . . . . . . . . . 11
โข (๐ โ (((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) โ
โ) |
84 | 83, 14, 16 | addassd 11185 |
. . . . . . . . . 10
โข (๐ โ (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (3 ยท ๐ด)) + 1) = ((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + ((3 ยท ๐ด) + 1))) |
85 | 84 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ ((((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (3 ยท ๐ด)) + 1) โ (3 ยท
๐ด)) = (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + ((3 ยท ๐ด) + 1)) โ (3 ยท
๐ด))) |
86 | 15, 16 | addcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) โ
โ) |
87 | 86, 14, 14 | addsubassd 11540 |
. . . . . . . . . . 11
โข (๐ โ ((((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) + (3 ยท
๐ด)) โ (3 ยท
๐ด)) = (((((3โ2)
ยท (๐ดโ2)) + (3
ยท ๐ด)) + 1) + ((3
ยท ๐ด) โ (3
ยท ๐ด)))) |
88 | 81 | oveq1d 7376 |
. . . . . . . . . . . . . 14
โข (๐ โ (((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) = (((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด))) |
89 | 88 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ ((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + 1) = ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1)) |
90 | 89 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ โ (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + 1) + (3 ยท ๐ด)) = (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) + (3 ยท
๐ด))) |
91 | 90 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ โ ((((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + 1) + (3 ยท ๐ด)) โ (3 ยท ๐ด)) = ((((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) + (3 ยท
๐ด)) โ (3 ยท
๐ด))) |
92 | 14 | subidd 11508 |
. . . . . . . . . . . . 13
โข (๐ โ ((3 ยท ๐ด) โ (3 ยท ๐ด)) = 0) |
93 | 92 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) + ((3 ยท
๐ด) โ (3 ยท
๐ด))) = (((((3โ2)
ยท (๐ดโ2)) + (3
ยท ๐ด)) + 1) +
0)) |
94 | 86 | addid1d 11363 |
. . . . . . . . . . . 12
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) + 0) =
((((3โ2) ยท (๐ดโ2)) + (3 ยท ๐ด)) + 1)) |
95 | 93, 94 | eqtr2d 2774 |
. . . . . . . . . . 11
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = (((((3โ2)
ยท (๐ดโ2)) + (3
ยท ๐ด)) + 1) + ((3
ยท ๐ด) โ (3
ยท ๐ด)))) |
96 | 87, 91, 95 | 3eqtr4rd 2784 |
. . . . . . . . . 10
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = ((((((3 ยท
๐ด)โ2) + (3 ยท
๐ด)) + 1) + (3 ยท
๐ด)) โ (3 ยท
๐ด))) |
97 | 83, 16, 14 | addassd 11185 |
. . . . . . . . . . 11
โข (๐ โ (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + 1) + (3 ยท ๐ด)) = ((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (1 + (3 ยท ๐ด)))) |
98 | 97 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ ((((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + 1) + (3 ยท ๐ด)) โ (3 ยท ๐ด)) = (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (1 + (3 ยท ๐ด))) โ (3 ยท ๐ด))) |
99 | 96, 98 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = (((((3 ยท
๐ด)โ2) + (3 ยท
๐ด)) + (1 + (3 ยท
๐ด))) โ (3 ยท
๐ด))) |
100 | 80, 85, 99 | 3eqtr4rd 2784 |
. . . . . . . 8
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = ((((((3 ยท
๐ด)โ2) + (3 ยท
๐ด)) + (3 ยท ๐ด)) + 1) โ (3 ยท
๐ด))) |
101 | 82, 14, 14 | addassd 11185 |
. . . . . . . . . 10
โข (๐ โ ((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (3 ยท ๐ด)) = (((3 ยท ๐ด)โ2) + ((3 ยท ๐ด) + (3 ยท ๐ด)))) |
102 | 101 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ (((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (3 ยท ๐ด)) + 1) = ((((3 ยท ๐ด)โ2) + ((3 ยท ๐ด) + (3 ยท ๐ด))) + 1)) |
103 | 102 | oveq1d 7376 |
. . . . . . . 8
โข (๐ โ ((((((3 ยท ๐ด)โ2) + (3 ยท ๐ด)) + (3 ยท ๐ด)) + 1) โ (3 ยท
๐ด)) = (((((3 ยท ๐ด)โ2) + ((3 ยท ๐ด) + (3 ยท ๐ด))) + 1) โ (3 ยท
๐ด))) |
104 | 100, 103 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = (((((3 ยท
๐ด)โ2) + ((3 ยท
๐ด) + (3 ยท ๐ด))) + 1) โ (3 ยท
๐ด))) |
105 | 73, 77, 104 | 3eqtr4rd 2784 |
. . . . . 6
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = (((((3 ยท
๐ด)โ2) + (2 ยท (3
ยท ๐ด))) + (1โ2))
โ (3 ยท ๐ด))) |
106 | 67, 69, 105 | 3eqtr4rd 2784 |
. . . . 5
โข (๐ โ ((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) = ((((3 ยท
๐ด) + 1)โ2) โ (3
ยท ๐ด))) |
107 | 106 | oveq1d 7376 |
. . . 4
โข (๐ โ (((((3โ2) ยท
(๐ดโ2)) + (3 ยท
๐ด)) + 1) ยท 3) =
(((((3 ยท ๐ด) +
1)โ2) โ (3 ยท ๐ด)) ยท 3)) |
108 | 62, 107 | eqtrd 2773 |
. . 3
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) = (((((3
ยท ๐ด) + 1)โ2)
โ (3 ยท ๐ด))
ยท 3)) |
109 | 2, 9 | remulcld 11193 |
. . . . . . . 8
โข (๐ โ (3 ยท ๐ด) โ
โ) |
110 | | peano2re 11336 |
. . . . . . . 8
โข ((3
ยท ๐ด) โ โ
โ ((3 ยท ๐ด) + 1)
โ โ) |
111 | 109, 110 | syl 17 |
. . . . . . 7
โข (๐ โ ((3 ยท ๐ด) + 1) โ
โ) |
112 | 111 | resqcld 14039 |
. . . . . 6
โข (๐ โ (((3 ยท ๐ด) + 1)โ2) โ
โ) |
113 | 112, 109 | resubcld 11591 |
. . . . 5
โข (๐ โ ((((3 ยท ๐ด) + 1)โ2) โ (3
ยท ๐ด)) โ
โ) |
114 | 113 | recnd 11191 |
. . . 4
โข (๐ โ ((((3 ยท ๐ด) + 1)โ2) โ (3
ยท ๐ด)) โ
โ) |
115 | | 3nn 12240 |
. . . . . . . 8
โข 3 โ
โ |
116 | | nnq 12895 |
. . . . . . . 8
โข (3 โ
โ โ 3 โ โ) |
117 | 115, 116 | ax-mp 5 |
. . . . . . 7
โข 3 โ
โ |
118 | | qmulcl 12900 |
. . . . . . 7
โข ((3
โ โ โง ๐ด
โ โ) โ (3 ยท ๐ด) โ โ) |
119 | 117, 7, 118 | sylancr 588 |
. . . . . 6
โข (๐ โ (3 ยท ๐ด) โ
โ) |
120 | 119 | 3cubeslem1 41054 |
. . . . 5
โข (๐ โ 0 < ((((3 ยท
๐ด) + 1)โ2) โ (3
ยท ๐ด))) |
121 | 120 | gt0ne0d 11727 |
. . . 4
โข (๐ โ ((((3 ยท ๐ด) + 1)โ2) โ (3
ยท ๐ด)) โ
0) |
122 | | 3ne0 12267 |
. . . . 5
โข 3 โ
0 |
123 | 122 | a1i 11 |
. . . 4
โข (๐ โ 3 โ 0) |
124 | 114, 3, 121, 123 | mulne0d 11815 |
. . 3
โข (๐ โ (((((3 ยท ๐ด) + 1)โ2) โ (3
ยท ๐ด)) ยท 3)
โ 0) |
125 | 108, 124 | eqnetrd 3008 |
. 2
โข (๐ โ ((((3โ3) ยท
(๐ดโ2)) + ((3โ2)
ยท ๐ด)) + 3) โ
0) |
126 | 125 | neneqd 2945 |
1
โข (๐ โ ยฌ ((((3โ3)
ยท (๐ดโ2)) +
((3โ2) ยท ๐ด)) +
3) = 0) |