Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
2 | 1 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
3 | | 2pos 12263 |
. . . . . . . . . 10
โข 0 <
2 |
4 | 3 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 < 2) |
5 | | aks4d1p9.1 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
(โคโฅโ3)) |
6 | | eluzelz 12780 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ3) โ ๐ โ โค) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
8 | 7 | zred 12614 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
9 | | 0red 11165 |
. . . . . . . . . 10
โข (๐ โ 0 โ
โ) |
10 | | 3re 12240 |
. . . . . . . . . . 11
โข 3 โ
โ |
11 | 10 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 3 โ
โ) |
12 | | 3pos 12265 |
. . . . . . . . . . 11
โข 0 <
3 |
13 | 12 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 0 < 3) |
14 | | eluzle 12783 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ3) โ 3 โค ๐) |
15 | 5, 14 | syl 17 |
. . . . . . . . . 10
โข (๐ โ 3 โค ๐) |
16 | 9, 11, 8, 13, 15 | ltletrd 11322 |
. . . . . . . . 9
โข (๐ โ 0 < ๐) |
17 | | 1red 11163 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โ) |
18 | | 1lt2 12331 |
. . . . . . . . . . . 12
โข 1 <
2 |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 1 < 2) |
20 | 17, 19 | ltned 11298 |
. . . . . . . . . 10
โข (๐ โ 1 โ 2) |
21 | 20 | necomd 3000 |
. . . . . . . . 9
โข (๐ โ 2 โ 1) |
22 | 2, 4, 8, 16, 21 | relogbcld 40459 |
. . . . . . . 8
โข (๐ โ (2 logb ๐) โ
โ) |
23 | 22 | resqcld 14037 |
. . . . . . 7
โข (๐ โ ((2 logb ๐)โ2) โ
โ) |
24 | | aks4d1p9.2 |
. . . . . . . . . . . . 13
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
25 | | aks4d1p9.3 |
. . . . . . . . . . . . 13
โข ๐ต = (โโ((2
logb ๐)โ5)) |
26 | | aks4d1p9.4 |
. . . . . . . . . . . . 13
โข ๐
= inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) |
27 | 5, 24, 25, 26 | aks4d1p4 40565 |
. . . . . . . . . . . 12
โข (๐ โ (๐
โ (1...๐ต) โง ยฌ ๐
โฅ ๐ด)) |
28 | 27 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ (1...๐ต)) |
29 | | elfznn 13477 |
. . . . . . . . . . 11
โข (๐
โ (1...๐ต) โ ๐
โ โ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐
โ โ) |
31 | 5, 24, 25, 26 | aks4d1p8 40573 |
. . . . . . . . . 10
โข (๐ โ (๐ gcd ๐
) = 1) |
32 | 30, 7, 31 | 3jca 1129 |
. . . . . . . . 9
โข (๐ โ (๐
โ โ โง ๐ โ โค โง (๐ gcd ๐
) = 1)) |
33 | | odzcl 16672 |
. . . . . . . . 9
โข ((๐
โ โ โง ๐ โ โค โง (๐ gcd ๐
) = 1) โ
((odโคโ๐
)โ๐) โ โ) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
โข (๐ โ
((odโคโ๐
)โ๐) โ โ) |
35 | 34 | nnzd 12533 |
. . . . . . 7
โข (๐ โ
((odโคโ๐
)โ๐) โ โค) |
36 | | flge 13717 |
. . . . . . 7
โข ((((2
logb ๐)โ2)
โ โ โง ((odโคโ๐
)โ๐) โ โค) โ
(((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2) โ
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2)))) |
37 | 23, 35, 36 | syl2anc 585 |
. . . . . 6
โข (๐ โ
(((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2) โ
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2)))) |
38 | 37 | biimpd 228 |
. . . . 5
โข (๐ โ
(((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2) โ
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2)))) |
39 | 38 | imp 408 |
. . . 4
โข ((๐ โง
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2)) โ
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) |
40 | 30 | nnzd 12533 |
. . . . . . . . 9
โข (๐ โ ๐
โ โค) |
41 | 40 | adantr 482 |
. . . . . . . 8
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐
โ
โค) |
42 | 7 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐ โ
โค) |
43 | 34 | nnnn0d 12480 |
. . . . . . . . . . 11
โข (๐ โ
((odโคโ๐
)โ๐) โ
โ0) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
((odโคโ๐
)โ๐) โ
โ0) |
45 | 42, 44 | zexpcld 14000 |
. . . . . . . . 9
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ (๐โ((odโคโ๐
)โ๐)) โ โค) |
46 | | 1zzd 12541 |
. . . . . . . . 9
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ 1
โ โค) |
47 | 45, 46 | zsubcld 12619 |
. . . . . . . 8
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((๐โ((odโคโ๐
)โ๐)) โ 1) โ
โค) |
48 | 5, 25 | aks4d1lem1 40548 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ต โ โ โง 9 < ๐ต)) |
49 | 48 | simpld 496 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ โ) |
50 | 49 | nnred 12175 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ โ) |
51 | 49 | nngt0d 12209 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < ๐ต) |
52 | 2, 4, 50, 51, 21 | relogbcld 40459 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 logb ๐ต) โ
โ) |
53 | 52 | flcld 13710 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ(2
logb ๐ต)) โ
โค) |
54 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โ
โ) |
55 | 9, 4 | gtned 11297 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โ 0) |
56 | 54, 55, 21 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 โ โ โง 2
โ 0 โง 2 โ 1)) |
57 | | logb1 26135 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง 2 โ 0 โง 2 โ 1) โ (2 logb 1) =
0) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 logb 1) =
0) |
59 | | 2z 12542 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โค |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ
โค) |
61 | 2 | leidd 11728 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โค 2) |
62 | | 0lt1 11684 |
. . . . . . . . . . . . . . . . . 18
โข 0 <
1 |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 0 < 1) |
64 | 49 | nnge1d 12208 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โค ๐ต) |
65 | 60, 61, 17, 63, 50, 51, 64 | logblebd 40462 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 logb 1) โค
(2 logb ๐ต)) |
66 | 58, 65 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โค (2 logb
๐ต)) |
67 | | 0zd 12518 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 โ
โค) |
68 | | flge 13717 |
. . . . . . . . . . . . . . . 16
โข (((2
logb ๐ต) โ
โ โง 0 โ โค) โ (0 โค (2 logb ๐ต) โ 0 โค
(โโ(2 logb ๐ต)))) |
69 | 52, 67, 68 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 โค (2 logb
๐ต) โ 0 โค
(โโ(2 logb ๐ต)))) |
70 | 66, 69 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 โค (โโ(2
logb ๐ต))) |
71 | 53, 70 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(2
logb ๐ต)) โ
โค โง 0 โค (โโ(2 logb ๐ต)))) |
72 | | elnn0z 12519 |
. . . . . . . . . . . . 13
โข
((โโ(2 logb ๐ต)) โ โ0 โ
((โโ(2 logb ๐ต)) โ โค โง 0 โค
(โโ(2 logb ๐ต)))) |
73 | 71, 72 | sylibr 233 |
. . . . . . . . . . . 12
โข (๐ โ (โโ(2
logb ๐ต)) โ
โ0) |
74 | 7, 73 | zexpcld 14000 |
. . . . . . . . . . 11
โข (๐ โ (๐โ(โโ(2 logb
๐ต))) โ
โค) |
75 | | fzfid 13885 |
. . . . . . . . . . . 12
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ Fin) |
76 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โค) |
77 | | elfznn 13477 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ ๐ โ โ) |
78 | 77 | nnnn0d 12480 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ ๐ โ โ0) |
79 | 78 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ0) |
80 | 76, 79 | zexpcld 14000 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) โ โค) |
81 | | 1zzd 12541 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โ
โค) |
82 | 80, 81 | zsubcld 12619 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 1) โ โค) |
83 | 75, 82 | fprodzcl 15844 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1) โ โค) |
84 | 74, 83 | zmulcld 12620 |
. . . . . . . . . 10
โข (๐ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โ
โค) |
85 | 24 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
86 | 85 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ โ (๐ด โ โค โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โ
โค)) |
87 | 84, 86 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โค) |
88 | 87 | adantr 482 |
. . . . . . . 8
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐ด โ
โค) |
89 | | iddvds 16159 |
. . . . . . . . . . 11
โข
(((odโคโ๐
)โ๐) โ โค โ
((odโคโ๐
)โ๐) โฅ ((odโคโ๐
)โ๐)) |
90 | 35, 89 | syl 17 |
. . . . . . . . . 10
โข (๐ โ
((odโคโ๐
)โ๐) โฅ ((odโคโ๐
)โ๐)) |
91 | | odzdvds 16674 |
. . . . . . . . . . 11
โข (((๐
โ โ โง ๐ โ โค โง (๐ gcd ๐
) = 1) โง
((odโคโ๐
)โ๐) โ โ0) โ (๐
โฅ ((๐โ((odโคโ๐
)โ๐)) โ 1) โ
((odโคโ๐
)โ๐) โฅ ((odโคโ๐
)โ๐))) |
92 | 32, 43, 91 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ (๐
โฅ ((๐โ((odโคโ๐
)โ๐)) โ 1) โ
((odโคโ๐
)โ๐) โฅ ((odโคโ๐
)โ๐))) |
93 | 90, 92 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ ๐
โฅ ((๐โ((odโคโ๐
)โ๐)) โ 1)) |
94 | 93 | adantr 482 |
. . . . . . . 8
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐
โฅ ((๐โ((odโคโ๐
)โ๐)) โ 1)) |
95 | 73 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
(โโ(2 logb ๐ต)) โ
โ0) |
96 | 42, 95 | zexpcld 14000 |
. . . . . . . . . 10
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ (๐โ(โโ(2
logb ๐ต))) โ
โค) |
97 | | fzfid 13885 |
. . . . . . . . . . 11
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
(1...(โโ((2 logb ๐)โ2))) โ Fin) |
98 | 42 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โค) |
99 | 77 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
100 | 99 | nnnn0d 12480 |
. . . . . . . . . . . . 13
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ0) |
101 | 98, 100 | zexpcld 14000 |
. . . . . . . . . . . 12
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) โ โค) |
102 | | 1zzd 12541 |
. . . . . . . . . . . 12
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โ
โค) |
103 | 101, 102 | zsubcld 12619 |
. . . . . . . . . . 11
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 1) โ โค) |
104 | 97, 103 | fprodzcl 15844 |
. . . . . . . . . 10
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
โ๐ โ
(1...(โโ((2 logb ๐)โ2)))((๐โ๐) โ 1) โ โค) |
105 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ง =
((odโคโ๐
)โ๐) โ ((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐ง) = ((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ
1))โ((odโคโ๐
)โ๐))) |
106 | 105 | breq1d 5120 |
. . . . . . . . . . . 12
โข (๐ง =
((odโคโ๐
)โ๐) โ (((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐ง) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐) โ ((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ
1))โ((odโคโ๐
)โ๐)) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐))) |
107 | | ssidd 3972 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ (1...(โโ((2
logb ๐)โ2)))) |
108 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โค) |
109 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โ ๐ฅ โ โ) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ฅ โ โ) |
111 | 110 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ฅ โ โ0) |
112 | 108, 111 | zexpcld 14000 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐ฅ) โ โค) |
113 | | 1zzd 12541 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โ
โค) |
114 | 112, 113 | zsubcld 12619 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐ฅ) โ 1) โ โค) |
115 | 114 | fmpttd 7068 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1)):(1...(โโ((2
logb ๐)โ2)))โถโค) |
116 | 75, 107, 115 | fprodfvdvdsd 16223 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ง โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐ง) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐)) |
117 | 116 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
โ๐ง โ
(1...(โโ((2 logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐ง) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐)) |
118 | 22 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ (2
logb ๐) โ
โ) |
119 | 118 | resqcld 14037 |
. . . . . . . . . . . . . 14
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((2
logb ๐)โ2)
โ โ) |
120 | 119 | flcld 13710 |
. . . . . . . . . . . . 13
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
(โโ((2 logb ๐)โ2)) โ โค) |
121 | 35 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
((odโคโ๐
)โ๐) โ โค) |
122 | 34 | nnge1d 12208 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โค
((odโคโ๐
)โ๐)) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ 1 โค
((odโคโ๐
)โ๐)) |
124 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) |
125 | 46, 120, 121, 123, 124 | elfzd 13439 |
. . . . . . . . . . . 12
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
((odโคโ๐
)โ๐) โ (1...(โโ((2
logb ๐)โ2)))) |
126 | 106, 117,
125 | rspcdva 3585 |
. . . . . . . . . . 11
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ
1))โ((odโคโ๐
)โ๐)) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐)) |
127 | | eqidd 2738 |
. . . . . . . . . . . . 13
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ (๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1)) = (๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))) |
128 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ฅ =
((odโคโ๐
)โ๐)) โ ๐ฅ = ((odโคโ๐
)โ๐)) |
129 | 128 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ฅ =
((odโคโ๐
)โ๐)) โ (๐โ๐ฅ) = (๐โ((odโคโ๐
)โ๐))) |
130 | 129 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ฅ =
((odโคโ๐
)โ๐)) โ ((๐โ๐ฅ) โ 1) = ((๐โ((odโคโ๐
)โ๐)) โ 1)) |
131 | 127, 130,
125, 47 | fvmptd 6960 |
. . . . . . . . . . . 12
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ
1))โ((odโคโ๐
)โ๐)) = ((๐โ((odโคโ๐
)โ๐)) โ 1)) |
132 | | eqidd 2738 |
. . . . . . . . . . . . . 14
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1)) = (๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))) |
133 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โง ๐ฅ = ๐) โ ๐ฅ = ๐) |
134 | 133 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โง ๐ฅ = ๐) โ (๐โ๐ฅ) = (๐โ๐)) |
135 | 134 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข ((((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โง ๐ฅ = ๐) โ ((๐โ๐ฅ) โ 1) = ((๐โ๐) โ 1)) |
136 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ (1...(โโ((2
logb ๐)โ2)))) |
137 | 132, 135,
136, 103 | fvmptd 6960 |
. . . . . . . . . . . . 13
โข (((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐) = ((๐โ๐) โ 1)) |
138 | 137 | prodeq2dv 15813 |
. . . . . . . . . . . 12
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
โ๐ โ
(1...(โโ((2 logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐) = โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
139 | 131, 138 | breq12d 5123 |
. . . . . . . . . . 11
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ
(((๐ฅ โ
(1...(โโ((2 logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ
1))โ((odโคโ๐
)โ๐)) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐ฅ โ (1...(โโ((2
logb ๐)โ2))) โฆ ((๐โ๐ฅ) โ 1))โ๐) โ ((๐โ((odโคโ๐
)โ๐)) โ 1) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
140 | 126, 139 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((๐โ((odโคโ๐
)โ๐)) โ 1) โฅ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
141 | 47, 96, 104, 140 | dvdsmultr2d 16188 |
. . . . . . . . 9
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((๐โ((odโคโ๐
)โ๐)) โ 1) โฅ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
142 | 24 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
143 | 141, 142 | breqtrrd 5138 |
. . . . . . . 8
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ((๐โ((odโคโ๐
)โ๐)) โ 1) โฅ ๐ด) |
144 | 41, 47, 88, 94, 143 | dvdstrd 16184 |
. . . . . . 7
โข ((๐ โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐
โฅ ๐ด) |
145 | 144 | ex 414 |
. . . . . 6
โข (๐ โ
(((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2)) โ ๐
โฅ ๐ด)) |
146 | 145 | adantr 482 |
. . . . 5
โข ((๐ โง
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2)) โ
(((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2)) โ ๐
โฅ ๐ด)) |
147 | 146 | imp 408 |
. . . 4
โข (((๐ โง
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2)) โง
((odโคโ๐
)โ๐) โค (โโ((2 logb
๐)โ2))) โ ๐
โฅ ๐ด) |
148 | 39, 147 | mpdan 686 |
. . 3
โข ((๐ โง
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2)) โ ๐
โฅ ๐ด) |
149 | 27 | simprd 497 |
. . . 4
โข (๐ โ ยฌ ๐
โฅ ๐ด) |
150 | 149 | adantr 482 |
. . 3
โข ((๐ โง
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2)) โ ยฌ ๐
โฅ ๐ด) |
151 | 148, 150 | pm2.65da 816 |
. 2
โข (๐ โ ยฌ
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2)) |
152 | 34 | nnred 12175 |
. . 3
โข (๐ โ
((odโคโ๐
)โ๐) โ โ) |
153 | 23, 152 | ltnled 11309 |
. 2
โข (๐ โ (((2 logb ๐)โ2) <
((odโคโ๐
)โ๐) โ ยฌ
((odโคโ๐
)โ๐) โค ((2 logb ๐)โ2))) |
154 | 151, 153 | mpbird 257 |
1
โข (๐ โ ((2 logb ๐)โ2) <
((odโคโ๐
)โ๐)) |