Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ (2โ๐) = (2โ1)) |
2 | | 2cn 12235 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
3 | | exp1 13980 |
. . . . . . . . . . . . . 14
โข (2 โ
โ โ (2โ1) = 2) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(2โ1) = 2 |
5 | 1, 4 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (2โ๐) = 2) |
6 | 5 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ = 1 โ ((2โ๐) โ 1) = (2 โ
1)) |
7 | | 2m1e1 12286 |
. . . . . . . . . . 11
โข (2
โ 1) = 1 |
8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ = 1 โ ((2โ๐) โ 1) =
1) |
9 | 8 | adantl 483 |
. . . . . . . . 9
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ = 1) โ
((2โ๐) โ 1) =
1) |
10 | 9 | eqeq1d 2739 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ = 1) โ
(((2โ๐) โ 1) =
(๐โ๐) โ 1 = (๐โ๐))) |
11 | | eldifi 4091 |
. . . . . . . . . . . . 13
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
12 | | prmnn 16557 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
13 | | nnnn0 12427 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ0) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ๐ โ
โ0) |
15 | 14 | nn0zd 12532 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
16 | | iddvdsexp 16169 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โฅ (๐โ๐)) |
17 | 15, 16 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โฅ (๐โ๐)) |
18 | | breq2 5114 |
. . . . . . . . . . . . 13
โข (1 =
(๐โ๐) โ (๐ โฅ 1 โ ๐ โฅ (๐โ๐))) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง 1 = (๐โ๐)) โ (๐ โฅ 1 โ ๐ โฅ (๐โ๐))) |
20 | | dvds1 16208 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (๐ โฅ 1 โ
๐ = 1)) |
21 | 14, 20 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (โ โ {2})
โ (๐ โฅ 1 โ
๐ = 1)) |
22 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (๐ โ โ โ 1 โ
โ)) |
23 | | 1nprm 16562 |
. . . . . . . . . . . . . . . . 17
โข ยฌ 1
โ โ |
24 | 23 | pm2.21i 119 |
. . . . . . . . . . . . . . . 16
โข (1 โ
โ โ ๐ =
1) |
25 | 22, 24 | syl6bi 253 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (๐ โ โ โ ๐ = 1)) |
26 | 11, 25 | syl5com 31 |
. . . . . . . . . . . . . 14
โข (๐ โ (โ โ {2})
โ (๐ = 1 โ ๐ = 1)) |
27 | 21, 26 | sylbid 239 |
. . . . . . . . . . . . 13
โข (๐ โ (โ โ {2})
โ (๐ โฅ 1 โ
๐ = 1)) |
28 | 27 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง 1 = (๐โ๐)) โ (๐ โฅ 1 โ ๐ = 1)) |
29 | 19, 28 | sylbird 260 |
. . . . . . . . . . 11
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง 1 = (๐โ๐)) โ (๐ โฅ (๐โ๐) โ ๐ = 1)) |
30 | 29 | ex 414 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (1 = (๐โ๐) โ (๐ โฅ (๐โ๐) โ ๐ = 1))) |
31 | 17, 30 | mpid 44 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (1 = (๐โ๐) โ ๐ = 1)) |
32 | 31 | adantr 482 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ = 1) โ (1 =
(๐โ๐) โ ๐ = 1)) |
33 | 10, 32 | sylbid 239 |
. . . . . . 7
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ = 1) โ
(((2โ๐) โ 1) =
(๐โ๐) โ ๐ = 1)) |
34 | 33 | ex 414 |
. . . . . 6
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (๐ = 1 โ
(((2โ๐) โ 1) =
(๐โ๐) โ ๐ = 1))) |
35 | 34 | com23 86 |
. . . . 5
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (((2โ๐) โ
1) = (๐โ๐) โ (๐ = 1 โ ๐ = 1))) |
36 | 35 | a1d 25 |
. . . 4
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((ยฌ 2 โฅ ๐
โง 2 โฅ ๐) โ
(((2โ๐) โ 1) =
(๐โ๐) โ (๐ = 1 โ ๐ = 1)))) |
37 | 36 | 3adant3 1133 |
. . 3
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((ยฌ 2 โฅ ๐
โง 2 โฅ ๐) โ
(((2โ๐) โ 1) =
(๐โ๐) โ (๐ = 1 โ ๐ = 1)))) |
38 | 37 | 3imp 1112 |
. 2
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ 2 โฅ ๐
โง 2 โฅ ๐) โง
((2โ๐) โ 1) =
(๐โ๐)) โ (๐ = 1 โ ๐ = 1)) |
39 | | neqne 2952 |
. . . . . . . . . . . 12
โข (ยฌ
๐ = 1 โ ๐ โ 1) |
40 | 39 | anim2i 618 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ยฌ
๐ = 1) โ (๐ โ โ โง ๐ โ 1)) |
41 | | eluz2b3 12854 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ2) โ (๐ โ โ โง ๐ โ 1)) |
42 | 40, 41 | sylibr 233 |
. . . . . . . . . 10
โข ((๐ โ โ โง ยฌ
๐ = 1) โ ๐ โ
(โคโฅโ2)) |
43 | | oddge22np1 16238 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ2) โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ ((2 ยท ๐) + 1) = ๐)) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โ โง ยฌ
๐ = 1) โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โ ((2
ยท ๐) + 1) = ๐)) |
45 | 44 | 3ad2antl3 1188 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(ยฌ 2 โฅ ๐ โ
โ๐ โ โ ((2
ยท ๐) + 1) = ๐)) |
46 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ((2 ยท ๐) + 1) โ (2โ๐) = (2โ((2 ยท ๐) + 1))) |
47 | 46 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ((2 ยท ๐) + 1) โ ((2โ๐) โ 1) = ((2โ((2
ยท ๐) + 1)) โ
1)) |
48 | 47 | eqcoms 2745 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท ๐) + 1) = ๐ โ ((2โ๐) โ 1) = ((2โ((2
ยท ๐) + 1)) โ
1)) |
49 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ 2 โ
โ) |
50 | | 2nn0 12437 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
โ0 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ 2 โ
โ0) |
52 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ
โ0) |
53 | 51, 52 | nn0mulcld 12485 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (2
ยท ๐) โ
โ0) |
54 | 49, 53 | expp1d 14059 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ
(2โ((2 ยท ๐) +
1)) = ((2โ(2 ยท ๐)) ยท 2)) |
55 | 51, 53 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ
(2โ(2 ยท ๐))
โ โ0) |
56 | 55 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ
(2โ(2 ยท ๐))
โ โ) |
57 | 56, 49 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ
((2โ(2 ยท ๐))
ยท 2) = (2 ยท (2โ(2 ยท ๐)))) |
58 | 54, 57 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ
(2โ((2 ยท ๐) +
1)) = (2 ยท (2โ(2 ยท ๐)))) |
59 | 58 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((2โ((2 ยท ๐) +
1)) โ 1) = ((2 ยท (2โ(2 ยท ๐))) โ 1)) |
60 | | npcan1 11587 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((2โ(2 ยท ๐)) โ โ โ (((2โ(2
ยท ๐)) โ 1) +
1) = (2โ(2 ยท ๐))) |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ
(((2โ(2 ยท ๐))
โ 1) + 1) = (2โ(2 ยท ๐))) |
62 | 61 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ
(2โ(2 ยท ๐)) =
(((2โ(2 ยท ๐))
โ 1) + 1)) |
63 | 62 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (2
ยท (2โ(2 ยท ๐))) = (2 ยท (((2โ(2 ยท ๐)) โ 1) +
1))) |
64 | | peano2cnm 11474 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((2โ(2 ยท ๐)) โ โ โ ((2โ(2 ยท
๐)) โ 1) โ
โ) |
65 | 56, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ
((2โ(2 ยท ๐))
โ 1) โ โ) |
66 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ 1 โ
โ) |
67 | 49, 65, 66 | adddid 11186 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (2
ยท (((2โ(2 ยท ๐)) โ 1) + 1)) = ((2 ยท
((2โ(2 ยท ๐))
โ 1)) + (2 ยท 1))) |
68 | 63, 67 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (2
ยท (2โ(2 ยท ๐))) = ((2 ยท ((2โ(2 ยท ๐)) โ 1)) + (2 ยท
1))) |
69 | 68 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ((2
ยท (2โ(2 ยท ๐))) โ 1) = (((2 ยท ((2โ(2
ยท ๐)) โ 1)) +
(2 ยท 1)) โ 1)) |
70 | 49, 65 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (2
ยท ((2โ(2 ยท ๐)) โ 1)) โ
โ) |
71 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
โ |
72 | 2, 71 | mulcli 11169 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 1) โ โ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (2
ยท 1) โ โ) |
74 | 70, 73, 66 | addsubassd 11539 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (((2
ยท ((2โ(2 ยท ๐)) โ 1)) + (2 ยท 1)) โ 1) =
((2 ยท ((2โ(2 ยท ๐)) โ 1)) + ((2 ยท 1) โ
1))) |
75 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (2
ยท 1) = 2 |
76 | 75 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((2
ยท 1) โ 1) = (2 โ 1) |
77 | 76, 7 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((2
ยท 1) โ 1) = 1 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ((2
ยท 1) โ 1) = 1) |
79 | 78 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ((2
ยท ((2โ(2 ยท ๐)) โ 1)) + ((2 ยท 1) โ 1))
= ((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1)) |
80 | 74, 79 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (((2
ยท ((2โ(2 ยท ๐)) โ 1)) + (2 ยท 1)) โ 1) =
((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1)) |
81 | 59, 69, 80 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((2โ((2 ยท ๐) +
1)) โ 1) = ((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1)) |
82 | 81 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((2โ((2 ยท ๐) +
1)) โ 1) = ((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1)) |
83 | 48, 82 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง ((2 ยท ๐) + 1) = ๐) โ ((2โ๐) โ 1) = ((2 ยท ((2โ(2
ยท ๐)) โ 1)) +
1)) |
84 | 83 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง ((2 ยท ๐) + 1) = ๐) โ (((2โ๐) โ 1) = (๐โ๐) โ ((2 ยท ((2โ(2 ยท
๐)) โ 1)) + 1) =
(๐โ๐))) |
85 | 14 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ0) |
86 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ0) |
87 | 86 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ0) |
88 | 85, 87 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐โ๐) โ
โ0) |
89 | 88 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐โ๐) โ
โ) |
90 | 89 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (๐โ๐) โ
โ) |
91 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ 1 โ โ) |
92 | 70 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (2 ยท ((2โ(2 ยท ๐)) โ 1)) โ
โ) |
93 | 90, 91, 92 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ ((๐โ๐) โ โ โง 1 โ
โ โง (2 ยท ((2โ(2 ยท ๐)) โ 1)) โ
โ)) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((๐โ๐) โ โ โง 1 โ โ
โง (2 ยท ((2โ(2 ยท ๐)) โ 1)) โ
โ)) |
95 | | subadd2 11412 |
. . . . . . . . . . . . . . . . 17
โข (((๐โ๐) โ โ โง 1 โ โ
โง (2 ยท ((2โ(2 ยท ๐)) โ 1)) โ โ) โ
(((๐โ๐) โ 1) = (2 ยท ((2โ(2
ยท ๐)) โ 1))
โ ((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1) = (๐โ๐))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(((๐โ๐) โ 1) = (2 ยท ((2โ(2
ยท ๐)) โ 1))
โ ((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1) = (๐โ๐))) |
97 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
98 | 11, 12, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
99 | 98 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ) |
100 | 99, 87 | pwm1geoser 15761 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐โ๐) โ 1) = ((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐))) |
101 | 100 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ ((๐โ๐) โ 1) = ((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐))) |
102 | 101 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (((๐โ๐) โ 1) = (2 ยท
((2โ(2 ยท ๐))
โ 1)) โ ((๐
โ 1) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = (2 ยท ((2โ(2 ยท ๐)) โ
1)))) |
103 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(((๐โ๐) โ 1) = (2 ยท ((2โ(2
ยท ๐)) โ 1))
โ ((๐ โ 1)
ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) = (2 ยท ((2โ(2 ยท ๐)) โ
1)))) |
104 | 99 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
๐ โ
โ) |
105 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ 1
โ โ) |
106 | 104, 105 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(๐ โ 1) โ
โ) |
107 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (0...(๐ โ 1))
โ Fin) |
108 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ๐ โ
โ0) |
109 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ๐ โ
โ0) |
111 | 108, 110 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) โ
โ0) |
112 | 111 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) โ โค) |
113 | 107, 112 | fsumzcl 15627 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐) โ โค) |
114 | 113 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐) โ โ) |
115 | 114 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐) โ โ) |
116 | 106, 115 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) โ โ) |
117 | 56 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(2โ(2 ยท ๐))
โ โ) |
118 | 117, 105 | subcld 11519 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((2โ(2 ยท ๐))
โ 1) โ โ) |
119 | | 2rp 12927 |
. . . . . . . . . . . . . . . . . . . . 21
โข 2 โ
โ+ |
120 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ 2
โ โ+) |
121 | 120 | rpcnne0d 12973 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(2 โ โ โง 2 โ 0)) |
122 | | divmul2 11824 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) โ โ โง ((2โ(2 ยท
๐)) โ 1) โ
โ โง (2 โ โ โง 2 โ 0)) โ ((((๐ โ 1) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) / 2) = ((2โ(2 ยท ๐)) โ 1) โ ((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = (2 ยท ((2โ(2 ยท ๐)) โ
1)))) |
123 | 116, 118,
121, 122 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) / 2) = ((2โ(2 ยท ๐)) โ 1) โ ((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = (2 ยท ((2โ(2 ยท ๐)) โ
1)))) |
124 | | div23 11839 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ 1) โ โ โง
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐) โ โ โง (2 โ โ
โง 2 โ 0)) โ (((๐ โ 1) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) / 2) = (((๐ โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐))) |
125 | 106, 115,
121, 124 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) / 2) = (((๐ โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐))) |
126 | 125 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) / 2) = ((2โ(2 ยท ๐)) โ 1) โ (((๐ โ 1) / 2) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1))) |
127 | 51 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ 2 โ
โค) |
128 | | 2nn 12233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข 2 โ
โ |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ 2 โ
โ) |
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ๐ โ
โ) |
131 | 129, 130 | nnmulcld 12213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
132 | | iddvdsexp 16169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((2
โ โค โง (2 ยท ๐) โ โ) โ 2 โฅ (2โ(2
ยท ๐))) |
133 | 127, 131,
132 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ 2 โฅ
(2โ(2 ยท ๐))) |
134 | 133 | notnotd 144 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ยฌ
ยฌ 2 โฅ (2โ(2 ยท ๐))) |
135 | 55 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ
(2โ(2 ยท ๐))
โ โค) |
136 | | oddm1even 16232 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((2โ(2 ยท ๐)) โ โค โ (ยฌ 2 โฅ
(2โ(2 ยท ๐))
โ 2 โฅ ((2โ(2 ยท ๐)) โ 1))) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (ยฌ 2
โฅ (2โ(2 ยท ๐)) โ 2 โฅ ((2โ(2 ยท
๐)) โ
1))) |
138 | 134, 137 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ยฌ 2
โฅ ((2โ(2 ยท ๐)) โ 1)) |
139 | 138 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
ยฌ 2 โฅ ((2โ(2 ยท ๐)) โ 1)) |
140 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ 1) / 2) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1) โ (2 โฅ (((๐ โ 1) / 2) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) โ 2 โฅ ((2โ(2 ยท
๐)) โ
1))) |
141 | 140 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ 1) / 2) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1) โ (ยฌ 2 โฅ
(((๐ โ 1) / 2)
ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) โ ยฌ 2 โฅ ((2โ(2
ยท ๐)) โ
1))) |
142 | 141 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง (((๐ โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1)) โ (ยฌ 2 โฅ
(((๐ โ 1) / 2)
ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) โ ยฌ 2 โฅ ((2โ(2
ยท ๐)) โ
1))) |
143 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(0...(๐ โ 1)) โ
Fin) |
144 | 112 | ad4ant14 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) โ โค) |
145 | | elnn0 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
146 | | eldifsn 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
147 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข ((๐ โ โ โง ๐ โ 2) โ ๐ โ 2) |
148 | 147 | necomd 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข ((๐ โ โ โง ๐ โ 2) โ 2 โ ๐) |
149 | 146, 148 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ โ (โ โ {2})
โ 2 โ ๐) |
150 | 149 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โ โง ๐ โ (โ โ {2}))
โ 2 โ ๐) |
151 | 150 | neneqd 2949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง ๐ โ (โ โ {2}))
โ ยฌ 2 = ๐) |
152 | | 2prm 16575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข 2 โ
โ |
153 | 11 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โ โง ๐ โ (โ โ {2}))
โ ๐ โ
โ) |
154 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โ โง ๐ โ (โ โ {2}))
โ ๐ โ
โ) |
155 | | prmdvdsexpb 16599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((2
โ โ โง ๐
โ โ โง ๐
โ โ) โ (2 โฅ (๐โ๐) โ 2 = ๐)) |
156 | 152, 153,
154, 155 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง ๐ โ (โ โ {2}))
โ (2 โฅ (๐โ๐) โ 2 = ๐)) |
157 | 151, 156 | mtbird 325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ โ โง ๐ โ (โ โ {2}))
โ ยฌ 2 โฅ (๐โ๐)) |
158 | 157 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ โ โ โ (๐ โ (โ โ {2})
โ ยฌ 2 โฅ (๐โ๐))) |
159 | | n2dvds1 16257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ยฌ 2
โฅ 1 |
160 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ = 0 โ (๐โ๐) = (๐โ0)) |
161 | 98 | exp0d 14052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ โ (โ โ {2})
โ (๐โ0) =
1) |
162 | 160, 161 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ (๐โ๐) = 1) |
163 | 162 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ (2
โฅ (๐โ๐) โ 2 โฅ
1)) |
164 | 159, 163 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ ยฌ
2 โฅ (๐โ๐)) |
165 | 164 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ = 0 โ (๐ โ (โ โ {2}) โ ยฌ 2
โฅ (๐โ๐))) |
166 | 158, 165 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โจ ๐ = 0) โ (๐ โ (โ โ {2}) โ ยฌ 2
โฅ (๐โ๐))) |
167 | 145, 166 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ0
โ (๐ โ (โ
โ {2}) โ ยฌ 2 โฅ (๐โ๐))) |
168 | 167, 109 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ (โ โ {2})
โ (๐ โ
(0...(๐ โ 1)) โ
ยฌ 2 โฅ (๐โ๐))) |
169 | 168 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โ
(0...(๐ โ 1)) โ
ยฌ 2 โฅ (๐โ๐))) |
170 | 169 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(๐ โ (0...(๐ โ 1)) โ ยฌ 2
โฅ (๐โ๐))) |
171 | 170 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง ๐ โ (0...(๐ โ 1))) โ ยฌ 2 โฅ (๐โ๐)) |
172 | | nnm1nn0 12461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
173 | | hashfz0 14339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ 1) โ
โ0 โ (โฏโ(0...(๐ โ 1))) = ((๐ โ 1) + 1)) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โ โ
(โฏโ(0...(๐
โ 1))) = ((๐ โ
1) + 1)) |
175 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ โ โ โ ๐ โ
โ) |
176 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ โ โ โ 1 โ
โ) |
177 | 175, 176 | npcand 11523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
178 | 174, 177 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ ๐ = (โฏโ(0...(๐ โ 1)))) |
179 | 178 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ =
(โฏโ(0...(๐
โ 1)))) |
180 | 179 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ ๐ =
(โฏโ(0...(๐
โ 1)))) |
181 | 180 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (2 โฅ ๐ โ
2 โฅ (โฏโ(0...(๐ โ 1))))) |
182 | 181 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ 2
โฅ (โฏโ(0...(๐ โ 1)))) |
183 | 143, 144,
171, 182 | evensumodd 16278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ 2
โฅ ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) |
184 | 183 | olcd 873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(2 โฅ ((๐ โ 1) /
2) โจ 2 โฅ ฮฃ๐
โ (0...(๐ โ
1))(๐โ๐))) |
185 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
186 | | oddn2prm 16691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ (โ โ {2})
โ ยฌ 2 โฅ ๐) |
187 | | oddm1d2 16249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
188 | 15, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ (โ โ {2})
โ (ยฌ 2 โฅ ๐
โ ((๐ โ 1) / 2)
โ โค)) |
189 | 186, 188 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โค) |
190 | 189 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((๐ โ 1) / 2)
โ โค) |
191 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (0...(๐ โ 1))
โ Fin) |
192 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ๐ โ
โ0) |
193 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ๐ โ
โ0) |
194 | 192, 193 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) โ
โ0) |
195 | 194 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) โ โค) |
196 | 191, 195 | fsumzcl 15627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐) โ โค) |
197 | 185, 190,
196 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2 โ โ โง ((๐ โ 1) / 2) โ โค โง
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐) โ โค)) |
198 | 197 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (2 โ โ โง ((๐ โ 1) / 2) โ โค โง
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐) โ โค)) |
199 | | euclemma 16596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((2
โ โ โง ((๐
โ 1) / 2) โ โค โง ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐) โ โค) โ (2 โฅ (((๐ โ 1) / 2) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) โ (2 โฅ ((๐ โ 1) / 2) โจ 2 โฅ ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)))) |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (2 โฅ (((๐
โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) โ (2 โฅ ((๐ โ 1) / 2) โจ 2 โฅ ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)))) |
201 | 200 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(2 โฅ (((๐ โ 1)
/ 2) ยท ฮฃ๐
โ (0...(๐ โ
1))(๐โ๐)) โ (2 โฅ ((๐ โ 1) / 2) โจ 2 โฅ
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)))) |
202 | 184, 201 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ 2
โฅ (((๐ โ 1) /
2) ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐))) |
203 | 202 | pm2.24d 151 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(ยฌ 2 โฅ (((๐
โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) โ ๐ = 1)) |
204 | 203 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง (((๐ โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1)) โ (ยฌ 2 โฅ
(((๐ โ 1) / 2)
ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) โ ๐ = 1)) |
205 | 142, 204 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง (((๐ โ 1) / 2) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1)) โ (ยฌ 2 โฅ
((2โ(2 ยท ๐))
โ 1) โ ๐ =
1)) |
206 | 205 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((((๐ โ 1) / 2)
ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1) โ (ยฌ 2 โฅ
((2โ(2 ยท ๐))
โ 1) โ ๐ =
1))) |
207 | 139, 206 | mpid 44 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((((๐ โ 1) / 2)
ยท ฮฃ๐ โ
(0...(๐ โ 1))(๐โ๐)) = ((2โ(2 ยท ๐)) โ 1) โ ๐ = 1)) |
208 | 126, 207 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
((((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) / 2) = ((2โ(2 ยท ๐)) โ 1) โ ๐ = 1)) |
209 | 123, 208 | sylbird 260 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(((๐ โ 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))(๐โ๐)) = (2 ยท ((2โ(2 ยท ๐)) โ 1)) โ ๐ = 1)) |
210 | 103, 209 | sylbid 239 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(((๐โ๐) โ 1) = (2 ยท ((2โ(2
ยท ๐)) โ 1))
โ ๐ =
1)) |
211 | 96, 210 | sylbird 260 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง 2 โฅ ๐) โ
(((2 ยท ((2โ(2 ยท ๐)) โ 1)) + 1) = (๐โ๐) โ ๐ = 1)) |
212 | 211 | adantr 482 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง ((2 ยท ๐) + 1) = ๐) โ (((2 ยท ((2โ(2 ยท
๐)) โ 1)) + 1) =
(๐โ๐) โ ๐ = 1)) |
213 | 84, 212 | sylbid 239 |
. . . . . . . . . . . . 13
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง 2 โฅ ๐) โง ((2 ยท ๐) + 1) = ๐) โ (((2โ๐) โ 1) = (๐โ๐) โ ๐ = 1)) |
214 | 213 | exp31 421 |
. . . . . . . . . . . 12
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (2 โฅ ๐ โ
(((2 ยท ๐) + 1) =
๐ โ (((2โ๐) โ 1) = (๐โ๐) โ ๐ = 1)))) |
215 | 214 | com23 86 |
. . . . . . . . . . 11
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (((2 ยท ๐) +
1) = ๐ โ (2 โฅ
๐ โ (((2โ๐) โ 1) = (๐โ๐) โ ๐ = 1)))) |
216 | 215 | rexlimdva 3153 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (โ๐ โ
โ ((2 ยท ๐) +
1) = ๐ โ (2 โฅ
๐ โ (((2โ๐) โ 1) = (๐โ๐) โ ๐ = 1)))) |
217 | 216 | com34 91 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (โ๐ โ
โ ((2 ยท ๐) +
1) = ๐ โ
(((2โ๐) โ 1) =
(๐โ๐) โ (2 โฅ ๐ โ ๐ = 1)))) |
218 | 217 | adantr 482 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(โ๐ โ โ
((2 ยท ๐) + 1) =
๐ โ (((2โ๐) โ 1) = (๐โ๐) โ (2 โฅ ๐ โ ๐ = 1)))) |
219 | 45, 218 | sylbid 239 |
. . . . . . 7
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(ยฌ 2 โฅ ๐ โ
(((2โ๐) โ 1) =
(๐โ๐) โ (2 โฅ ๐ โ ๐ = 1)))) |
220 | 219 | com24 95 |
. . . . . 6
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(2 โฅ ๐ โ
(((2โ๐) โ 1) =
(๐โ๐) โ (ยฌ 2 โฅ ๐ โ ๐ = 1)))) |
221 | 220 | ex 414 |
. . . . 5
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (ยฌ ๐ = 1 โ
(2 โฅ ๐ โ
(((2โ๐) โ 1) =
(๐โ๐) โ (ยฌ 2 โฅ ๐ โ ๐ = 1))))) |
222 | 221 | com25 99 |
. . . 4
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (ยฌ 2 โฅ ๐
โ (2 โฅ ๐ โ
(((2โ๐) โ 1) =
(๐โ๐) โ (ยฌ ๐ = 1 โ ๐ = 1))))) |
223 | 222 | impd 412 |
. . 3
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((ยฌ 2 โฅ ๐
โง 2 โฅ ๐) โ
(((2โ๐) โ 1) =
(๐โ๐) โ (ยฌ ๐ = 1 โ ๐ = 1)))) |
224 | 223 | 3imp 1112 |
. 2
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ 2 โฅ ๐
โง 2 โฅ ๐) โง
((2โ๐) โ 1) =
(๐โ๐)) โ (ยฌ ๐ = 1 โ ๐ = 1)) |
225 | 38, 224 | pm2.61d 179 |
1
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ 2 โฅ ๐
โง 2 โฅ ๐) โง
((2โ๐) โ 1) =
(๐โ๐)) โ ๐ = 1) |