Step | Hyp | Ref
| Expression |
1 | | perfectALTVlem.2 |
. . . 4
โข (๐ โ ๐ต โ โ) |
2 | | 1re 11160 |
. . . . . 6
โข 1 โ
โ |
3 | 2 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ
โ) |
4 | | perfectALTVlem.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
5 | | perfectALTVlem.3 |
. . . . . . . 8
โข (๐ โ ๐ต โ Odd ) |
6 | | perfectALTVlem.4 |
. . . . . . . 8
โข (๐ โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = (2 ยท ((2โ๐ด) ยท ๐ต))) |
7 | 4, 1, 5, 6 | perfectALTVlem1 45999 |
. . . . . . 7
โข (๐ โ ((2โ(๐ด + 1)) โ โ โง
((2โ(๐ด + 1)) โ
1) โ โ โง (๐ต
/ ((2โ(๐ด + 1)) โ
1)) โ โ)) |
8 | 7 | simp3d 1145 |
. . . . . 6
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
9 | 8 | nnred 12173 |
. . . . 5
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
10 | 1 | nnred 12173 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
11 | 8 | nnge1d 12206 |
. . . . 5
โข (๐ โ 1 โค (๐ต / ((2โ(๐ด + 1)) โ 1))) |
12 | | 2cn 12233 |
. . . . . . . . . . 11
โข 2 โ
โ |
13 | | exp1 13979 |
. . . . . . . . . . 11
โข (2 โ
โ โ (2โ1) = 2) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . 10
โข
(2โ1) = 2 |
15 | | df-2 12221 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
16 | 14, 15 | eqtri 2761 |
. . . . . . . . 9
โข
(2โ1) = (1 + 1) |
17 | | 2re 12232 |
. . . . . . . . . . 11
โข 2 โ
โ |
18 | 17 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
19 | | 1zzd 12539 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โค) |
20 | 4 | peano2nnd 12175 |
. . . . . . . . . . 11
โข (๐ โ (๐ด + 1) โ โ) |
21 | 20 | nnzd 12531 |
. . . . . . . . . 10
โข (๐ โ (๐ด + 1) โ โค) |
22 | | 1lt2 12329 |
. . . . . . . . . . 11
โข 1 <
2 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 1 < 2) |
24 | 4 | nnrpd 12960 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ
โ+) |
25 | | ltaddrp 12957 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐ด
โ โ+) โ 1 < (1 + ๐ด)) |
26 | 2, 24, 25 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ 1 < (1 + ๐ด)) |
27 | | ax-1cn 11114 |
. . . . . . . . . . . 12
โข 1 โ
โ |
28 | 4 | nncnd 12174 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
29 | | addcom 11346 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + ๐ด) = (๐ด + 1)) |
30 | 27, 28, 29 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (1 + ๐ด) = (๐ด + 1)) |
31 | 26, 30 | breqtrd 5132 |
. . . . . . . . . 10
โข (๐ โ 1 < (๐ด + 1)) |
32 | | ltexp2a 14077 |
. . . . . . . . . 10
โข (((2
โ โ โง 1 โ โค โง (๐ด + 1) โ โค) โง (1 < 2 โง
1 < (๐ด + 1))) โ
(2โ1) < (2โ(๐ด
+ 1))) |
33 | 18, 19, 21, 23, 31, 32 | syl32anc 1379 |
. . . . . . . . 9
โข (๐ โ (2โ1) <
(2โ(๐ด +
1))) |
34 | 16, 33 | eqbrtrrid 5142 |
. . . . . . . 8
โข (๐ โ (1 + 1) <
(2โ(๐ด +
1))) |
35 | 7 | simp1d 1143 |
. . . . . . . . . 10
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
36 | 35 | nnred 12173 |
. . . . . . . . 9
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
37 | 3, 3, 36 | ltaddsubd 11760 |
. . . . . . . 8
โข (๐ โ ((1 + 1) <
(2โ(๐ด + 1)) โ 1
< ((2โ(๐ด + 1))
โ 1))) |
38 | 34, 37 | mpbid 231 |
. . . . . . 7
โข (๐ โ 1 < ((2โ(๐ด + 1)) โ
1)) |
39 | | 1rp 12924 |
. . . . . . . . 9
โข 1 โ
โ+ |
40 | 39 | a1i 11 |
. . . . . . . 8
โข (๐ โ 1 โ
โ+) |
41 | | peano2rem 11473 |
. . . . . . . . . . 11
โข
((2โ(๐ด + 1))
โ โ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
42 | 36, 41 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
43 | | expgt1 14012 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (๐ด +
1) โ โ โง 1 < 2) โ 1 < (2โ(๐ด + 1))) |
44 | 18, 20, 23, 43 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ 1 < (2โ(๐ด + 1))) |
45 | | posdif 11653 |
. . . . . . . . . . . 12
โข ((1
โ โ โง (2โ(๐ด + 1)) โ โ) โ (1 <
(2โ(๐ด + 1)) โ 0
< ((2โ(๐ด + 1))
โ 1))) |
46 | 2, 36, 45 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (1 < (2โ(๐ด + 1)) โ 0 <
((2โ(๐ด + 1)) โ
1))) |
47 | 44, 46 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ 0 < ((2โ(๐ด + 1)) โ
1)) |
48 | 42, 47 | jca 513 |
. . . . . . . . 9
โข (๐ โ (((2โ(๐ด + 1)) โ 1) โ โ
โง 0 < ((2โ(๐ด +
1)) โ 1))) |
49 | | elrp 12922 |
. . . . . . . . 9
โข
(((2โ(๐ด + 1))
โ 1) โ โ+ โ (((2โ(๐ด + 1)) โ 1) โ โ โง 0
< ((2โ(๐ด + 1))
โ 1))) |
50 | 48, 49 | sylibr 233 |
. . . . . . . 8
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ+) |
51 | | nnrp 12931 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต โ
โ+) |
52 | 1, 51 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ+) |
53 | 40, 50, 52 | ltdiv2d 12985 |
. . . . . . 7
โข (๐ โ (1 < ((2โ(๐ด + 1)) โ 1) โ (๐ต / ((2โ(๐ด + 1)) โ 1)) < (๐ต / 1))) |
54 | 38, 53 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) < (๐ต / 1)) |
55 | 1 | nncnd 12174 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
56 | 55 | div1d 11928 |
. . . . . 6
โข (๐ โ (๐ต / 1) = ๐ต) |
57 | 54, 56 | breqtrd 5132 |
. . . . 5
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) < ๐ต) |
58 | 3, 9, 10, 11, 57 | lelttrd 11318 |
. . . 4
โข (๐ โ 1 < ๐ต) |
59 | | eluz2b2 12851 |
. . . 4
โข (๐ต โ
(โคโฅโ2) โ (๐ต โ โ โง 1 < ๐ต)) |
60 | 1, 58, 59 | sylanbrc 584 |
. . 3
โข (๐ โ ๐ต โ
(โคโฅโ2)) |
61 | | fzfid 13884 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐ต) โ Fin) |
62 | | dvdsssfz1 16205 |
. . . . . . . . . . . . 13
โข (๐ต โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ (1...๐ต)) |
63 | 1, 62 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ (1...๐ต)) |
64 | | ssfi 9120 |
. . . . . . . . . . . 12
โข
(((1...๐ต) โ Fin
โง {๐ฅ โ โ
โฃ ๐ฅ โฅ ๐ต} โ (1...๐ต)) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ Fin) |
65 | 61, 63, 64 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ Fin) |
66 | 65 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ Fin) |
67 | | ssrab2 4038 |
. . . . . . . . . . . . 13
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ โ |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} โ โ) |
69 | 68 | sselda 3945 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
70 | 69 | nnred 12173 |
. . . . . . . . . 10
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
71 | 69 | nnnn0d 12478 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ0) |
72 | 71 | nn0ge0d 12481 |
. . . . . . . . . 10
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ 0 โค ๐) |
73 | | df-tp 4592 |
. . . . . . . . . . . 12
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {๐}) |
74 | | prssi 4782 |
. . . . . . . . . . . . . . 15
โข (((๐ต / ((2โ(๐ด + 1)) โ 1)) โ โ โง
๐ต โ โ) โ
{(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ
โ) |
75 | 8, 1, 74 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ โ) |
76 | 75 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ โ) |
77 | | simplrl 776 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
78 | 77 | snssd 4770 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {๐} โ โ) |
79 | 76, 78 | unssd 4147 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {๐}) โ โ) |
80 | 73, 79 | eqsstrid 3993 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ โ) |
81 | | eltpi 4649 |
. . . . . . . . . . . . 13
โข (๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = ๐)) |
82 | 7 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
83 | 82 | nnzd 12531 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โค) |
84 | 8 | nnzd 12531 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โค) |
85 | | dvdsmul2 16166 |
. . . . . . . . . . . . . . . . . 18
โข
((((2โ(๐ด + 1))
โ 1) โ โค โง (๐ต / ((2โ(๐ด + 1)) โ 1)) โ โค) โ
(๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ
(((2โ(๐ด + 1)) โ
1) ยท (๐ต /
((2โ(๐ด + 1)) โ
1)))) |
86 | 83, 84, 85 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ (((2โ(๐ด + 1)) โ 1) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1)))) |
87 | 82 | nncnd 12174 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
88 | 82 | nnne0d 12208 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
0) |
89 | 55, 87, 88 | divcan2d 11938 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท
(๐ต / ((2โ(๐ด + 1)) โ 1))) = ๐ต) |
90 | 86, 89 | breqtrd 5132 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ ๐ต) |
91 | | breq1 5109 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ (๐ฅ โฅ ๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โฅ ๐ต)) |
92 | 90, 91 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ๐ฅ โฅ ๐ต)) |
93 | 92 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ๐ฅ โฅ ๐ต)) |
94 | 1 | nnzd 12531 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ โค) |
95 | | iddvds 16157 |
. . . . . . . . . . . . . . . . 17
โข (๐ต โ โค โ ๐ต โฅ ๐ต) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โฅ ๐ต) |
97 | | breq1 5109 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ต โ (๐ฅ โฅ ๐ต โ ๐ต โฅ ๐ต)) |
98 | 96, 97 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ฅ = ๐ต โ ๐ฅ โฅ ๐ต)) |
99 | 98 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ = ๐ต โ ๐ฅ โฅ ๐ต)) |
100 | | simplrr 777 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โฅ ๐ต) |
101 | | breq1 5109 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ (๐ฅ โฅ ๐ต โ ๐ โฅ ๐ต)) |
102 | 100, 101 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ = ๐ โ ๐ฅ โฅ ๐ต)) |
103 | 93, 99, 102 | 3jaod 1429 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ((๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = ๐) โ ๐ฅ โฅ ๐ต)) |
104 | 81, 103 | syl5 34 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ ๐ฅ โฅ ๐ต)) |
105 | 104 | imp 408 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}) โ ๐ฅ โฅ ๐ต) |
106 | 80, 105 | ssrabdv 4032 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) |
107 | 66, 70, 72, 106 | fsumless 15686 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}๐ โค ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
108 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
109 | | disjsn 4673 |
. . . . . . . . . . . 12
โข (({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {๐}) = โ
โ ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
110 | 108, 109 | sylibr 233 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {๐}) = โ
) |
111 | 73 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {๐})) |
112 | | tpfi 9270 |
. . . . . . . . . . . 12
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ Fin |
113 | 112 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐} โ Fin) |
114 | 80 | sselda 3945 |
. . . . . . . . . . . 12
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}) โ ๐ โ โ) |
115 | 114 | nncnd 12174 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}) โ ๐ โ โ) |
116 | 110, 111,
113, 115 | fsumsplit 15631 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}๐ = (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {๐}๐)) |
117 | 8 | nncnd 12174 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
118 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ๐ = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
119 | 118 | sumsn 15636 |
. . . . . . . . . . . . . . 15
โข (((๐ต / ((2โ(๐ด + 1)) โ 1)) โ โ โง
(๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) โ ฮฃ๐
โ {(๐ต /
((2โ(๐ด + 1)) โ
1))}๐ = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
120 | 8, 117, 119 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1))}๐ = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
121 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ต โ ๐ = ๐ต) |
122 | 121 | sumsn 15636 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ โ โง ๐ต โ โ) โ
ฮฃ๐ โ {๐ต}๐ = ๐ต) |
123 | 1, 55, 122 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ {๐ต}๐ = ๐ต) |
124 | 120, 123 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1))}๐ + ฮฃ๐ โ {๐ต}๐) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ๐ต)) |
125 | | incom 4162 |
. . . . . . . . . . . . . . 15
โข ({๐ต} โฉ {(๐ต / ((2โ(๐ด + 1)) โ 1))}) = ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โฉ {๐ต}) |
126 | 9, 57 | gtned 11295 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1))) |
127 | | disjsn2 4674 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ ({๐ต} โฉ {(๐ต / ((2โ(๐ด + 1)) โ 1))}) =
โ
) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ({๐ต} โฉ {(๐ต / ((2โ(๐ด + 1)) โ 1))}) =
โ
) |
129 | 125, 128 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
โข (๐ โ ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โฉ {๐ต}) = โ
) |
130 | | df-pr 4590 |
. . . . . . . . . . . . . . 15
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} = ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โช {๐ต}) |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} = ({(๐ต / ((2โ(๐ด + 1)) โ 1))} โช {๐ต})) |
132 | | prfi 9269 |
. . . . . . . . . . . . . . 15
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ Fin |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ Fin) |
134 | 75 | sselda 3945 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
135 | 134 | nncnd 12174 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
136 | 129, 131,
133, 135 | fsumsplit 15631 |
. . . . . . . . . . . . 13
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ = (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1))}๐ + ฮฃ๐ โ {๐ต}๐)) |
137 | 87, 55 | mulcld 11180 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท ๐ต) โ
โ) |
138 | 55, 137, 87, 88 | divdird 11974 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) / ((2โ(๐ด + 1)) โ 1)) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ((((2โ(๐ด + 1)) โ 1) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)))) |
139 | 35 | nncnd 12174 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
140 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ 1 โ
โ) |
141 | 139, 140,
55 | subdird 11617 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท ๐ต) = (((2โ(๐ด + 1)) ยท ๐ต) โ (1 ยท ๐ต))) |
142 | 55 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (1 ยท ๐ต) = ๐ต) |
143 | 142 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((2โ(๐ด + 1)) ยท ๐ต) โ (1 ยท ๐ต)) = (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต)) |
144 | 141, 143 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((2โ(๐ด + 1)) โ 1) ยท ๐ต) = (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต)) |
145 | 144 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) = (๐ต + (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต))) |
146 | 139, 55 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) โ
โ) |
147 | 55, 146 | pncan3d 11520 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต + (((2โ(๐ด + 1)) ยท ๐ต) โ ๐ต)) = ((2โ(๐ด + 1)) ยท ๐ต)) |
148 | 145, 147 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) = ((2โ(๐ด + 1)) ยท ๐ต)) |
149 | 148 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) / ((2โ(๐ด + 1)) โ 1)) = (((2โ(๐ด + 1)) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1))) |
150 | 139, 55, 87, 88 | divassd 11971 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2โ(๐ด + 1)) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)) = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
151 | 149, 150 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต + (((2โ(๐ด + 1)) โ 1) ยท ๐ต)) / ((2โ(๐ด + 1)) โ 1)) = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
152 | 55, 87, 88 | divcan3d 11941 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((((2โ(๐ด + 1)) โ 1) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)) = ๐ต) |
153 | 152 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ((((2โ(๐ด + 1)) โ 1) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1))) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ๐ต)) |
154 | 138, 151,
153 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) = ((๐ต / ((2โ(๐ด + 1)) โ 1)) + ๐ต)) |
155 | 124, 136,
154 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
156 | 155 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
157 | 77 | nncnd 12174 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
158 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ๐ = ๐) |
159 | 158 | sumsn 15636 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
ฮฃ๐ โ {๐}๐ = ๐) |
160 | 157, 157,
159 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {๐}๐ = ๐) |
161 | 156, 160 | oveq12d 7376 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {๐}๐) = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐)) |
162 | 116, 161 | eqtrd 2773 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, ๐}๐ = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐)) |
163 | 4 | nnnn0d 12478 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ด โ
โ0) |
164 | | expp1 13980 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐ด
โ โ0) โ (2โ(๐ด + 1)) = ((2โ๐ด) ยท 2)) |
165 | 12, 163, 164 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2โ(๐ด + 1)) = ((2โ๐ด) ยท 2)) |
166 | | 2nn 12231 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
167 | | nnexpcl 13986 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐ด
โ โ0) โ (2โ๐ด) โ โ) |
168 | 166, 163,
167 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2โ๐ด) โ โ) |
169 | 168 | nncnd 12174 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2โ๐ด) โ โ) |
170 | | mulcom 11142 |
. . . . . . . . . . . . . . . . 17
โข
(((2โ๐ด) โ
โ โง 2 โ โ) โ ((2โ๐ด) ยท 2) = (2 ยท (2โ๐ด))) |
171 | 169, 12, 170 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2โ๐ด) ยท 2) = (2 ยท (2โ๐ด))) |
172 | 165, 171 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2โ(๐ด + 1)) = (2 ยท (2โ๐ด))) |
173 | 172 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) = ((2 ยท (2โ๐ด)) ยท ๐ต)) |
174 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ) |
175 | 174, 169,
55 | mulassd 11183 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท (2โ๐ด)) ยท ๐ต) = (2 ยท ((2โ๐ด) ยท ๐ต))) |
176 | | isodd7 45943 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ต โ Odd โ (๐ต โ โค โง (2 gcd
๐ต) = 1)) |
177 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ โค โง (2 gcd
๐ต) = 1) โ (2 gcd ๐ต) = 1) |
178 | 176, 177 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ Odd โ (2 gcd ๐ต) = 1) |
179 | 5, 178 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 gcd ๐ต) = 1) |
180 | | 2z 12540 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โค |
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โ
โค) |
182 | | rpexp1i 16604 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โค โง ๐ต
โ โค โง ๐ด
โ โ0) โ ((2 gcd ๐ต) = 1 โ ((2โ๐ด) gcd ๐ต) = 1)) |
183 | 181, 94, 163, 182 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 gcd ๐ต) = 1 โ ((2โ๐ด) gcd ๐ต) = 1)) |
184 | 179, 183 | mpd 15 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2โ๐ด) gcd ๐ต) = 1) |
185 | | sgmmul 26565 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ((2โ๐ด) โ โ โง ๐ต โ โ โง ((2โ๐ด) gcd ๐ต) = 1)) โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต))) |
186 | 140, 168,
1, 184, 185 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต))) |
187 | | pncan 11412 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด + 1)
โ 1) = ๐ด) |
188 | 28, 27, 187 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ด + 1) โ 1) = ๐ด) |
189 | 188 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2โ((๐ด + 1) โ 1)) =
(2โ๐ด)) |
190 | 189 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 ฯ (2โ((๐ด + 1) โ 1))) = (1 ฯ
(2โ๐ด))) |
191 | | 1sgm2ppw 26564 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด + 1) โ โ โ (1
ฯ (2โ((๐ด + 1)
โ 1))) = ((2โ(๐ด
+ 1)) โ 1)) |
192 | 20, 191 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 ฯ (2โ((๐ด + 1) โ 1))) =
((2โ(๐ด + 1)) โ
1)) |
193 | 190, 192 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 ฯ (2โ๐ด)) = ((2โ(๐ด + 1)) โ 1)) |
194 | 193 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต)) = (((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต))) |
195 | 186, 6, 194 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 ยท ((2โ๐ด) ยท ๐ต)) = (((2โ(๐ด + 1)) โ 1) ยท (1 ฯ ๐ต))) |
196 | 173, 175,
195 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) = (((2โ(๐ด + 1)) โ 1) ยท (1 ฯ ๐ต))) |
197 | 196 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ (((2โ(๐ด + 1)) ยท ๐ต) / ((2โ(๐ด + 1)) โ 1)) = ((((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต)) /
((2โ(๐ด + 1)) โ
1))) |
198 | | 1nn0 12434 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ0 |
199 | | sgmnncl 26512 |
. . . . . . . . . . . . . . 15
โข ((1
โ โ0 โง ๐ต โ โ) โ (1 ฯ ๐ต) โ
โ) |
200 | 198, 1, 199 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (๐ โ (1 ฯ ๐ต) โ
โ) |
201 | 200 | nncnd 12174 |
. . . . . . . . . . . . 13
โข (๐ โ (1 ฯ ๐ต) โ
โ) |
202 | 201, 87, 88 | divcan3d 11941 |
. . . . . . . . . . . 12
โข (๐ โ ((((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต)) /
((2โ(๐ด + 1)) โ
1)) = (1 ฯ ๐ต)) |
203 | 197, 150,
202 | 3eqtr3d 2781 |
. . . . . . . . . . 11
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) = (1 ฯ ๐ต)) |
204 | | sgmval 26507 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐ต
โ โ) โ (1 ฯ ๐ต) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} (๐โ๐1)) |
205 | 27, 1, 204 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (1 ฯ ๐ต) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} (๐โ๐1)) |
206 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) |
207 | 67, 206 | sselid 3943 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
208 | 207 | nncnd 12174 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
209 | 208 | cxp1d 26077 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ (๐โ๐1) = ๐) |
210 | 209 | sumeq2dv 15593 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต} (๐โ๐1) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
211 | 203, 205,
210 | 3eqtrrd 2778 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
212 | 211 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
213 | 107, 162,
212 | 3brtr3d 5137 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โค ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
214 | 36, 9 | remulcld 11190 |
. . . . . . . . . . 11
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) โ
โ) |
215 | 214 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) โ
โ) |
216 | 77 | nnrpd 12960 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ+) |
217 | 215, 216 | ltaddrpd 12995 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐)) |
218 | 77 | nnred 12173 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ๐ โ โ) |
219 | 215, 218 | readdcld 11189 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โ โ) |
220 | 215, 219 | ltnled 11307 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โ ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โค ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))))) |
221 | 217, 220 | mpbid 231 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โง ยฌ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) โ ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + ๐) โค ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
222 | 213, 221 | condan 817 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โ ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
223 | | elpri 4609 |
. . . . . . 7
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) |
224 | 222, 223 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐ต)) โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) |
225 | 224 | expr 458 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต))) |
226 | 225 | ralrimiva 3140 |
. . . 4
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต))) |
227 | 3, 58 | gtned 11295 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ 1) |
228 | 227 | necomd 2996 |
. . . . . . . . 9
โข (๐ โ 1 โ ๐ต) |
229 | | 1nn 12169 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
230 | 229 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ) |
231 | | 1dvds 16158 |
. . . . . . . . . . . . 13
โข (๐ต โ โค โ 1 โฅ
๐ต) |
232 | 94, 231 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 1 โฅ ๐ต) |
233 | | breq1 5109 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (๐ โฅ ๐ต โ 1 โฅ ๐ต)) |
234 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
235 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (๐ = ๐ต โ 1 = ๐ต)) |
236 | 234, 235 | orbi12d 918 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ ((๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต) โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต))) |
237 | 233, 236 | imbi12d 345 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ ((๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) โ (1 โฅ ๐ต โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต)))) |
238 | 237 | rspcv 3576 |
. . . . . . . . . . . 12
โข (1 โ
โ โ (โ๐
โ โ (๐ โฅ
๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)) โ (1 โฅ ๐ต โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต)))) |
239 | 230, 226,
232, 238 | syl3c 66 |
. . . . . . . . . . 11
โข (๐ โ (1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ 1 = ๐ต)) |
240 | 239 | ord 863 |
. . . . . . . . . 10
โข (๐ โ (ยฌ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1 = ๐ต)) |
241 | 240 | necon1ad 2957 |
. . . . . . . . 9
โข (๐ โ (1 โ ๐ต โ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
242 | 228, 241 | mpd 15 |
. . . . . . . 8
โข (๐ โ 1 = (๐ต / ((2โ(๐ด + 1)) โ 1))) |
243 | 242 | eqeq2d 2744 |
. . . . . . 7
โข (๐ โ (๐ = 1 โ ๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
244 | 243 | orbi1d 916 |
. . . . . 6
โข (๐ โ ((๐ = 1 โจ ๐ = ๐ต) โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต))) |
245 | 244 | imbi2d 341 |
. . . . 5
โข (๐ โ ((๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต)) โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)))) |
246 | 245 | ralbidv 3171 |
. . . 4
โข (๐ โ (โ๐ โ โ (๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต)) โ โ๐ โ โ (๐ โฅ ๐ต โ (๐ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ = ๐ต)))) |
247 | 226, 246 | mpbird 257 |
. . 3
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต))) |
248 | | isprm2 16563 |
. . 3
โข (๐ต โ โ โ (๐ต โ
(โคโฅโ2) โง โ๐ โ โ (๐ โฅ ๐ต โ (๐ = 1 โจ ๐ = ๐ต)))) |
249 | 60, 247, 248 | sylanbrc 584 |
. 2
โข (๐ โ ๐ต โ โ) |
250 | 214 | ltp1d 12090 |
. . . 4
โข (๐ โ ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
251 | | peano2re 11333 |
. . . . . 6
โข
(((2โ(๐ด + 1))
ยท (๐ต /
((2โ(๐ด + 1)) โ
1))) โ โ โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โ
โ) |
252 | 214, 251 | syl 17 |
. . . . 5
โข (๐ โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โ
โ) |
253 | 214, 252 | ltnled 11307 |
. . . 4
โข (๐ โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) < (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โ ยฌ
(((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1))))) |
254 | 250, 253 | mpbid 231 |
. . 3
โข (๐ โ ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1)))) |
255 | 207 | nnred 12173 |
. . . . . . . 8
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ) |
256 | 207 | nnnn0d 12478 |
. . . . . . . . 9
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ ๐ โ โ0) |
257 | 256 | nn0ge0d 12481 |
. . . . . . . 8
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) โ 0 โค ๐) |
258 | | df-tp 4592 |
. . . . . . . . . 10
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {1}) |
259 | | snssi 4769 |
. . . . . . . . . . . 12
โข (1 โ
โ โ {1} โ โ) |
260 | 229, 259 | mp1i 13 |
. . . . . . . . . . 11
โข (๐ โ {1} โ
โ) |
261 | 75, 260 | unssd 4147 |
. . . . . . . . . 10
โข (๐ โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {1}) โ
โ) |
262 | 258, 261 | eqsstrid 3993 |
. . . . . . . . 9
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ โ) |
263 | | eltpi 4649 |
. . . . . . . . . . 11
โข (๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ (๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = 1)) |
264 | | breq1 5109 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (๐ฅ โฅ ๐ต โ 1 โฅ ๐ต)) |
265 | 232, 264 | syl5ibrcom 247 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ = 1 โ ๐ฅ โฅ ๐ต)) |
266 | 92, 98, 265 | 3jaod 1429 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฅ = (๐ต / ((2โ(๐ด + 1)) โ 1)) โจ ๐ฅ = ๐ต โจ ๐ฅ = 1) โ ๐ฅ โฅ ๐ต)) |
267 | 263, 266 | syl5 34 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ ๐ฅ โฅ ๐ต)) |
268 | 267 | imp 408 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}) โ ๐ฅ โฅ ๐ต) |
269 | 262, 268 | ssrabdv 4032 |
. . . . . . . 8
โข (๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}) |
270 | 65, 255, 257, 269 | fsumless 15686 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ โค ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
271 | 270 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ โค ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐) |
272 | 55, 87, 88 | diveq1ad 11945 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ต / ((2โ(๐ด + 1)) โ 1)) = 1 โ ๐ต = ((2โ(๐ด + 1)) โ 1))) |
273 | 272 | necon3bid 2985 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1 โ ๐ต โ ((2โ(๐ด + 1)) โ
1))) |
274 | 273 | biimpar 479 |
. . . . . . . . . . 11
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ 1) |
275 | 274 | necomd 2996 |
. . . . . . . . . 10
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ 1 โ (๐ต / ((2โ(๐ด + 1)) โ 1))) |
276 | 228 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ 1 โ ๐ต) |
277 | 275, 276 | nelprd 4618 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ยฌ 1 โ
{(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
278 | | disjsn 4673 |
. . . . . . . . 9
โข (({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {1}) = โ
โ ยฌ 1 โ
{(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}) |
279 | 277, 278 | sylibr 233 |
. . . . . . . 8
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โฉ {1}) = โ
) |
280 | 258 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} = ({(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต} โช {1})) |
281 | | tpfi 9270 |
. . . . . . . . 9
โข {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ Fin |
282 | 281 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ Fin) |
283 | 262 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1} โ โ) |
284 | 283 | sselda 3945 |
. . . . . . . . 9
โข (((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}) โ ๐ โ โ) |
285 | 284 | nncnd 12174 |
. . . . . . . 8
โข (((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โง ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}) โ ๐ โ โ) |
286 | 279, 280,
282, 285 | fsumsplit 15631 |
. . . . . . 7
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ = (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {1}๐)) |
287 | | id 22 |
. . . . . . . . . . 11
โข (๐ = 1 โ ๐ = 1) |
288 | 287 | sumsn 15636 |
. . . . . . . . . 10
โข ((1
โ โ โง 1 โ โ) โ ฮฃ๐ โ {1}๐ = 1) |
289 | 140, 27, 288 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ {1}๐ = 1) |
290 | 155, 289 | oveq12d 7376 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {1}๐) = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
291 | 290 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ (ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต}๐ + ฮฃ๐ โ {1}๐) = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
292 | 286, 291 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {(๐ต / ((2โ(๐ด + 1)) โ 1)), ๐ต, 1}๐ = (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1)) |
293 | 211 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ต}๐ = ((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1)))) |
294 | 271, 292,
293 | 3brtr3d 5137 |
. . . . 5
โข ((๐ โง ๐ต โ ((2โ(๐ด + 1)) โ 1)) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1)))) |
295 | 294 | ex 414 |
. . . 4
โข (๐ โ (๐ต โ ((2โ(๐ด + 1)) โ 1) โ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ
1))))) |
296 | 295 | necon1bd 2958 |
. . 3
โข (๐ โ (ยฌ (((2โ(๐ด + 1)) ยท (๐ต / ((2โ(๐ด + 1)) โ 1))) + 1) โค
((2โ(๐ด + 1)) ยท
(๐ต / ((2โ(๐ด + 1)) โ 1))) โ ๐ต = ((2โ(๐ด + 1)) โ 1))) |
297 | 254, 296 | mpd 15 |
. 2
โข (๐ โ ๐ต = ((2โ(๐ด + 1)) โ 1)) |
298 | 249, 297 | jca 513 |
1
โข (๐ โ (๐ต โ โ โง ๐ต = ((2โ(๐ด + 1)) โ 1))) |