Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . . . 6
โข (๐ = ((2 ยท ๐) + 1) โ (๐โ2) = (((2 ยท ๐) + 1)โ2)) |
2 | | 2z 12542 |
. . . . . . . . . 10
โข 2 โ
โค |
3 | 2 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โค โ 2 โ
โค) |
4 | | id 22 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โค) |
5 | 3, 4 | zmulcld 12620 |
. . . . . . . 8
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
6 | 5 | zcnd 12615 |
. . . . . . 7
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
7 | | binom21 14129 |
. . . . . . 7
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐) +
1)โ2) = ((((2 ยท ๐)โ2) + (2 ยท (2 ยท ๐))) + 1)) |
8 | 6, 7 | syl 17 |
. . . . . 6
โข (๐ โ โค โ (((2
ยท ๐) + 1)โ2) =
((((2 ยท ๐)โ2) +
(2 ยท (2 ยท ๐))) + 1)) |
9 | 1, 8 | sylan9eqr 2799 |
. . . . 5
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (๐โ2) = ((((2 ยท ๐)โ2) + (2 ยท (2
ยท ๐))) +
1)) |
10 | 9 | oveq1d 7377 |
. . . 4
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ ((๐โ2) โ 1) = (((((2
ยท ๐)โ2) + (2
ยท (2 ยท ๐))) +
1) โ 1)) |
11 | | 2cnd 12238 |
. . . . . . . . . . 11
โข (๐ โ โค โ 2 โ
โ) |
12 | | zcn 12511 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
13 | 11, 12 | sqmuld 14070 |
. . . . . . . . . 10
โข (๐ โ โค โ ((2
ยท ๐)โ2) =
((2โ2) ยท (๐โ2))) |
14 | | sq2 14108 |
. . . . . . . . . . . 12
โข
(2โ2) = 4 |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โค โ
(2โ2) = 4) |
16 | 15 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ โค โ
((2โ2) ยท (๐โ2)) = (4 ยท (๐โ2))) |
17 | 13, 16 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ โค โ ((2
ยท ๐)โ2) = (4
ยท (๐โ2))) |
18 | | mulass 11146 |
. . . . . . . . . . . 12
โข ((2
โ โ โง 2 โ โ โง ๐ โ โ) โ ((2 ยท 2)
ยท ๐) = (2 ยท
(2 ยท ๐))) |
19 | 18 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((2
โ โ โง 2 โ โ โง ๐ โ โ) โ (2 ยท (2
ยท ๐)) = ((2 ยท
2) ยท ๐)) |
20 | 11, 11, 12, 19 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ โค โ (2
ยท (2 ยท ๐)) =
((2 ยท 2) ยท ๐)) |
21 | | 2t2e4 12324 |
. . . . . . . . . . . 12
โข (2
ยท 2) = 4 |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โค โ (2
ยท 2) = 4) |
23 | 22 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ โค โ ((2
ยท 2) ยท ๐) =
(4 ยท ๐)) |
24 | 20, 23 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ โค โ (2
ยท (2 ยท ๐)) =
(4 ยท ๐)) |
25 | 17, 24 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ โค โ (((2
ยท ๐)โ2) + (2
ยท (2 ยท ๐))) =
((4 ยท (๐โ2)) +
(4 ยท ๐))) |
26 | 25 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ โค โ ((((2
ยท ๐)โ2) + (2
ยท (2 ยท ๐))) +
1) = (((4 ยท (๐โ2)) + (4 ยท ๐)) + 1)) |
27 | 26 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โค โ (((((2
ยท ๐)โ2) + (2
ยท (2 ยท ๐))) +
1) โ 1) = ((((4 ยท (๐โ2)) + (4 ยท ๐)) + 1) โ 1)) |
28 | | 4z 12544 |
. . . . . . . . . . 11
โข 4 โ
โค |
29 | 28 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โค โ 4 โ
โค) |
30 | | zsqcl 14041 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐โ2) โ
โค) |
31 | 29, 30 | zmulcld 12620 |
. . . . . . . . 9
โข (๐ โ โค โ (4
ยท (๐โ2)) โ
โค) |
32 | 31 | zcnd 12615 |
. . . . . . . 8
โข (๐ โ โค โ (4
ยท (๐โ2)) โ
โ) |
33 | 29, 4 | zmulcld 12620 |
. . . . . . . . 9
โข (๐ โ โค โ (4
ยท ๐) โ
โค) |
34 | 33 | zcnd 12615 |
. . . . . . . 8
โข (๐ โ โค โ (4
ยท ๐) โ
โ) |
35 | 32, 34 | addcld 11181 |
. . . . . . 7
โข (๐ โ โค โ ((4
ยท (๐โ2)) + (4
ยท ๐)) โ
โ) |
36 | | pncan1 11586 |
. . . . . . 7
โข (((4
ยท (๐โ2)) + (4
ยท ๐)) โ โ
โ ((((4 ยท (๐โ2)) + (4 ยท ๐)) + 1) โ 1) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
37 | 35, 36 | syl 17 |
. . . . . 6
โข (๐ โ โค โ ((((4
ยท (๐โ2)) + (4
ยท ๐)) + 1) โ
1) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
38 | 27, 37 | eqtrd 2777 |
. . . . 5
โข (๐ โ โค โ (((((2
ยท ๐)โ2) + (2
ยท (2 ยท ๐))) +
1) โ 1) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
39 | 38 | adantr 482 |
. . . 4
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (((((2 ยท
๐)โ2) + (2 ยท (2
ยท ๐))) + 1) โ
1) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
40 | 10, 39 | eqtrd 2777 |
. . 3
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ ((๐โ2) โ 1) = ((4
ยท (๐โ2)) + (4
ยท ๐))) |
41 | 40 | oveq1d 7377 |
. 2
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (((๐โ2) โ 1) / 8) = (((4
ยท (๐โ2)) + (4
ยท ๐)) /
8)) |
42 | | 4cn 12245 |
. . . . . . 7
โข 4 โ
โ |
43 | 42 | a1i 11 |
. . . . . 6
โข (๐ โ โค โ 4 โ
โ) |
44 | 30 | zcnd 12615 |
. . . . . 6
โข (๐ โ โค โ (๐โ2) โ
โ) |
45 | 43, 44, 12 | adddid 11186 |
. . . . 5
โข (๐ โ โค โ (4
ยท ((๐โ2) +
๐)) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
46 | 45 | eqcomd 2743 |
. . . 4
โข (๐ โ โค โ ((4
ยท (๐โ2)) + (4
ยท ๐)) = (4 ยท
((๐โ2) + ๐))) |
47 | 46 | oveq1d 7377 |
. . 3
โข (๐ โ โค โ (((4
ยท (๐โ2)) + (4
ยท ๐)) / 8) = ((4
ยท ((๐โ2) +
๐)) / 8)) |
48 | 47 | adantr 482 |
. 2
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (((4 ยท
(๐โ2)) + (4 ยท
๐)) / 8) = ((4 ยท
((๐โ2) + ๐)) / 8)) |
49 | | 4t2e8 12328 |
. . . . . . 7
โข (4
ยท 2) = 8 |
50 | 49 | a1i 11 |
. . . . . 6
โข (๐ โ โค โ (4
ยท 2) = 8) |
51 | 50 | eqcomd 2743 |
. . . . 5
โข (๐ โ โค โ 8 = (4
ยท 2)) |
52 | 51 | oveq2d 7378 |
. . . 4
โข (๐ โ โค โ ((4
ยท ((๐โ2) +
๐)) / 8) = ((4 ยท
((๐โ2) + ๐)) / (4 ยท
2))) |
53 | 30, 4 | zaddcld 12618 |
. . . . . 6
โข (๐ โ โค โ ((๐โ2) + ๐) โ โค) |
54 | 53 | zcnd 12615 |
. . . . 5
โข (๐ โ โค โ ((๐โ2) + ๐) โ โ) |
55 | | 2cnne0 12370 |
. . . . . 6
โข (2 โ
โ โง 2 โ 0) |
56 | 55 | a1i 11 |
. . . . 5
โข (๐ โ โค โ (2 โ
โ โง 2 โ 0)) |
57 | | 4ne0 12268 |
. . . . . . 7
โข 4 โ
0 |
58 | 42, 57 | pm3.2i 472 |
. . . . . 6
โข (4 โ
โ โง 4 โ 0) |
59 | 58 | a1i 11 |
. . . . 5
โข (๐ โ โค โ (4 โ
โ โง 4 โ 0)) |
60 | | divcan5 11864 |
. . . . 5
โข ((((๐โ2) + ๐) โ โ โง (2 โ โ
โง 2 โ 0) โง (4 โ โ โง 4 โ 0)) โ ((4 ยท
((๐โ2) + ๐)) / (4 ยท 2)) = (((๐โ2) + ๐) / 2)) |
61 | 54, 56, 59, 60 | syl3anc 1372 |
. . . 4
โข (๐ โ โค โ ((4
ยท ((๐โ2) +
๐)) / (4 ยท 2)) =
(((๐โ2) + ๐) / 2)) |
62 | 12 | sqvald 14055 |
. . . . . . 7
โข (๐ โ โค โ (๐โ2) = (๐ ยท ๐)) |
63 | 62 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โค โ ((๐โ2) + ๐) = ((๐ ยท ๐) + ๐)) |
64 | 12 | mulid1d 11179 |
. . . . . . . 8
โข (๐ โ โค โ (๐ ยท 1) = ๐) |
65 | 64 | eqcomd 2743 |
. . . . . . 7
โข (๐ โ โค โ ๐ = (๐ ยท 1)) |
66 | 65 | oveq2d 7378 |
. . . . . 6
โข (๐ โ โค โ ((๐ ยท ๐) + ๐) = ((๐ ยท ๐) + (๐ ยท 1))) |
67 | | 1cnd 11157 |
. . . . . . 7
โข (๐ โ โค โ 1 โ
โ) |
68 | | adddi 11147 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ (๐ ยท
(๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
69 | 68 | eqcomd 2743 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ ((๐
ยท ๐) + (๐ ยท 1)) = (๐ ยท (๐ + 1))) |
70 | 12, 12, 67, 69 | syl3anc 1372 |
. . . . . 6
โข (๐ โ โค โ ((๐ ยท ๐) + (๐ ยท 1)) = (๐ ยท (๐ + 1))) |
71 | 63, 66, 70 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ โค โ ((๐โ2) + ๐) = (๐ ยท (๐ + 1))) |
72 | 71 | oveq1d 7377 |
. . . 4
โข (๐ โ โค โ (((๐โ2) + ๐) / 2) = ((๐ ยท (๐ + 1)) / 2)) |
73 | 52, 61, 72 | 3eqtrd 2781 |
. . 3
โข (๐ โ โค โ ((4
ยท ((๐โ2) +
๐)) / 8) = ((๐ ยท (๐ + 1)) / 2)) |
74 | 73 | adantr 482 |
. 2
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ ((4 ยท
((๐โ2) + ๐)) / 8) = ((๐ ยท (๐ + 1)) / 2)) |
75 | 41, 48, 74 | 3eqtrd 2781 |
1
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (((๐โ2) โ 1) / 8) =
((๐ ยท (๐ + 1)) / 2)) |