Step | Hyp | Ref
| Expression |
1 | | bposlem2.1 |
. . 3
โข (๐ โ ๐ โ โ) |
2 | | bposlem2.2 |
. . 3
โข (๐ โ ๐ โ โ) |
3 | | pcbcctr 26768 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |
4 | 1, 2, 3 | syl2anc 584 |
. 2
โข (๐ โ (๐ pCnt ((2 ยท ๐)C๐)) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |
5 | | elfznn 13526 |
. . . . . 6
โข (๐ โ (1...(2 ยท ๐)) โ ๐ โ โ) |
6 | | elnn1uz2 12905 |
. . . . . 6
โข (๐ โ โ โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
7 | 5, 6 | sylib 217 |
. . . . 5
โข (๐ โ (1...(2 ยท ๐)) โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
8 | | oveq2 7413 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (๐โ๐) = (๐โ1)) |
9 | | prmnn 16607 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
10 | 2, 9 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
11 | 10 | nncnd 12224 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
12 | 11 | exp1d 14102 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ1) = ๐) |
13 | 8, 12 | sylan9eqr 2794 |
. . . . . . . . . . 11
โข ((๐ โง ๐ = 1) โ (๐โ๐) = ๐) |
14 | 13 | oveq2d 7421 |
. . . . . . . . . 10
โข ((๐ โง ๐ = 1) โ ((2 ยท ๐) / (๐โ๐)) = ((2 ยท ๐) / ๐)) |
15 | 14 | fveq2d 6892 |
. . . . . . . . 9
โข ((๐ โง ๐ = 1) โ (โโ((2 ยท
๐) / (๐โ๐))) = (โโ((2 ยท ๐) / ๐))) |
16 | | 2t1e2 12371 |
. . . . . . . . . . . . 13
โข (2
ยท 1) = 2 |
17 | 11 | mullidd 11228 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 ยท ๐) = ๐) |
18 | | bposlem2.5 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โค ๐) |
19 | 17, 18 | eqbrtrd 5169 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ยท ๐) โค ๐) |
20 | | 1red 11211 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โ
โ) |
21 | 1 | nnred 12223 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
22 | 10 | nnred 12223 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
23 | 10 | nngt0d 12257 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < ๐) |
24 | | lemuldiv 12090 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ๐
โ โ โง (๐
โ โ โง 0 < ๐)) โ ((1 ยท ๐) โค ๐ โ 1 โค (๐ / ๐))) |
25 | 20, 21, 22, 23, 24 | syl112anc 1374 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((1 ยท ๐) โค ๐ โ 1 โค (๐ / ๐))) |
26 | 19, 25 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โค (๐ / ๐)) |
27 | 21, 10 | nndivred 12262 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ / ๐) โ โ) |
28 | | 1re 11210 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
29 | | 2re 12282 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
30 | | 2pos 12311 |
. . . . . . . . . . . . . . . . 17
โข 0 <
2 |
31 | 29, 30 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
โข (2 โ
โ โง 0 < 2) |
32 | | lemul2 12063 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง (๐ /
๐) โ โ โง (2
โ โ โง 0 < 2)) โ (1 โค (๐ / ๐) โ (2 ยท 1) โค (2 ยท
(๐ / ๐)))) |
33 | 28, 31, 32 | mp3an13 1452 |
. . . . . . . . . . . . . . 15
โข ((๐ / ๐) โ โ โ (1 โค (๐ / ๐) โ (2 ยท 1) โค (2 ยท
(๐ / ๐)))) |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (1 โค (๐ / ๐) โ (2 ยท 1) โค (2 ยท
(๐ / ๐)))) |
35 | 26, 34 | mpbid 231 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท 1) โค (2
ยท (๐ / ๐))) |
36 | 16, 35 | eqbrtrrid 5183 |
. . . . . . . . . . . 12
โข (๐ โ 2 โค (2 ยท (๐ / ๐))) |
37 | | 2cnd 12286 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ
โ) |
38 | 1 | nncnd 12224 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
39 | 10 | nnne0d 12258 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ 0) |
40 | 37, 38, 11, 39 | divassd 12021 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) / ๐) = (2 ยท (๐ / ๐))) |
41 | 36, 40 | breqtrrd 5175 |
. . . . . . . . . . 11
โข (๐ โ 2 โค ((2 ยท ๐) / ๐)) |
42 | | bposlem2.4 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐) / 3) < ๐) |
43 | | 2nn 12281 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ |
44 | | nnmulcl 12232 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
45 | 43, 1, 44 | sylancr 587 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท ๐) โ
โ) |
46 | 45 | nnred 12223 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 ยท ๐) โ
โ) |
47 | | 3re 12288 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ |
48 | | 3pos 12313 |
. . . . . . . . . . . . . . . 16
โข 0 <
3 |
49 | 47, 48 | pm3.2i 471 |
. . . . . . . . . . . . . . 15
โข (3 โ
โ โง 0 < 3) |
50 | | ltdiv23 12101 |
. . . . . . . . . . . . . . 15
โข (((2
ยท ๐) โ โ
โง (3 โ โ โง 0 < 3) โง (๐ โ โ โง 0 < ๐)) โ (((2 ยท ๐) / 3) < ๐ โ ((2 ยท ๐) / ๐) < 3)) |
51 | 49, 50 | mp3an2 1449 |
. . . . . . . . . . . . . 14
โข (((2
ยท ๐) โ โ
โง (๐ โ โ
โง 0 < ๐)) โ
(((2 ยท ๐) / 3) <
๐ โ ((2 ยท ๐) / ๐) < 3)) |
52 | 46, 22, 23, 51 | syl12anc 835 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท ๐) / 3) < ๐ โ ((2 ยท ๐) / ๐) < 3)) |
53 | 42, 52 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) / ๐) < 3) |
54 | | df-3 12272 |
. . . . . . . . . . . 12
โข 3 = (2 +
1) |
55 | 53, 54 | breqtrdi 5188 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) / ๐) < (2 + 1)) |
56 | 46, 10 | nndivred 12262 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) / ๐) โ โ) |
57 | | 2z 12590 |
. . . . . . . . . . . 12
โข 2 โ
โค |
58 | | flbi 13777 |
. . . . . . . . . . . 12
โข ((((2
ยท ๐) / ๐) โ โ โง 2 โ
โค) โ ((โโ((2 ยท ๐) / ๐)) = 2 โ (2 โค ((2 ยท ๐) / ๐) โง ((2 ยท ๐) / ๐) < (2 + 1)))) |
59 | 56, 57, 58 | sylancl 586 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((2
ยท ๐) / ๐)) = 2 โ (2 โค ((2
ยท ๐) / ๐) โง ((2 ยท ๐) / ๐) < (2 + 1)))) |
60 | 41, 55, 59 | mpbir2and 711 |
. . . . . . . . . 10
โข (๐ โ (โโ((2
ยท ๐) / ๐)) = 2) |
61 | 60 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ๐ = 1) โ (โโ((2 ยท
๐) / ๐)) = 2) |
62 | 15, 61 | eqtrd 2772 |
. . . . . . . 8
โข ((๐ โง ๐ = 1) โ (โโ((2 ยท
๐) / (๐โ๐))) = 2) |
63 | 13 | oveq2d 7421 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ = 1) โ (๐ / (๐โ๐)) = (๐ / ๐)) |
64 | 63 | fveq2d 6892 |
. . . . . . . . . . 11
โข ((๐ โง ๐ = 1) โ (โโ(๐ / (๐โ๐))) = (โโ(๐ / ๐))) |
65 | | remulcl 11191 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โ โง (๐ /
๐) โ โ) โ
(2 ยท (๐ / ๐)) โ
โ) |
66 | 29, 27, 65 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท (๐ / ๐)) โ โ) |
67 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 3 โ
โ) |
68 | | 4re 12292 |
. . . . . . . . . . . . . . . . . 18
โข 4 โ
โ |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 4 โ
โ) |
70 | 40, 53 | eqbrtrrd 5171 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท (๐ / ๐)) < 3) |
71 | | 3lt4 12382 |
. . . . . . . . . . . . . . . . . 18
โข 3 <
4 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 3 < 4) |
73 | 66, 67, 69, 70, 72 | lttrd 11371 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 ยท (๐ / ๐)) < 4) |
74 | | 2t2e4 12372 |
. . . . . . . . . . . . . . . 16
โข (2
ยท 2) = 4 |
75 | 73, 74 | breqtrrdi 5189 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท (๐ / ๐)) < (2 ยท 2)) |
76 | | ltmul2 12061 |
. . . . . . . . . . . . . . . . 17
โข (((๐ / ๐) โ โ โง 2 โ โ
โง (2 โ โ โง 0 < 2)) โ ((๐ / ๐) < 2 โ (2 ยท (๐ / ๐)) < (2 ยท 2))) |
77 | 29, 31, 76 | mp3an23 1453 |
. . . . . . . . . . . . . . . 16
โข ((๐ / ๐) โ โ โ ((๐ / ๐) < 2 โ (2 ยท (๐ / ๐)) < (2 ยท 2))) |
78 | 27, 77 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ / ๐) < 2 โ (2 ยท (๐ / ๐)) < (2 ยท 2))) |
79 | 75, 78 | mpbird 256 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / ๐) < 2) |
80 | | df-2 12271 |
. . . . . . . . . . . . . 14
โข 2 = (1 +
1) |
81 | 79, 80 | breqtrdi 5188 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ / ๐) < (1 + 1)) |
82 | | 1z 12588 |
. . . . . . . . . . . . . 14
โข 1 โ
โค |
83 | | flbi 13777 |
. . . . . . . . . . . . . 14
โข (((๐ / ๐) โ โ โง 1 โ โค)
โ ((โโ(๐ /
๐)) = 1 โ (1 โค
(๐ / ๐) โง (๐ / ๐) < (1 + 1)))) |
84 | 27, 82, 83 | sylancl 586 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(๐ / ๐)) = 1 โ (1 โค (๐ / ๐) โง (๐ / ๐) < (1 + 1)))) |
85 | 26, 81, 84 | mpbir2and 711 |
. . . . . . . . . . . 12
โข (๐ โ (โโ(๐ / ๐)) = 1) |
86 | 85 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โง ๐ = 1) โ (โโ(๐ / ๐)) = 1) |
87 | 64, 86 | eqtrd 2772 |
. . . . . . . . . 10
โข ((๐ โง ๐ = 1) โ (โโ(๐ / (๐โ๐))) = 1) |
88 | 87 | oveq2d 7421 |
. . . . . . . . 9
โข ((๐ โง ๐ = 1) โ (2 ยท
(โโ(๐ / (๐โ๐)))) = (2 ยท 1)) |
89 | 88, 16 | eqtrdi 2788 |
. . . . . . . 8
โข ((๐ โง ๐ = 1) โ (2 ยท
(โโ(๐ / (๐โ๐)))) = 2) |
90 | 62, 89 | oveq12d 7423 |
. . . . . . 7
โข ((๐ โง ๐ = 1) โ ((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = (2 โ 2)) |
91 | | 2cn 12283 |
. . . . . . . 8
โข 2 โ
โ |
92 | 91 | subidi 11527 |
. . . . . . 7
โข (2
โ 2) = 0 |
93 | 90, 92 | eqtrdi 2788 |
. . . . . 6
โข ((๐ โง ๐ = 1) โ ((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = 0) |
94 | 45 | nnrpd 13010 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ
โ+) |
95 | 94 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท ๐)
โ โ+) |
96 | | eluzge2nn0 12867 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ0) |
97 | | nnexpcl 14036 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
98 | 10, 96, 97 | syl2an 596 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐โ๐) โ
โ) |
99 | 98 | nnrpd 13010 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐โ๐) โ
โ+) |
100 | 95, 99 | rpdivcld 13029 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((2 ยท ๐) /
(๐โ๐)) โ
โ+) |
101 | 100 | rpge0d 13016 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ2))
โ 0 โค ((2 ยท ๐) / (๐โ๐))) |
102 | 46 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท ๐)
โ โ) |
103 | | remulcl 11191 |
. . . . . . . . . . . . . . 15
โข ((3
โ โ โง ๐
โ โ) โ (3 ยท ๐) โ โ) |
104 | 47, 22, 103 | sylancr 587 |
. . . . . . . . . . . . . 14
โข (๐ โ (3 ยท ๐) โ
โ) |
105 | 104 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (3 ยท ๐)
โ โ) |
106 | 98 | nnred 12223 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐โ๐) โ
โ) |
107 | | ltdivmul 12085 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท ๐) โ โ
โง ๐ โ โ
โง (3 โ โ โง 0 < 3)) โ (((2 ยท ๐) / 3) < ๐ โ (2 ยท ๐) < (3 ยท ๐))) |
108 | 49, 107 | mp3an3 1450 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท ๐) โ โ
โง ๐ โ โ)
โ (((2 ยท ๐) /
3) < ๐ โ (2
ยท ๐) < (3
ยท ๐))) |
109 | 46, 22, 108 | syl2anc 584 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท ๐) / 3) < ๐ โ (2 ยท ๐) < (3 ยท ๐))) |
110 | 42, 109 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 ยท ๐) < (3 ยท ๐)) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท ๐) <
(3 ยท ๐)) |
112 | 22, 22 | remulcld 11240 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ ยท ๐) โ โ) |
113 | 112 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐ ยท ๐) โ
โ) |
114 | | bposlem2.3 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 < ๐) |
115 | | nnltp1le 12614 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐
โ โ) โ (2 < ๐ โ (2 + 1) โค ๐)) |
116 | 43, 10, 115 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2 < ๐ โ (2 + 1) โค ๐)) |
117 | 114, 116 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 + 1) โค ๐) |
118 | 54, 117 | eqbrtrid 5182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 3 โค ๐) |
119 | | lemul1 12062 |
. . . . . . . . . . . . . . . . . 18
โข ((3
โ โ โง ๐
โ โ โง (๐
โ โ โง 0 < ๐)) โ (3 โค ๐ โ (3 ยท ๐) โค (๐ ยท ๐))) |
120 | 47, 119 | mp3an1 1448 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ (3 โค ๐ โ (3 ยท ๐) โค (๐ ยท ๐))) |
121 | 22, 22, 23, 120 | syl12anc 835 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (3 โค ๐ โ (3 ยท ๐) โค (๐ ยท ๐))) |
122 | 118, 121 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (๐ โ (3 ยท ๐) โค (๐ ยท ๐)) |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (3 ยท ๐) โค
(๐ ยท ๐)) |
124 | 11 | sqvald 14104 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐โ2) = (๐ ยท ๐)) |
126 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ โ
โ) |
127 | 10 | nnge1d 12256 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โค ๐) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ2))
โ 1 โค ๐) |
129 | | simpr 485 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ โ
(โคโฅโ2)) |
130 | 126, 128,
129 | leexp2ad 14213 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐โ2) โค
(๐โ๐)) |
131 | 125, 130 | eqbrtrrd 5171 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐ ยท ๐) โค (๐โ๐)) |
132 | 105, 113,
106, 123, 131 | letrd 11367 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (3 ยท ๐) โค
(๐โ๐)) |
133 | 102, 105,
106, 111, 132 | ltletrd 11370 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท ๐) <
(๐โ๐)) |
134 | 98 | nncnd 12224 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐โ๐) โ
โ) |
135 | 134 | mulridd 11227 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((๐โ๐) ยท 1) = (๐โ๐)) |
136 | 133, 135 | breqtrrd 5175 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท ๐) <
((๐โ๐) ยท 1)) |
137 | | 1red 11211 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ 1 โ โ) |
138 | 102, 137,
99 | ltdivmuld 13063 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (((2 ยท ๐) /
(๐โ๐)) < 1 โ (2 ยท ๐) < ((๐โ๐) ยท 1))) |
139 | 136, 138 | mpbird 256 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((2 ยท ๐) /
(๐โ๐)) < 1) |
140 | | 1e0p1 12715 |
. . . . . . . . . 10
โข 1 = (0 +
1) |
141 | 139, 140 | breqtrdi 5188 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((2 ยท ๐) /
(๐โ๐)) < (0 + 1)) |
142 | 100 | rpred 13012 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((2 ยท ๐) /
(๐โ๐)) โ โ) |
143 | | 0z 12565 |
. . . . . . . . . 10
โข 0 โ
โค |
144 | | flbi 13777 |
. . . . . . . . . 10
โข ((((2
ยท ๐) / (๐โ๐)) โ โ โง 0 โ โค)
โ ((โโ((2 ยท ๐) / (๐โ๐))) = 0 โ (0 โค ((2 ยท ๐) / (๐โ๐)) โง ((2 ยท ๐) / (๐โ๐)) < (0 + 1)))) |
145 | 142, 143,
144 | sylancl 586 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((โโ((2 ยท ๐) / (๐โ๐))) = 0 โ (0 โค ((2 ยท ๐) / (๐โ๐)) โง ((2 ยท ๐) / (๐โ๐)) < (0 + 1)))) |
146 | 101, 141,
145 | mpbir2and 711 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (โโ((2 ยท ๐) / (๐โ๐))) = 0) |
147 | 1 | nnrpd 13010 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ
โ+) |
148 | 147 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ โ
โ+) |
149 | 148, 99 | rpdivcld 13029 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐ / (๐โ๐)) โ
โ+) |
150 | 149 | rpge0d 13016 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ 0 โค (๐ / (๐โ๐))) |
151 | 21 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ โ
โ) |
152 | 21, 147 | ltaddrpd 13045 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ < (๐ + ๐)) |
153 | 38 | 2timesd 12451 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท ๐) = (๐ + ๐)) |
154 | 152, 153 | breqtrrd 5175 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ < (2 ยท ๐)) |
155 | 154 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ < (2 ยท
๐)) |
156 | 151, 102,
106, 155, 133 | lttrd 11371 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ < (๐โ๐)) |
157 | 156, 135 | breqtrrd 5175 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ๐ < ((๐โ๐) ยท 1)) |
158 | 151, 137,
99 | ltdivmuld 13063 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((๐ / (๐โ๐)) < 1 โ ๐ < ((๐โ๐) ยท 1))) |
159 | 157, 158 | mpbird 256 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐ / (๐โ๐)) < 1) |
160 | 159, 140 | breqtrdi 5188 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐ / (๐โ๐)) < (0 + 1)) |
161 | 149 | rpred 13012 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (๐ / (๐โ๐)) โ โ) |
162 | | flbi 13777 |
. . . . . . . . . . . 12
โข (((๐ / (๐โ๐)) โ โ โง 0 โ โค)
โ ((โโ(๐ /
(๐โ๐))) = 0 โ (0 โค (๐ / (๐โ๐)) โง (๐ / (๐โ๐)) < (0 + 1)))) |
163 | 161, 143,
162 | sylancl 586 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((โโ(๐ /
(๐โ๐))) = 0 โ (0 โค (๐ / (๐โ๐)) โง (๐ / (๐โ๐)) < (0 + 1)))) |
164 | 150, 160,
163 | mpbir2and 711 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (โโ(๐ /
(๐โ๐))) = 0) |
165 | 164 | oveq2d 7421 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท (โโ(๐ / (๐โ๐)))) = (2 ยท 0)) |
166 | | 2t0e0 12377 |
. . . . . . . . 9
โข (2
ยท 0) = 0 |
167 | 165, 166 | eqtrdi 2788 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (2 ยท (โโ(๐ / (๐โ๐)))) = 0) |
168 | 146, 167 | oveq12d 7423 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = (0 โ 0)) |
169 | | 0m0e0 12328 |
. . . . . . 7
โข (0
โ 0) = 0 |
170 | 168, 169 | eqtrdi 2788 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = 0) |
171 | 93, 170 | jaodan 956 |
. . . . 5
โข ((๐ โง (๐ = 1 โจ ๐ โ (โคโฅโ2)))
โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = 0) |
172 | 7, 171 | sylan2 593 |
. . . 4
โข ((๐ โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = 0) |
173 | 172 | sumeq2dv 15645 |
. . 3
โข (๐ โ ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = ฮฃ๐ โ (1...(2 ยท ๐))0) |
174 | | fzfid 13934 |
. . . 4
โข (๐ โ (1...(2 ยท ๐)) โ Fin) |
175 | | sumz 15664 |
. . . . 5
โข (((1...(2
ยท ๐)) โ
(โคโฅโ1) โจ (1...(2 ยท ๐)) โ Fin) โ ฮฃ๐ โ (1...(2 ยท ๐))0 = 0) |
176 | 175 | olcs 874 |
. . . 4
โข ((1...(2
ยท ๐)) โ Fin
โ ฮฃ๐ โ
(1...(2 ยท ๐))0 =
0) |
177 | 174, 176 | syl 17 |
. . 3
โข (๐ โ ฮฃ๐ โ (1...(2 ยท ๐))0 = 0) |
178 | 173, 177 | eqtrd 2772 |
. 2
โข (๐ โ ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = 0) |
179 | 4, 178 | eqtrd 2772 |
1
โข (๐ โ (๐ pCnt ((2 ยท ๐)C๐)) = 0) |