Step | Hyp | Ref
| Expression |
1 | | perfectlem.2 |
. . . 4
โข (๐ โ ๐ต โ โ) |
2 | | 1red 11212 |
. . . . 5
โข (๐ โ 1 โ
โ) |
3 | | perfectlem.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
4 | | perfectlem.3 |
. . . . . . . 8
โข (๐ โ ยฌ 2 โฅ ๐ต) |
5 | | perfectlem.4 |
. . . . . . . 8
โข (๐ โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = (2 ยท ((2โ๐ด) ยท ๐ต))) |
6 | 3, 1, 4, 5 | perfectlem1 26722 |
. . . . . . 7
โข (๐ โ ((2โ(๐ด + 1)) โ โ โง
((2โ(๐ด + 1)) โ
1) โ โ โง (๐ต
/ ((2โ(๐ด + 1)) โ
1)) โ โ)) |
7 | 6 | simp3d 1145 |
. . . . . 6
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
8 | 7 | nnred 12224 |
. . . . 5
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
9 | 1 | nnred 12224 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
10 | 7 | nnge1d 12257 |
. . . . 5
โข (๐ โ 1 โค (๐ต / ((2โ(๐ด + 1)) โ 1))) |
11 | | 2cn 12284 |
. . . . . . . . . . 11
โข 2 โ
โ |
12 | | exp1 14030 |
. . . . . . . . . . 11
โข (2 โ
โ โ (2โ1) = 2) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
โข
(2โ1) = 2 |
14 | | df-2 12272 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
15 | 13, 14 | eqtri 2761 |
. . . . . . . . 9
โข
(2โ1) = (1 + 1) |
16 | | 2re 12283 |
. . . . . . . . . . 11
โข 2 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
18 | | 1zzd 12590 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โค) |
19 | 3 | peano2nnd 12226 |
. . . . . . . . . . 11
โข (๐ โ (๐ด + 1) โ โ) |
20 | 19 | nnzd 12582 |
. . . . . . . . . 10
โข (๐ โ (๐ด + 1) โ โค) |
21 | | 1lt2 12380 |
. . . . . . . . . . 11
โข 1 <
2 |
22 | 21 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 1 < 2) |
23 | | 1re 11211 |
. . . . . . . . . . . 12
โข 1 โ
โ |
24 | 3 | nnrpd 13011 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ
โ+) |
25 | | ltaddrp 13008 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐ด
โ โ+) โ 1 < (1 + ๐ด)) |
26 | 23, 24, 25 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ 1 < (1 + ๐ด)) |
27 | | ax-1cn 11165 |
. . . . . . . . . . . 12
โข 1 โ
โ |
28 | 3 | nncnd 12225 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
29 | | addcom 11397 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + ๐ด) = (๐ด + 1)) |
30 | 27, 28, 29 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (1 + ๐ด) = (๐ด + 1)) |
31 | 26, 30 | breqtrd 5174 |
. . . . . . . . . 10
โข (๐ โ 1 < (๐ด + 1)) |
32 | | ltexp2a 14128 |
. . . . . . . . . 10
โข (((2
โ โ โง 1 โ โค โง (๐ด + 1) โ โค) โง (1 < 2 โง
1 < (๐ด + 1))) โ
(2โ1) < (2โ(๐ด
+ 1))) |
33 | 17, 18, 20, 22, 31, 32 | syl32anc 1379 |
. . . . . . . . 9
โข (๐ โ (2โ1) <
(2โ(๐ด +
1))) |
34 | 15, 33 | eqbrtrrid 5184 |
. . . . . . . 8
โข (๐ โ (1 + 1) <
(2โ(๐ด +
1))) |
35 | 6 | simp1d 1143 |
. . . . . . . . . 10
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
36 | 35 | nnred 12224 |
. . . . . . . . 9
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
37 | 2, 2, 36 | ltaddsubd 11811 |
. . . . . . . 8
โข (๐ โ ((1 + 1) <
(2โ(๐ด + 1)) โ 1
< ((2โ(๐ด + 1))
โ 1))) |
38 | 34, 37 | mpbid 231 |
. . . . . . 7
โข (๐ โ 1 < ((2โ(๐ด + 1)) โ
1)) |
39 | | 0lt1 11733 |
. . . . . . . . 9
โข 0 <
1 |
40 | 39 | a1i 11 |
. . . . . . . 8
โข (๐ โ 0 < 1) |
41 | | peano2rem 11524 |
. . . . . . . . 9
โข
((2โ(๐ด + 1))
โ โ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
42 | 36, 41 | syl 17 |
. . . . . . . 8
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
43 | | expgt1 14063 |
. . . . . . . . . 10
โข ((2
โ โ โง (๐ด +
1) โ โ โง 1 < 2) โ 1 < (2โ(๐ด + 1))) |
44 | 16, 19, 22, 43 | mp3an2i 1467 |
. . . . . . . . 9
โข (๐ โ 1 < (2โ(๐ด + 1))) |
45 | | posdif 11704 |
. . . . . . . . . 10
โข ((1
โ โ โง (2โ(๐ด + 1)) โ โ) โ (1 <
(2โ(๐ด + 1)) โ 0
< ((2โ(๐ด + 1))
โ 1))) |
46 | 23, 36, 45 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ (1 < (2โ(๐ด + 1)) โ 0 <
((2โ(๐ด + 1)) โ
1))) |
47 | 44, 46 | mpbid 231 |
. . . . . . . 8
โข (๐ โ 0 < ((2โ(๐ด + 1)) โ
1)) |
48 | 1 | nngt0d 12258 |
. . . . . . . 8
โข (๐ โ 0 < ๐ต) |
49 | | ltdiv2 12097 |
. . . . . . . 8
โข (((1
โ โ โง 0 < 1) โง (((2โ(๐ด + 1)) โ 1) โ โ โง 0
< ((2โ(๐ด + 1))
โ 1)) โง (๐ต โ
โ โง 0 < ๐ต))
โ (1 < ((2โ(๐ด
+ 1)) โ 1) โ (๐ต
/ ((2โ(๐ด + 1)) โ
1)) < (๐ต /
1))) |
50 | 2, 40, 42, 47, 9, 48, 49 | syl222anc 1387 |
. . . . . . 7
โข (๐ โ (1 < ((2โ(๐ด + 1)) โ 1) โ (๐ต / ((2โ(๐ด + 1)) โ 1)) < (๐ต / 1))) |
51 | 38, 50 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) < (๐ต / 1)) |
52 | 1 | nncnd 12225 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
53 | 52 | div1d 11979 |
. . . . . 6
โข (๐ โ (๐ต / 1) = ๐ต) |
54 | 51, 53 | breqtrd 5174 |
. . . . 5
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) < ๐ต) |
55 | 2, 8, 9, 10, 54 | lelttrd 11369 |
. . . 4
โข (๐ โ 1 < ๐ต) |
56 | | eluz2b2 12902 |
. . . 4
โข (๐ต โ
(โคโฅโ2) โ (๐ต โ โ โง 1 < ๐ต)) |
57 | 1, 55, 56 | sylanbrc 584 |
. . 3
โข (๐ โ ๐ต โ
(โคโฅโ2)) |
58 | | fzfid 13935 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐ต) โ Fin) |
59 | | dvdsssfz1 16258 |
. . . . . . . . . . . . 13
โข (๐ต โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ (1...๐ต)) |
60 | 1, 59 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ (1...๐ต)) |
61 | 58, 60 | ssfid 9264 |
. . . . . . . . . . 11
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ Fin) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ Fin) |
63 | | ssrab2 4077 |
. . . . . . . . . . . . 13
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ โ |
64 | 63 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ โ) |
65 | 64 | sselda 3982 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
66 | 65 | nnred 12224 |
. . . . . . . . . 10
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
67 | 65 | nnnn0d 12529 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ0) |
68 | 67 | nn0ge0d 12532 |
. . . . . . . . . 10
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ 0 โค ๐) |
69 | | df-tp 4633 |
. . . . . . . . . . . 12
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {๐}) |
70 | 7, 1 | prssd 4825 |
. . . . . . . . . . . . . 14
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ โ) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ โ) |
72 | | simplrl 776 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
73 | 72 | snssd 4812 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {๐} โ โ) |
74 | 71, 73 | unssd 4186 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {๐}) โ โ) |
75 | 69, 74 | eqsstrid 4030 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ โ) |
76 | 6 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
77 | 76 | nnzd 12582 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โค) |
78 | 7 | nnzd 12582 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โค) |
79 | | dvdsmul2 16219 |
. . . . . . . . . . . . . . . . 17
โข
((((2โ(๐ด + 1))
โ 1) โ โค โง (๐ต / ((2โ(๐ด + 1)) โ 1)) โ โค) โ
(๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ
(((2โ(๐ด + 1)) โ
1) ยท (๐ต /
((2โ(๐ด + 1)) โ
1)))) |
80 | 77, 78, 79 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ (((2โ(๐ด + 1)) โ 1) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1)))) |
81 | 76 | nncnd 12225 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
82 | 76 | nnne0d 12259 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
0) |
83 | 52, 81, 82 | divcan2d 11989 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท
(๐ต / ((2โ(๐ด + 1)) โ 1))) = ๐ต) |
84 | 80, 83 | breqtrd 5174 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ ๐ต) |
85 | | breq1 5151 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ (๐ฅ โฅ ๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ ๐ต)) |
86 | 84, 85 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ๐ฅ โฅ ๐ต)) |
87 | 86 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ๐ฅ โฅ ๐ต)) |
88 | 1 | nnzd 12582 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ โค) |
89 | | iddvds 16210 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ โค โ ๐ต โฅ ๐ต) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โฅ ๐ต) |
91 | | breq1 5151 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ต โ (๐ฅ โฅ ๐ต โ ๐ต โฅ ๐ต)) |
92 | 90, 91 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฅ = ๐ต โ ๐ฅ โฅ ๐ต)) |
93 | 92 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ = ๐ต โ ๐ฅ โฅ ๐ต)) |
94 | | simplrr 777 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โฅ ๐ต) |
95 | | breq1 5151 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (๐ฅ โฅ ๐ต โ ๐ โฅ ๐ต)) |
96 | 94, 95 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ = ๐ โ ๐ฅ โฅ ๐ต)) |
97 | 87, 93, 96 | 3jaod 1429 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ((๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = ๐) โ ๐ฅ โฅ ๐ต)) |
98 | | eltpi 4691 |
. . . . . . . . . . . 12
โข (๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = ๐)) |
99 | 97, 98 | impel 507 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}) โ ๐ฅ โฅ ๐ต) |
100 | 75, 99 | ssrabdv 4071 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) |
101 | 62, 66, 68, 100 | fsumless 15739 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}๐ โค ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
102 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
103 | | disjsn 4715 |
. . . . . . . . . . . 12
โข (({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {๐}) = โ
โ ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
104 | 102, 103 | sylibr 233 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {๐}) = โ
) |
105 | 69 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {๐})) |
106 | | tpfi 9320 |
. . . . . . . . . . . 12
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ Fin |
107 | 106 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ Fin) |
108 | 75 | sselda 3982 |
. . . . . . . . . . . 12
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}) โ ๐ โ โ) |
109 | 108 | nncnd 12225 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}) โ ๐ โ โ) |
110 | 104, 105,
107, 109 | fsumsplit 15684 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}๐ = (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {๐}๐)) |
111 | 7 | nncnd 12225 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
112 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ๐ = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
113 | 112 | sumsn 15689 |
. . . . . . . . . . . . . . 15
โข (((๐ต / ((2โ(๐ด + 1)) โ 1)) โ โ โง
(๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) โ ฮฃ๐
โ {(๐ต /
((2โ(๐ด + 1)) โ
1))}๐ = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
114 | 7, 111, 113 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1))}๐ = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
115 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ต โ ๐ = ๐ต) |
116 | 115 | sumsn 15689 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ โ โง ๐ต โ โ) โ
ฮฃ๐ โ {๐ต}๐ = ๐ต) |
117 | 1, 52, 116 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ {๐ต}๐ = ๐ต) |
118 | 114, 117 | oveq12d 7424 |
. . . . . . . . . . . . 13
โข (๐ โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1))}๐ + ฮฃ๐ โ {๐ต}๐) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ๐ต)) |
119 | | incom 4201 |
. . . . . . . . . . . . . . 15
โข ({๐ต} โฉ {(๐ต / ((2โ(๐ด + 1)) โ 1))}) = ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โฉ {๐ต}) |
120 | 8, 54 | gtned 11346 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1))) |
121 | | disjsn2 4716 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ({๐ต} โฉ {(๐ต / ((2โ(๐ด + 1)) โ 1))}) =
โ
) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ({๐ต} โฉ {(๐ต / ((2โ(๐ด + 1)) โ 1))}) =
โ
) |
123 | 119, 122 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
โข (๐ โ ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โฉ {๐ต}) = โ
) |
124 | | df-pr 4631 |
. . . . . . . . . . . . . . 15
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} = ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โช {๐ต}) |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} = ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โช {๐ต})) |
126 | | prfi 9319 |
. . . . . . . . . . . . . . 15
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ Fin |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ Fin) |
128 | 70 | sselda 3982 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
129 | 128 | nncnd 12225 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
130 | 123, 125,
127, 129 | fsumsplit 15684 |
. . . . . . . . . . . . 13
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ = (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1))}๐ + ฮฃ๐ โ {๐ต}๐)) |
131 | 81, 52 | mulcld 11231 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท ๐ต) โ
โ) |
132 | 52, 131, 81, 82 | divdird 12025 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) / ((2โ(๐ด + 1)) โ 1)) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ((((2โ(๐ด + 1)) โ 1) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)))) |
133 | 35 | nncnd 12225 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
134 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ 1 โ
โ) |
135 | 133, 134,
52 | subdird 11668 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท ๐ต) = (((2โ(๐ด + 1)) ยท ๐ต) โ (1 ยท ๐ต))) |
136 | 52 | mullidd 11229 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (1 ยท ๐ต) = ๐ต) |
137 | 136 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((2โ(๐ด + 1)) ยท ๐ต) โ (1 ยท ๐ต)) = (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต)) |
138 | 135, 137 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท ๐ต) = (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต)) |
139 | 138 | oveq2d 7422 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) = (๐ต + (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต))) |
140 | 133, 52 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) โ
โ) |
141 | 52, 140 | pncan3d 11571 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต + (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต)) = ((2โ(๐ด + 1)) ยท ๐ต)) |
142 | 139, 141 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) = ((2โ(๐ด + 1)) ยท ๐ต)) |
143 | 142 | oveq1d 7421 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) / ((2โ(๐ด + 1)) โ 1)) = (((2โ(๐ด + 1)) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1))) |
144 | 133, 52, 81, 82 | divassd 12022 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2โ(๐ด + 1)) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)) = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
145 | 143, 144 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) / ((2โ(๐ด + 1)) โ 1)) = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
146 | 52, 81, 82 | divcan3d 11992 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((((2โ(๐ด + 1)) โ 1) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)) = ๐ต) |
147 | 146 | oveq2d 7422 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ((((2โ(๐ด + 1)) โ 1) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1))) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ๐ต)) |
148 | 132, 145,
147 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ๐ต)) |
149 | 118, 130,
148 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
150 | 149 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
151 | 72 | nncnd 12225 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
152 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ๐ = ๐) |
153 | 152 | sumsn 15689 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
ฮฃ๐ โ {๐}๐ = ๐) |
154 | 151, 151,
153 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {๐}๐ = ๐) |
155 | 150, 154 | oveq12d 7424 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {๐}๐) = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐)) |
156 | 110, 155 | eqtrd 2773 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}๐ = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐)) |
157 | 3 | nnnn0d 12529 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ด โ
โ0) |
158 | | expp1 14031 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐ด
โ โ0) โ (2โ(๐ด + 1)) = ((2โ๐ด) ยท 2)) |
159 | 11, 157, 158 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2โ(๐ด + 1)) = ((2โ๐ด) ยท 2)) |
160 | | 2nn 12282 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
161 | | nnexpcl 14037 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐ด
โ โ0) โ (2โ๐ด) โ โ) |
162 | 160, 157,
161 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2โ๐ด) โ โ) |
163 | 162 | nncnd 12225 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2โ๐ด) โ โ) |
164 | | mulcom 11193 |
. . . . . . . . . . . . . . . . 17
โข
(((2โ๐ด) โ
โ โง 2 โ โ) โ ((2โ๐ด) ยท 2) = (2 ยท (2โ๐ด))) |
165 | 163, 11, 164 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2โ๐ด) ยท 2) = (2 ยท (2โ๐ด))) |
166 | 159, 165 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2โ(๐ด + 1)) = (2 ยท (2โ๐ด))) |
167 | 166 | oveq1d 7421 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) = ((2 ยท (2โ๐ด)) ยท ๐ต)) |
168 | | 2cnd 12287 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ) |
169 | 168, 163,
52 | mulassd 11234 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท (2โ๐ด)) ยท ๐ต) = (2 ยท ((2โ๐ด) ยท ๐ต))) |
170 | | 2prm 16626 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
171 | | coprm 16645 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐ต
โ โค) โ (ยฌ 2 โฅ ๐ต โ (2 gcd ๐ต) = 1)) |
172 | 170, 88, 171 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (ยฌ 2 โฅ ๐ต โ (2 gcd ๐ต) = 1)) |
173 | 4, 172 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 gcd ๐ต) = 1) |
174 | | 2z 12591 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โค |
175 | | rpexp1i 16657 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โค โง ๐ต
โ โค โง ๐ด
โ โ0) โ ((2 gcd ๐ต) = 1 โ ((2โ๐ด) gcd ๐ต) = 1)) |
176 | 174, 88, 157, 175 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 gcd ๐ต) = 1 โ ((2โ๐ด) gcd ๐ต) = 1)) |
177 | 173, 176 | mpd 15 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2โ๐ด) gcd ๐ต) = 1) |
178 | | sgmmul 26694 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ((2โ๐ด) โ โ โง ๐ต โ โ โง ((2โ๐ด) gcd ๐ต) = 1)) โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต))) |
179 | 134, 162,
1, 177, 178 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต))) |
180 | | pncan 11463 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด + 1)
โ 1) = ๐ด) |
181 | 28, 27, 180 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ด + 1) โ 1) = ๐ด) |
182 | 181 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2โ((๐ด + 1) โ 1)) =
(2โ๐ด)) |
183 | 182 | oveq2d 7422 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 ฯ (2โ((๐ด + 1) โ 1))) = (1 ฯ
(2โ๐ด))) |
184 | | 1sgm2ppw 26693 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด + 1) โ โ โ (1
ฯ (2โ((๐ด + 1)
โ 1))) = ((2โ(๐ด
+ 1)) โ 1)) |
185 | 19, 184 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 ฯ (2โ((๐ด + 1) โ 1))) =
((2โ(๐ด + 1)) โ
1)) |
186 | 183, 185 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 ฯ (2โ๐ด)) = ((2โ(๐ด + 1)) โ 1)) |
187 | 186 | oveq1d 7421 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต)) = (((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต))) |
188 | 179, 5, 187 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 ยท ((2โ๐ด) ยท ๐ต)) = (((2โ(๐ด + 1)) โ 1) ยท (1 ฯ ๐ต))) |
189 | 167, 169,
188 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) = (((2โ(๐ด + 1)) โ 1) ยท (1 ฯ ๐ต))) |
190 | 189 | oveq1d 7421 |
. . . . . . . . . . . 12
โข (๐ โ (((2โ(๐ด + 1)) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)) = ((((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต)) /
((2โ(๐ด + 1)) โ
1))) |
191 | | 1nn0 12485 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ0 |
192 | | sgmnncl 26641 |
. . . . . . . . . . . . . . 15
โข ((1
โ โ0 โง ๐ต โ โ) โ (1 ฯ ๐ต) โ
โ) |
193 | 191, 1, 192 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (๐ โ (1 ฯ ๐ต) โ
โ) |
194 | 193 | nncnd 12225 |
. . . . . . . . . . . . 13
โข (๐ โ (1 ฯ ๐ต) โ
โ) |
195 | 194, 81, 82 | divcan3d 11992 |
. . . . . . . . . . . 12
โข (๐ โ ((((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต)) /
((2โ(๐ด + 1)) โ
1)) = (1 ฯ ๐ต)) |
196 | 190, 144,
195 | 3eqtr3d 2781 |
. . . . . . . . . . 11
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) = (1 ฯ ๐ต)) |
197 | | sgmval 26636 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐ต
โ โ) โ (1 ฯ ๐ต) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} (๐โ๐1)) |
198 | 27, 1, 197 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (1 ฯ ๐ต) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} (๐โ๐1)) |
199 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) |
200 | 63, 199 | sselid 3980 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
201 | 200 | nncnd 12225 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
202 | 201 | cxp1d 26206 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ (๐โ๐1) = ๐) |
203 | 202 | sumeq2dv 15646 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} (๐โ๐1) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
204 | 196, 198,
203 | 3eqtrrd 2778 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
205 | 204 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
206 | 101, 156,
205 | 3brtr3d 5179 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โค ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
207 | 36, 8 | remulcld 11241 |
. . . . . . . . . . 11
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) โ
โ) |
208 | 207 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) โ
โ) |
209 | 72 | nnrpd 13011 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ+) |
210 | 208, 209 | ltaddrpd 13046 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐)) |
211 | 72 | nnred 12224 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
212 | 208, 211 | readdcld 11240 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โ โ) |
213 | 208, 212 | ltnled 11358 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โ ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โค ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))))) |
214 | 210, 213 | mpbid 231 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โค ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
215 | 206, 214 | condan 817 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
216 | | elpri 4650 |
. . . . . . 7
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) |
217 | 215, 216 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) |
218 | 217 | expr 458 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต))) |
219 | 218 | ralrimiva 3147 |
. . . 4
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต))) |
220 | 2, 55 | gtned 11346 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ 1) |
221 | 220 | necomd 2997 |
. . . . . . . . 9
โข (๐ โ 1 โ ๐ต) |
222 | | 1dvds 16211 |
. . . . . . . . . . . . 13
โข (๐ต โ โค โ 1 โฅ
๐ต) |
223 | 88, 222 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 1 โฅ ๐ต) |
224 | | breq1 5151 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (๐ โฅ ๐ต โ 1 โฅ ๐ต)) |
225 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
226 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (๐ = ๐ต โ 1 = ๐ต)) |
227 | 225, 226 | orbi12d 918 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ ((๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต) โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต))) |
228 | 224, 227 | imbi12d 345 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ ((๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) โ (1 โฅ ๐ต โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต)))) |
229 | | 1nn 12220 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
230 | 229 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โ
โ) |
231 | 228, 219,
230 | rspcdva 3614 |
. . . . . . . . . . . 12
โข (๐ โ (1 โฅ ๐ต โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต))) |
232 | 223, 231 | mpd 15 |
. . . . . . . . . . 11
โข (๐ โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต)) |
233 | 232 | ord 863 |
. . . . . . . . . 10
โข (๐ โ (ยฌ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1 = ๐ต)) |
234 | 233 | necon1ad 2958 |
. . . . . . . . 9
โข (๐ โ (1 โ ๐ต โ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
235 | 221, 234 | mpd 15 |
. . . . . . . 8
โข (๐ โ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
236 | 235 | eqeq2d 2744 |
. . . . . . 7
โข (๐ โ (๐ = 1 โ ๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
237 | 236 | orbi1d 916 |
. . . . . 6
โข (๐ โ ((๐ = 1 โจ ๐ = ๐ต) โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต))) |
238 | 237 | imbi2d 341 |
. . . . 5
โข (๐ โ ((๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต)) โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)))) |
239 | 238 | ralbidv 3178 |
. . . 4
โข (๐ โ (โ๐ โ โ (๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต)) โ โ๐ โ โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)))) |
240 | 219, 239 | mpbird 257 |
. . 3
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต))) |
241 | | isprm2 16616 |
. . 3
โข (๐ต โ โ โ (๐ต โ
(โคโฅโ2) โง โ๐ โ โ (๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต)))) |
242 | 57, 240, 241 | sylanbrc 584 |
. 2
โข (๐ โ ๐ต โ โ) |
243 | 207 | ltp1d 12141 |
. . . 4
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
244 | | peano2re 11384 |
. . . . . 6
โข
(((2โ(๐ด + 1))
ยท (๐ต /
((2โ(๐ด + 1)) โ
1))) โ โ โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โ
โ) |
245 | 207, 244 | syl 17 |
. . . . 5
โข (๐ โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โ
โ) |
246 | 207, 245 | ltnled 11358 |
. . . 4
โข (๐ โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โ ยฌ
(((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1))))) |
247 | 243, 246 | mpbid 231 |
. . 3
โข (๐ โ ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1)))) |
248 | 200 | nnred 12224 |
. . . . . . . 8
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
249 | 200 | nnnn0d 12529 |
. . . . . . . . 9
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ0) |
250 | 249 | nn0ge0d 12532 |
. . . . . . . 8
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ 0 โค ๐) |
251 | | df-tp 4633 |
. . . . . . . . . 10
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {1}) |
252 | | snssi 4811 |
. . . . . . . . . . . 12
โข (1 โ
โ โ {1} โ โ) |
253 | 229, 252 | mp1i 13 |
. . . . . . . . . . 11
โข (๐ โ {1} โ
โ) |
254 | 70, 253 | unssd 4186 |
. . . . . . . . . 10
โข (๐ โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {1}) โ
โ) |
255 | 251, 254 | eqsstrid 4030 |
. . . . . . . . 9
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ โ) |
256 | | breq1 5151 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (๐ฅ โฅ ๐ต โ 1 โฅ ๐ต)) |
257 | 223, 256 | syl5ibrcom 246 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ = 1 โ ๐ฅ โฅ ๐ต)) |
258 | 86, 92, 257 | 3jaod 1429 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = 1) โ ๐ฅ โฅ ๐ต)) |
259 | | eltpi 4691 |
. . . . . . . . . 10
โข (๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = 1)) |
260 | 258, 259 | impel 507 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}) โ ๐ฅ โฅ ๐ต) |
261 | 255, 260 | ssrabdv 4071 |
. . . . . . . 8
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) |
262 | 61, 248, 250, 261 | fsumless 15739 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ โค ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
263 | 262 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ โค ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
264 | 52, 81, 82 | diveq1ad 11996 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ต / ((2โ(๐ด + 1)) โ 1)) = 1 โ ๐ต = ((2โ(๐ด + 1)) โ 1))) |
265 | 264 | necon3bid 2986 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1 โ ๐ต โ ((2โ(๐ด + 1)) โ
1))) |
266 | 265 | biimpar 479 |
. . . . . . . . . . 11
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1) |
267 | 266 | necomd 2997 |
. . . . . . . . . 10
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ 1 โ (๐ต / ((2โ(๐ด + 1)) โ 1))) |
268 | 221 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ 1 โ ๐ต) |
269 | 267, 268 | nelprd 4659 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ยฌ 1 โ
{(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
270 | | disjsn 4715 |
. . . . . . . . 9
โข (({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {1}) = โ
โ ยฌ 1 โ
{(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
271 | 269, 270 | sylibr 233 |
. . . . . . . 8
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {1}) = โ
) |
272 | 251 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {1})) |
273 | | tpfi 9320 |
. . . . . . . . 9
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ Fin |
274 | 273 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ Fin) |
275 | 255 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ โ) |
276 | 275 | sselda 3982 |
. . . . . . . . 9
โข (((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}) โ ๐ โ โ) |
277 | 276 | nncnd 12225 |
. . . . . . . 8
โข (((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}) โ ๐ โ โ) |
278 | 271, 272,
274, 277 | fsumsplit 15684 |
. . . . . . 7
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ = (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {1}๐)) |
279 | | id 22 |
. . . . . . . . . . 11
โข (๐ = 1 โ ๐ = 1) |
280 | 279 | sumsn 15689 |
. . . . . . . . . 10
โข ((1
โ โ โง 1 โ โ) โ ฮฃ๐ โ {1}๐ = 1) |
281 | 2, 27, 280 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ {1}๐ = 1) |
282 | 149, 281 | oveq12d 7424 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {1}๐) = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
283 | 282 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {1}๐) = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
284 | 278, 283 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
285 | 204 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
286 | 263, 284,
285 | 3brtr3d 5179 |
. . . . 5
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1)))) |
287 | 286 | ex 414 |
. . . 4
โข (๐ โ (๐ต โ ((2โ(๐ด + 1)) โ 1) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1))))) |
288 | 287 | necon1bd 2959 |
. . 3
โข (๐ โ (ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ 1))) โ ๐ต = ((2โ(๐ด + 1)) โ 1))) |
289 | 247, 288 | mpd 15 |
. 2
โข (๐ โ ๐ต = ((2โ(๐ด + 1)) โ 1)) |
290 | 242, 289 | jca 513 |
1
โข (๐ โ (๐ต โ โ โง ๐ต = ((2โ(๐ด + 1)) โ 1))) |