Step | Hyp | Ref
| Expression |
1 | | prmrec.3 |
. . . 4
โข (๐ โ ๐ โ โ) |
2 | 1 | nnred 12175 |
. . 3
โข (๐ โ ๐ โ โ) |
3 | 2 | rehalfcld 12407 |
. 2
โข (๐ โ (๐ / 2) โ โ) |
4 | | fzfi 13884 |
. . . . . 6
โข
(1...๐) โ
Fin |
5 | | prmrec.4 |
. . . . . . 7
โข ๐ = {๐ โ (1...๐) โฃ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐} |
6 | 5 | ssrab3 4045 |
. . . . . 6
โข ๐ โ (1...๐) |
7 | | ssfi 9124 |
. . . . . 6
โข
(((1...๐) โ Fin
โง ๐ โ (1...๐)) โ ๐ โ Fin) |
8 | 4, 6, 7 | mp2an 691 |
. . . . 5
โข ๐ โ Fin |
9 | | hashcl 14263 |
. . . . 5
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
10 | 8, 9 | ax-mp 5 |
. . . 4
โข
(โฏโ๐)
โ โ0 |
11 | 10 | nn0rei 12431 |
. . 3
โข
(โฏโ๐)
โ โ |
12 | 11 | a1i 11 |
. 2
โข (๐ โ (โฏโ๐) โ
โ) |
13 | | 2nn 12233 |
. . . . 5
โข 2 โ
โ |
14 | | prmrec.2 |
. . . . . 6
โข (๐ โ ๐พ โ โ) |
15 | 14 | nnnn0d 12480 |
. . . . 5
โข (๐ โ ๐พ โ
โ0) |
16 | | nnexpcl 13987 |
. . . . 5
โข ((2
โ โ โง ๐พ
โ โ0) โ (2โ๐พ) โ โ) |
17 | 13, 15, 16 | sylancr 588 |
. . . 4
โข (๐ โ (2โ๐พ) โ โ) |
18 | 17 | nnred 12175 |
. . 3
โข (๐ โ (2โ๐พ) โ โ) |
19 | 1 | nnrpd 12962 |
. . . . 5
โข (๐ โ ๐ โ
โ+) |
20 | 19 | rpsqrtcld 15303 |
. . . 4
โข (๐ โ (โโ๐) โ
โ+) |
21 | 20 | rpred 12964 |
. . 3
โข (๐ โ (โโ๐) โ
โ) |
22 | 18, 21 | remulcld 11192 |
. 2
โข (๐ โ ((2โ๐พ) ยท (โโ๐)) โ โ) |
23 | 2 | recnd 11190 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
24 | 23 | 2halvesd 12406 |
. . . . 5
โข (๐ โ ((๐ / 2) + (๐ / 2)) = ๐) |
25 | 6 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐ โ (1...๐)) |
26 | 14 | peano2nnd 12177 |
. . . . . . . . . . . . 13
โข (๐ โ (๐พ + 1) โ โ) |
27 | | elfzuz 13444 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐พ + 1)...๐) โ ๐ โ (โคโฅโ(๐พ + 1))) |
28 | | eluznn 12850 |
. . . . . . . . . . . . 13
โข (((๐พ + 1) โ โ โง ๐ โ
(โคโฅโ(๐พ + 1))) โ ๐ โ โ) |
29 | 26, 27, 28 | syl2an 597 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐พ + 1)...๐)) โ ๐ โ โ) |
30 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
31 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ โฅ ๐ โ ๐ โฅ ๐)) |
32 | 30, 31 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โ โ โง ๐ โฅ ๐))) |
33 | 32 | rabbidv 3418 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
34 | | prmrec.7 |
. . . . . . . . . . . . . . 15
โข ๐ = (๐ โ โ โฆ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
35 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
โข
(1...๐) โ
V |
36 | 35 | rabex 5294 |
. . . . . . . . . . . . . . 15
โข {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ V |
37 | 33, 34, 36 | fvmpt 6953 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
39 | | ssrab2 4042 |
. . . . . . . . . . . . 13
โข {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ (1...๐) |
40 | 38, 39 | eqsstrdi 4003 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (๐โ๐) โ (1...๐)) |
41 | 29, 40 | syldan 592 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐พ + 1)...๐)) โ (๐โ๐) โ (1...๐)) |
42 | 41 | ralrimiva 3144 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
43 | | iunss 5010 |
. . . . . . . . . 10
โข (โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐) โ โ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
44 | 42, 43 | sylibr 233 |
. . . . . . . . 9
โข (๐ โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
45 | 25, 44 | unssd 4151 |
. . . . . . . 8
โข (๐ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ (1...๐)) |
46 | | breq1 5113 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐ โฅ ๐ โ ๐ โฅ ๐)) |
47 | 46 | notbid 318 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (ยฌ ๐ โฅ ๐ โ ยฌ ๐ โฅ ๐)) |
48 | 47 | cbvralvw 3228 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
(โ โ (1...๐พ))
ยฌ ๐ โฅ ๐ โ โ๐ โ (โ โ
(1...๐พ)) ยฌ ๐ โฅ ๐) |
49 | | breq2 5114 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ฅ โ (๐ โฅ ๐ โ ๐ โฅ ๐ฅ)) |
50 | 49 | notbid 318 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (ยฌ ๐ โฅ ๐ โ ยฌ ๐ โฅ ๐ฅ)) |
51 | 50 | ralbidv 3175 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ (โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ โ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ)) |
52 | 48, 51 | bitrid 283 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ โ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ)) |
53 | 52, 5 | elrab2 3653 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ โ (๐ฅ โ (1...๐) โง โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ)) |
54 | | elun1 4141 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
55 | 53, 54 | sylbir 234 |
. . . . . . . . . . 11
โข ((๐ฅ โ (1...๐) โง โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ) โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
56 | 55 | ex 414 |
. . . . . . . . . 10
โข (๐ฅ โ (1...๐) โ (โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
57 | 56 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...๐)) โ (โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
58 | | dfrex2 3077 |
. . . . . . . . . 10
โข
(โ๐ โ
(โ โ (1...๐พ))๐ โฅ ๐ฅ โ ยฌ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ) |
59 | 14 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐พ โ โค) |
60 | 59 | peano2zd 12617 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐พ + 1) โ โค) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐พ + 1) โ โค) |
62 | 1 | nnzd 12533 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โค) |
63 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ โค) |
64 | | eldifi 4091 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โ โ
(1...๐พ)) โ ๐ โ
โ) |
65 | 64 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ โ) |
66 | | prmz 16558 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โค) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ โค) |
68 | | eldifn 4092 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ โ
(1...๐พ)) โ ยฌ ๐ โ (1...๐พ)) |
69 | 68 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ยฌ ๐ โ (1...๐พ)) |
70 | | prmnn 16557 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
71 | 65, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ โ) |
72 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . 19
โข โ =
(โคโฅโ1) |
73 | 71, 72 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ
(โคโฅโ1)) |
74 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐พ โ โค) |
75 | | elfz5 13440 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ
(โคโฅโ1) โง ๐พ โ โค) โ (๐ โ (1...๐พ) โ ๐ โค ๐พ)) |
76 | 73, 74, 75 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐ โ (1...๐พ) โ ๐ โค ๐พ)) |
77 | 69, 76 | mtbid 324 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ยฌ ๐ โค ๐พ) |
78 | 14 | nnred 12175 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐พ โ โ) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐พ โ โ) |
80 | 71 | nnred 12175 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ โ) |
81 | 79, 80 | ltnled 11309 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐พ < ๐ โ ยฌ ๐ โค ๐พ)) |
82 | 77, 81 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐พ < ๐) |
83 | | zltp1le 12560 |
. . . . . . . . . . . . . . . 16
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ < ๐ โ (๐พ + 1) โค ๐)) |
84 | 74, 67, 83 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐พ < ๐ โ (๐พ + 1) โค ๐)) |
85 | 82, 84 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐พ + 1) โค ๐) |
86 | | elfznn 13477 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (1...๐) โ ๐ฅ โ โ) |
87 | 86 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ โ) |
88 | 87 | nnred 12175 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ โ) |
89 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ โ) |
90 | | simprr 772 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โฅ ๐ฅ) |
91 | | dvdsle 16199 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ฅ โ โ) โ (๐ โฅ ๐ฅ โ ๐ โค ๐ฅ)) |
92 | 67, 87, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐ โฅ ๐ฅ โ ๐ โค ๐ฅ)) |
93 | 90, 92 | mpd 15 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โค ๐ฅ) |
94 | | elfzle2 13452 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (1...๐) โ ๐ฅ โค ๐) |
95 | 94 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โค ๐) |
96 | 80, 88, 89, 93, 95 | letrd 11319 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โค ๐) |
97 | 61, 63, 67, 85, 96 | elfzd 13439 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ โ ((๐พ + 1)...๐)) |
98 | 49 | anbi2d 630 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โ โ โง ๐ โฅ ๐ฅ))) |
99 | | simplr 768 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ (1...๐)) |
100 | 65, 90 | jca 513 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐ โ โ โง ๐ โฅ ๐ฅ)) |
101 | 98, 99, 100 | elrabd 3652 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
102 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
103 | 102, 46 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โ โ โง ๐ โฅ ๐))) |
104 | 103 | rabbidv 3418 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
105 | 35 | rabex 5294 |
. . . . . . . . . . . . . . . 16
โข {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ V |
106 | 104, 34, 105 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
107 | 71, 106 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
108 | 101, 107 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ (๐โ๐)) |
109 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
110 | 109 | eliuni 4965 |
. . . . . . . . . . . . 13
โข ((๐ โ ((๐พ + 1)...๐) โง ๐ฅ โ (๐โ๐)) โ ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) |
111 | 97, 108, 110 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) |
112 | | elun2 4142 |
. . . . . . . . . . . 12
โข (๐ฅ โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1...๐)) โง (๐ โ (โ โ (1...๐พ)) โง ๐ โฅ ๐ฅ)) โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
114 | 113 | rexlimdvaa 3154 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...๐)) โ (โ๐ โ (โ โ (1...๐พ))๐ โฅ ๐ฅ โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
115 | 58, 114 | biimtrrid 242 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...๐)) โ (ยฌ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
116 | 57, 115 | pm2.61d 179 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...๐)) โ ๐ฅ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
117 | 45, 116 | eqelssd 3970 |
. . . . . . 7
โข (๐ โ (๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) = (1...๐)) |
118 | 117 | fveq2d 6851 |
. . . . . 6
โข (๐ โ (โฏโ(๐ โช โช ๐ โ ((๐พ + 1)...๐)(๐โ๐))) = (โฏโ(1...๐))) |
119 | 1 | nnnn0d 12480 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
120 | | hashfz1 14253 |
. . . . . . 7
โข (๐ โ โ0
โ (โฏโ(1...๐)) = ๐) |
121 | 119, 120 | syl 17 |
. . . . . 6
โข (๐ โ (โฏโ(1...๐)) = ๐) |
122 | 118, 121 | eqtr2d 2778 |
. . . . 5
โข (๐ โ ๐ = (โฏโ(๐ โช โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
123 | 8 | a1i 11 |
. . . . . 6
โข (๐ โ ๐ โ Fin) |
124 | | ssfi 9124 |
. . . . . . 7
โข
(((1...๐) โ Fin
โง โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin) |
125 | 4, 44, 124 | sylancr 588 |
. . . . . 6
โข (๐ โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin) |
126 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐ฅ)) |
127 | 126 | notbid 318 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (ยฌ ๐ โฅ ๐ฅ โ ยฌ ๐ โฅ ๐ฅ)) |
128 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ฅ โ (๐ โฅ ๐ โ ๐ โฅ ๐ฅ)) |
129 | 128 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ฅ โ (ยฌ ๐ โฅ ๐ โ ยฌ ๐ โฅ ๐ฅ)) |
130 | 129 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ฅ โ (โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ โ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ)) |
131 | 130, 5 | elrab2 3653 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ ๐ โ (๐ฅ โ (1...๐) โง โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ)) |
132 | 131 | simprbi 498 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ ๐ โ โ๐ โ (โ โ (1...๐พ)) ยฌ ๐ โฅ ๐ฅ) |
133 | 132 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ โ๐ โ (โ โ
(1...๐พ)) ยฌ ๐ โฅ ๐ฅ) |
134 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ ๐ โ โ) |
135 | | noel 4295 |
. . . . . . . . . . . . . . . . . 18
โข ยฌ
๐ โ
โ
|
136 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ ๐ โ ((๐พ + 1)...๐)) |
137 | 136 | biantrud 533 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ (๐ โ (1...๐พ) โ (๐ โ (1...๐พ) โง ๐ โ ((๐พ + 1)...๐)))) |
138 | | elin 3931 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((1...๐พ) โฉ ((๐พ + 1)...๐)) โ (๐ โ (1...๐พ) โง ๐ โ ((๐พ + 1)...๐))) |
139 | 137, 138 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ (๐ โ (1...๐พ) โ ๐ โ ((1...๐พ) โฉ ((๐พ + 1)...๐)))) |
140 | 78 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐พ < (๐พ + 1)) |
141 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐พ < (๐พ + 1) โ ((1...๐พ) โฉ ((๐พ + 1)...๐)) = โ
) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((1...๐พ) โฉ ((๐พ + 1)...๐)) = โ
) |
143 | 142 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ ((1...๐พ) โฉ ((๐พ + 1)...๐)) = โ
) |
144 | 143 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ (๐ โ ((1...๐พ) โฉ ((๐พ + 1)...๐)) โ ๐ โ โ
)) |
145 | 139, 144 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ (๐ โ (1...๐พ) โ ๐ โ โ
)) |
146 | 135, 145 | mtbiri 327 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ ยฌ ๐ โ (1...๐พ)) |
147 | 134, 146 | eldifd 3926 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ ๐ โ (โ โ (1...๐พ))) |
148 | 127, 133,
147 | rspcdva 3585 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ ๐) โง (๐ โ ((๐พ + 1)...๐) โง ๐ โ โ)) โ ยฌ ๐ โฅ ๐ฅ) |
149 | 148 | expr 458 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ (๐ โ โ โ ยฌ ๐ โฅ ๐ฅ)) |
150 | | imnan 401 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โ ยฌ
๐ โฅ ๐ฅ) โ ยฌ (๐ โ โ โง ๐ โฅ ๐ฅ)) |
151 | 149, 150 | sylib 217 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ ยฌ (๐ โ โ โง ๐ โฅ ๐ฅ)) |
152 | 29 | adantlr 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ ๐ โ โ) |
153 | 152, 37 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
154 | 153 | eleq2d 2824 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ (๐ฅ โ (๐โ๐) โ ๐ฅ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)})) |
155 | | breq2 5114 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ฅ โ (๐ โฅ ๐ โ ๐ โฅ ๐ฅ)) |
156 | 155 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ฅ โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โ โ โง ๐ โฅ ๐ฅ))) |
157 | 156 | elrab 3650 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ (๐ฅ โ (1...๐) โง (๐ โ โ โง ๐ โฅ ๐ฅ))) |
158 | 157 | simprbi 498 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ (๐ โ โ โง ๐ โฅ ๐ฅ)) |
159 | 154, 158 | syl6bi 253 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ (๐ฅ โ (๐โ๐) โ (๐ โ โ โง ๐ โฅ ๐ฅ))) |
160 | 151, 159 | mtod 197 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ ๐) โง ๐ โ ((๐พ + 1)...๐)) โ ยฌ ๐ฅ โ (๐โ๐)) |
161 | 160 | nrexdv 3147 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐) โ ยฌ โ๐ โ ((๐พ + 1)...๐)๐ฅ โ (๐โ๐)) |
162 | | eliun 4963 |
. . . . . . . . . . 11
โข (๐ฅ โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ โ๐ โ ((๐พ + 1)...๐)๐ฅ โ (๐โ๐)) |
163 | 161, 162 | sylnibr 329 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐) โ ยฌ ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) |
164 | 163 | ex 414 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ โ ยฌ ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
165 | | imnan 401 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ โ ยฌ ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ ยฌ (๐ฅ โ ๐ โง ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
166 | 164, 165 | sylib 217 |
. . . . . . . 8
โข (๐ โ ยฌ (๐ฅ โ ๐ โง ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
167 | | elin 3931 |
. . . . . . . 8
โข (๐ฅ โ (๐ โฉ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ (๐ฅ โ ๐ โง ๐ฅ โ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
168 | 166, 167 | sylnibr 329 |
. . . . . . 7
โข (๐ โ ยฌ ๐ฅ โ (๐ โฉ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
169 | 168 | eq0rdv 4369 |
. . . . . 6
โข (๐ โ (๐ โฉ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) = โ
) |
170 | | hashun 14289 |
. . . . . 6
โข ((๐ โ Fin โง โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin โง (๐ โฉ โช
๐ โ ((๐พ + 1)...๐)(๐โ๐)) = โ
) โ (โฏโ(๐ โช โช ๐ โ ((๐พ + 1)...๐)(๐โ๐))) = ((โฏโ๐) + (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
171 | 123, 125,
169, 170 | syl3anc 1372 |
. . . . 5
โข (๐ โ (โฏโ(๐ โช โช ๐ โ ((๐พ + 1)...๐)(๐โ๐))) = ((โฏโ๐) + (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
172 | 24, 122, 171 | 3eqtrd 2781 |
. . . 4
โข (๐ โ ((๐ / 2) + (๐ / 2)) = ((โฏโ๐) + (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)))) |
173 | | hashcl 14263 |
. . . . . . 7
โข (โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ
โ0) |
174 | 125, 173 | syl 17 |
. . . . . 6
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ
โ0) |
175 | 174 | nn0red 12481 |
. . . . 5
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ โ) |
176 | | fzfid 13885 |
. . . . . . . 8
โข (๐ โ ((๐พ + 1)...๐) โ Fin) |
177 | 26, 28 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ ๐ โ
โ) |
178 | | nnrecre 12202 |
. . . . . . . . . . 11
โข (๐ โ โ โ (1 /
๐) โ
โ) |
179 | | 0re 11164 |
. . . . . . . . . . 11
โข 0 โ
โ |
180 | | ifcl 4536 |
. . . . . . . . . . 11
โข (((1 /
๐) โ โ โง 0
โ โ) โ if(๐
โ โ, (1 / ๐), 0)
โ โ) |
181 | 178, 179,
180 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ โ โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
182 | 177, 181 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
183 | 27, 182 | sylan2 594 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((๐พ + 1)...๐)) โ if(๐ โ โ, (1 / ๐), 0) โ โ) |
184 | 176, 183 | fsumrecl 15626 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) โ โ) |
185 | 2, 184 | remulcld 11192 |
. . . . . 6
โข (๐ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ โ) |
186 | | prmrec.1 |
. . . . . . . 8
โข ๐น = (๐ โ โ โฆ if(๐ โ โ, (1 / ๐), 0)) |
187 | | prmrec.5 |
. . . . . . . 8
โข (๐ โ seq1( + , ๐น) โ dom โ
) |
188 | | prmrec.6 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐พ + 1))if(๐ โ โ, (1 / ๐), 0) < (1 / 2)) |
189 | 186, 14, 1, 5, 187, 188, 34 | prmreclem4 16798 |
. . . . . . 7
โข (๐ โ (๐ โ (โคโฅโ๐พ) โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |
190 | | eluz 12784 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐พ โ โค) โ (๐พ โ
(โคโฅโ๐) โ ๐ โค ๐พ)) |
191 | 62, 59, 190 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐พ โ (โคโฅโ๐) โ ๐ โค ๐พ)) |
192 | | nnleltp1 12565 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐พ โ โ) โ (๐ โค ๐พ โ ๐ < (๐พ + 1))) |
193 | 1, 14, 192 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ โค ๐พ โ ๐ < (๐พ + 1))) |
194 | | fzn 13464 |
. . . . . . . . . 10
โข (((๐พ + 1) โ โค โง ๐ โ โค) โ (๐ < (๐พ + 1) โ ((๐พ + 1)...๐) = โ
)) |
195 | 60, 62, 194 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ < (๐พ + 1) โ ((๐พ + 1)...๐) = โ
)) |
196 | 191, 193,
195 | 3bitrd 305 |
. . . . . . . 8
โข (๐ โ (๐พ โ (โคโฅโ๐) โ ((๐พ + 1)...๐) = โ
)) |
197 | | 0le0 12261 |
. . . . . . . . . 10
โข 0 โค
0 |
198 | 23 | mul01d 11361 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท 0) = 0) |
199 | 197, 198 | breqtrrid 5148 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ ยท 0)) |
200 | | iuneq1 4975 |
. . . . . . . . . . . . 13
โข (((๐พ + 1)...๐) = โ
โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) = โช ๐ โ โ
(๐โ๐)) |
201 | | 0iun 5028 |
. . . . . . . . . . . . 13
โข โช ๐ โ โ
(๐โ๐) = โ
|
202 | 200, 201 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (((๐พ + 1)...๐) = โ
โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) = โ
) |
203 | 202 | fveq2d 6851 |
. . . . . . . . . . 11
โข (((๐พ + 1)...๐) = โ
โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) =
(โฏโโ
)) |
204 | | hash0 14274 |
. . . . . . . . . . 11
โข
(โฏโโ
) = 0 |
205 | 203, 204 | eqtrdi 2793 |
. . . . . . . . . 10
โข (((๐พ + 1)...๐) = โ
โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) = 0) |
206 | | sumeq1 15580 |
. . . . . . . . . . . 12
โข (((๐พ + 1)...๐) = โ
โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ โ
if(๐ โ โ, (1 / ๐), 0)) |
207 | | sum0 15613 |
. . . . . . . . . . . 12
โข
ฮฃ๐ โ
โ
if(๐ โ
โ, (1 / ๐), 0) =
0 |
208 | 206, 207 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (((๐พ + 1)...๐) = โ
โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) = 0) |
209 | 208 | oveq2d 7378 |
. . . . . . . . . 10
โข (((๐พ + 1)...๐) = โ
โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท 0)) |
210 | 205, 209 | breq12d 5123 |
. . . . . . . . 9
โข (((๐พ + 1)...๐) = โ
โ ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ 0 โค (๐ ยท 0))) |
211 | 199, 210 | syl5ibrcom 247 |
. . . . . . . 8
โข (๐ โ (((๐พ + 1)...๐) = โ
โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |
212 | 196, 211 | sylbid 239 |
. . . . . . 7
โข (๐ โ (๐พ โ (โคโฅโ๐) โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |
213 | | uztric 12794 |
. . . . . . . 8
โข ((๐พ โ โค โง ๐ โ โค) โ (๐ โ
(โคโฅโ๐พ) โจ ๐พ โ (โคโฅโ๐))) |
214 | 59, 62, 213 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ โ (โคโฅโ๐พ) โจ ๐พ โ (โคโฅโ๐))) |
215 | 189, 212,
214 | mpjaod 859 |
. . . . . 6
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0))) |
216 | | eqid 2737 |
. . . . . . . . . 10
โข
(โคโฅโ(๐พ + 1)) =
(โคโฅโ(๐พ + 1)) |
217 | | eleq1w 2821 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
218 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (1 / ๐) = (1 / ๐)) |
219 | 217, 218 | ifbieq1d 4515 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ if(๐ โ โ, (1 / ๐), 0) = if(๐ โ โ, (1 / ๐), 0)) |
220 | | ovex 7395 |
. . . . . . . . . . . . 13
โข (1 /
๐) โ
V |
221 | | c0ex 11156 |
. . . . . . . . . . . . 13
โข 0 โ
V |
222 | 220, 221 | ifex 4541 |
. . . . . . . . . . . 12
โข if(๐ โ โ, (1 / ๐), 0) โ V |
223 | 219, 186,
222 | fvmpt 6953 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐นโ๐) = if(๐ โ โ, (1 / ๐), 0)) |
224 | 177, 223 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ (๐นโ๐) = if(๐ โ โ, (1 / ๐), 0)) |
225 | 181 | recnd 11190 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
226 | 223, 225 | eqeltrd 2838 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐นโ๐) โ โ) |
227 | 226 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
228 | 72, 26, 227 | iserex 15548 |
. . . . . . . . . . 11
โข (๐ โ (seq1( + , ๐น) โ dom โ โ
seq(๐พ + 1)( + , ๐น) โ dom โ
)) |
229 | 187, 228 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ seq(๐พ + 1)( + , ๐น) โ dom โ ) |
230 | 216, 60, 224, 182, 229 | isumrecl 15657 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐พ + 1))if(๐ โ โ, (1 / ๐), 0) โ โ) |
231 | | halfre 12374 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
232 | 231 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (1 / 2) โ
โ) |
233 | | fzssuz 13489 |
. . . . . . . . . . 11
โข ((๐พ + 1)...๐) โ
(โคโฅโ(๐พ + 1)) |
234 | 233 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ ((๐พ + 1)...๐) โ
(โคโฅโ(๐พ + 1))) |
235 | | nnrp 12933 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ+) |
236 | 235 | rpreccld 12974 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (1 /
๐) โ
โ+) |
237 | 236 | rpge0d 12968 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 โค (1
/ ๐)) |
238 | | breq2 5114 |
. . . . . . . . . . . . 13
โข ((1 /
๐) = if(๐ โ โ, (1 / ๐), 0) โ (0 โค (1 / ๐) โ 0 โค if(๐ โ โ, (1 / ๐), 0))) |
239 | | breq2 5114 |
. . . . . . . . . . . . 13
โข (0 =
if(๐ โ โ, (1 /
๐), 0) โ (0 โค 0
โ 0 โค if(๐ โ
โ, (1 / ๐),
0))) |
240 | 238, 239 | ifboth 4530 |
. . . . . . . . . . . 12
โข ((0 โค
(1 / ๐) โง 0 โค 0)
โ 0 โค if(๐ โ
โ, (1 / ๐),
0)) |
241 | 237, 197,
240 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 โค
if(๐ โ โ, (1 /
๐), 0)) |
242 | 177, 241 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ 0 โค if(๐ โ โ, (1 / ๐), 0)) |
243 | 216, 60, 176, 234, 224, 182, 242, 229 | isumless 15737 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) โค ฮฃ๐ โ (โคโฅโ(๐พ + 1))if(๐ โ โ, (1 / ๐), 0)) |
244 | 184, 230,
232, 243, 188 | lelttrd 11320 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) < (1 / 2)) |
245 | 1 | nngt0d 12209 |
. . . . . . . . 9
โข (๐ โ 0 < ๐) |
246 | | ltmul2 12013 |
. . . . . . . . 9
โข
((ฮฃ๐ โ
((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) โ โ โง (1 / 2) โ
โ โง (๐ โ
โ โง 0 < ๐))
โ (ฮฃ๐ โ
((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) < (1 / 2) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) < (๐ ยท (1 / 2)))) |
247 | 184, 232,
2, 245, 246 | syl112anc 1375 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) < (1 / 2) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) < (๐ ยท (1 / 2)))) |
248 | 244, 247 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) < (๐ ยท (1 / 2))) |
249 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
250 | | 2ne0 12264 |
. . . . . . . . 9
โข 2 โ
0 |
251 | | divrec 11836 |
. . . . . . . . 9
โข ((๐ โ โ โง 2 โ
โ โง 2 โ 0) โ (๐ / 2) = (๐ ยท (1 / 2))) |
252 | 249, 250,
251 | mp3an23 1454 |
. . . . . . . 8
โข (๐ โ โ โ (๐ / 2) = (๐ ยท (1 / 2))) |
253 | 23, 252 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ / 2) = (๐ ยท (1 / 2))) |
254 | 248, 253 | breqtrrd 5138 |
. . . . . 6
โข (๐ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) < (๐ / 2)) |
255 | 175, 185,
3, 215, 254 | lelttrd 11320 |
. . . . 5
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) < (๐ / 2)) |
256 | 175, 3, 12, 255 | ltadd2dd 11321 |
. . . 4
โข (๐ โ ((โฏโ๐) + (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐))) < ((โฏโ๐) + (๐ / 2))) |
257 | 172, 256 | eqbrtrd 5132 |
. . 3
โข (๐ โ ((๐ / 2) + (๐ / 2)) < ((โฏโ๐) + (๐ / 2))) |
258 | 3, 12, 3 | ltadd1d 11755 |
. . 3
โข (๐ โ ((๐ / 2) < (โฏโ๐) โ ((๐ / 2) + (๐ / 2)) < ((โฏโ๐) + (๐ / 2)))) |
259 | 257, 258 | mpbird 257 |
. 2
โข (๐ โ (๐ / 2) < (โฏโ๐)) |
260 | | oveq1 7369 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
261 | 260 | breq1d 5120 |
. . . . . . 7
โข (๐ = ๐ โ ((๐โ2) โฅ ๐ฅ โ (๐โ2) โฅ ๐ฅ)) |
262 | 261 | cbvrabv 3420 |
. . . . . 6
โข {๐ โ โ โฃ (๐โ2) โฅ ๐ฅ} = {๐ โ โ โฃ (๐โ2) โฅ ๐ฅ} |
263 | | breq2 5114 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐โ2) โฅ ๐ฅ โ (๐โ2) โฅ ๐)) |
264 | 263 | rabbidv 3418 |
. . . . . 6
โข (๐ฅ = ๐ โ {๐ โ โ โฃ (๐โ2) โฅ ๐ฅ} = {๐ โ โ โฃ (๐โ2) โฅ ๐}) |
265 | 262, 264 | eqtrid 2789 |
. . . . 5
โข (๐ฅ = ๐ โ {๐ โ โ โฃ (๐โ2) โฅ ๐ฅ} = {๐ โ โ โฃ (๐โ2) โฅ ๐}) |
266 | 265 | supeq1d 9389 |
. . . 4
โข (๐ฅ = ๐ โ sup({๐ โ โ โฃ (๐โ2) โฅ ๐ฅ}, โ, < ) = sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < )) |
267 | 266 | cbvmptv 5223 |
. . 3
โข (๐ฅ โ โ โฆ
sup({๐ โ โ
โฃ (๐โ2) โฅ
๐ฅ}, โ, < )) =
(๐ โ โ โฆ
sup({๐ โ โ
โฃ (๐โ2) โฅ
๐}, โ, <
)) |
268 | 186, 14, 1, 5, 267 | prmreclem3 16797 |
. 2
โข (๐ โ (โฏโ๐) โค ((2โ๐พ) ยท (โโ๐))) |
269 | 3, 12, 22, 259, 268 | ltletrd 11322 |
1
โข (๐ โ (๐ / 2) < ((2โ๐พ) ยท (โโ๐))) |