Step | Hyp | Ref
| Expression |
1 | | nnuz 12814 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
2 | | 1zzd 12542 |
. . . . . . . . 9
β’ (β€
β 1 β β€) |
3 | | nnrecre 12203 |
. . . . . . . . . . . . 13
β’ (π β β β (1 /
π) β
β) |
4 | 3 | adantl 483 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β (1 / π) β β) |
5 | | 0re 11165 |
. . . . . . . . . . . 12
β’ 0 β
β |
6 | | ifcl 4535 |
. . . . . . . . . . . 12
β’ (((1 /
π) β β β§ 0
β β) β if(π
β β, (1 / π), 0)
β β) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . . . . 11
β’
((β€ β§ π
β β) β if(π
β β, (1 / π), 0)
β β) |
8 | | prmrec.1 |
. . . . . . . . . . 11
β’ πΉ = (π β β β¦ if(π β β, (1 / π), 0)) |
9 | 7, 8 | fmptd 7066 |
. . . . . . . . . 10
β’ (β€
β πΉ:ββΆβ) |
10 | 9 | ffvelcdmda 7039 |
. . . . . . . . 9
β’
((β€ β§ π
β β) β (πΉβπ) β β) |
11 | 1, 2, 10 | serfre 13946 |
. . . . . . . 8
β’ (β€
β seq1( + , πΉ):ββΆβ) |
12 | 11 | mptru 1549 |
. . . . . . 7
β’ seq1( + ,
πΉ):ββΆβ |
13 | | frn 6679 |
. . . . . . 7
β’ (seq1( +
, πΉ):ββΆβ
β ran seq1( + , πΉ)
β β) |
14 | 12, 13 | mp1i 13 |
. . . . . 6
β’ (seq1( +
, πΉ) β dom β
β ran seq1( + , πΉ)
β β) |
15 | | 1nn 12172 |
. . . . . . . 8
β’ 1 β
β |
16 | 12 | fdmi 6684 |
. . . . . . . 8
β’ dom seq1(
+ , πΉ) =
β |
17 | 15, 16 | eleqtrri 2833 |
. . . . . . 7
β’ 1 β
dom seq1( + , πΉ) |
18 | | ne0i 4298 |
. . . . . . . 8
β’ (1 β
dom seq1( + , πΉ) β dom
seq1( + , πΉ) β
β
) |
19 | | dm0rn0 5884 |
. . . . . . . . 9
β’ (dom
seq1( + , πΉ) = β
β ran seq1( + , πΉ) =
β
) |
20 | 19 | necon3bii 2993 |
. . . . . . . 8
β’ (dom
seq1( + , πΉ) β β
β ran seq1( + , πΉ)
β β
) |
21 | 18, 20 | sylib 217 |
. . . . . . 7
β’ (1 β
dom seq1( + , πΉ) β ran
seq1( + , πΉ) β
β
) |
22 | 17, 21 | mp1i 13 |
. . . . . 6
β’ (seq1( +
, πΉ) β dom β
β ran seq1( + , πΉ)
β β
) |
23 | | 1zzd 12542 |
. . . . . . . . 9
β’ (seq1( +
, πΉ) β dom β
β 1 β β€) |
24 | | climdm 15445 |
. . . . . . . . . 10
β’ (seq1( +
, πΉ) β dom β
β seq1( + , πΉ) β
( β βseq1( + , πΉ))) |
25 | 24 | biimpi 215 |
. . . . . . . . 9
β’ (seq1( +
, πΉ) β dom β
β seq1( + , πΉ) β
( β βseq1( + , πΉ))) |
26 | 12 | a1i 11 |
. . . . . . . . . 10
β’ (seq1( +
, πΉ) β dom β
β seq1( + , πΉ):ββΆβ) |
27 | 26 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (seq1( + , πΉ)βπ) β β) |
28 | 1, 23, 25, 27 | climrecl 15474 |
. . . . . . . 8
β’ (seq1( +
, πΉ) β dom β
β ( β βseq1( + , πΉ)) β β) |
29 | | simpr 486 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β π β
β) |
30 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β seq1( + , πΉ) β
( β βseq1( + , πΉ))) |
31 | | eleq1w 2817 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β β β π β β)) |
32 | | oveq2 7369 |
. . . . . . . . . . . . . . 15
β’ (π = π β (1 / π) = (1 / π)) |
33 | 31, 32 | ifbieq1d 4514 |
. . . . . . . . . . . . . 14
β’ (π = π β if(π β β, (1 / π), 0) = if(π β β, (1 / π), 0)) |
34 | | prmnn 16558 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π
β β) β π
β β) |
36 | 35 | nnrecred 12212 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π
β β) β (1 / π) β β) |
37 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ Β¬ π β β) β 0 β
β) |
38 | 36, 37 | ifclda 4525 |
. . . . . . . . . . . . . . . 16
β’ (β€
β if(π β β,
(1 / π), 0) β
β) |
39 | 38 | mptru 1549 |
. . . . . . . . . . . . . . 15
β’ if(π β β, (1 / π), 0) β
β |
40 | 39 | elexi 3466 |
. . . . . . . . . . . . . 14
β’ if(π β β, (1 / π), 0) β V |
41 | 33, 8, 40 | fvmpt 6952 |
. . . . . . . . . . . . 13
β’ (π β β β (πΉβπ) = if(π β β, (1 / π), 0)) |
42 | 41 | adantl 483 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (πΉβπ) = if(π β β, (1 / π), 0)) |
43 | 39 | a1i 11 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β if(π β β,
(1 / π), 0) β
β) |
44 | 42, 43 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (πΉβπ) β
β) |
45 | 44 | adantlr 714 |
. . . . . . . . . 10
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β β)
β (πΉβπ) β
β) |
46 | | nnrp 12934 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β+) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β π β
β+) |
48 | 47 | rpreccld 12975 |
. . . . . . . . . . . . . 14
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (1 / π) β
β+) |
49 | 48 | rpge0d 12969 |
. . . . . . . . . . . . 13
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β 0 β€ (1 / π)) |
50 | | 0le0 12262 |
. . . . . . . . . . . . 13
β’ 0 β€
0 |
51 | | breq2 5113 |
. . . . . . . . . . . . . 14
β’ ((1 /
π) = if(π β β, (1 / π), 0) β (0 β€ (1 / π) β 0 β€ if(π β β, (1 / π), 0))) |
52 | | breq2 5113 |
. . . . . . . . . . . . . 14
β’ (0 =
if(π β β, (1 /
π), 0) β (0 β€ 0
β 0 β€ if(π β
β, (1 / π),
0))) |
53 | 51, 52 | ifboth 4529 |
. . . . . . . . . . . . 13
β’ ((0 β€
(1 / π) β§ 0 β€ 0)
β 0 β€ if(π β
β, (1 / π),
0)) |
54 | 49, 50, 53 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β 0 β€ if(π β
β, (1 / π),
0)) |
55 | 54, 42 | breqtrrd 5137 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β 0 β€ (πΉβπ)) |
56 | 55 | adantlr 714 |
. . . . . . . . . 10
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β β)
β 0 β€ (πΉβπ)) |
57 | 1, 29, 30, 45, 56 | climserle 15556 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (seq1( + , πΉ)βπ) β€ ( β βseq1( + , πΉ))) |
58 | 57 | ralrimiva 3140 |
. . . . . . . 8
β’ (seq1( +
, πΉ) β dom β
β βπ β
β (seq1( + , πΉ)βπ) β€ ( β βseq1( + , πΉ))) |
59 | | brralrspcev 5169 |
. . . . . . . 8
β’ (((
β βseq1( + , πΉ)) β β β§ βπ β β (seq1( + , πΉ)βπ) β€ ( β βseq1( + , πΉ))) β βπ₯ β β βπ β β (seq1( + , πΉ)βπ) β€ π₯) |
60 | 28, 58, 59 | syl2anc 585 |
. . . . . . 7
β’ (seq1( +
, πΉ) β dom β
β βπ₯ β
β βπ β
β (seq1( + , πΉ)βπ) β€ π₯) |
61 | | ffn 6672 |
. . . . . . . . 9
β’ (seq1( +
, πΉ):ββΆβ
β seq1( + , πΉ) Fn
β) |
62 | | breq1 5112 |
. . . . . . . . . 10
β’ (π§ = (seq1( + , πΉ)βπ) β (π§ β€ π₯ β (seq1( + , πΉ)βπ) β€ π₯)) |
63 | 62 | ralrn 7042 |
. . . . . . . . 9
β’ (seq1( +
, πΉ) Fn β β
(βπ§ β ran seq1(
+ , πΉ)π§ β€ π₯ β βπ β β (seq1( + , πΉ)βπ) β€ π₯)) |
64 | 12, 61, 63 | mp2b 10 |
. . . . . . . 8
β’
(βπ§ β
ran seq1( + , πΉ)π§ β€ π₯ β βπ β β (seq1( + , πΉ)βπ) β€ π₯) |
65 | 64 | rexbii 3094 |
. . . . . . 7
β’
(βπ₯ β
β βπ§ β
ran seq1( + , πΉ)π§ β€ π₯ β βπ₯ β β βπ β β (seq1( + , πΉ)βπ) β€ π₯) |
66 | 60, 65 | sylibr 233 |
. . . . . 6
β’ (seq1( +
, πΉ) β dom β
β βπ₯ β
β βπ§ β
ran seq1( + , πΉ)π§ β€ π₯) |
67 | 14, 22, 66 | suprcld 12126 |
. . . . 5
β’ (seq1( +
, πΉ) β dom β
β sup(ran seq1( + , πΉ), β, < ) β
β) |
68 | | 2rp 12928 |
. . . . . 6
β’ 2 β
β+ |
69 | | rpreccl 12949 |
. . . . . 6
β’ (2 β
β+ β (1 / 2) β β+) |
70 | 68, 69 | ax-mp 5 |
. . . . 5
β’ (1 / 2)
β β+ |
71 | | ltsubrp 12959 |
. . . . 5
β’ ((sup(ran
seq1( + , πΉ), β, <
) β β β§ (1 / 2) β β+) β (sup(ran
seq1( + , πΉ), β, <
) β (1 / 2)) < sup(ran seq1( + , πΉ), β, < )) |
72 | 67, 70, 71 | sylancl 587 |
. . . 4
β’ (seq1( +
, πΉ) β dom β
β (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
sup(ran seq1( + , πΉ),
β, < )) |
73 | | halfre 12375 |
. . . . . 6
β’ (1 / 2)
β β |
74 | | resubcl 11473 |
. . . . . 6
β’ ((sup(ran
seq1( + , πΉ), β, <
) β β β§ (1 / 2) β β) β (sup(ran seq1( + , πΉ), β, < ) β (1 /
2)) β β) |
75 | 67, 73, 74 | sylancl 587 |
. . . . 5
β’ (seq1( +
, πΉ) β dom β
β (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) β
β) |
76 | | suprlub 12127 |
. . . . 5
β’ (((ran
seq1( + , πΉ) β
β β§ ran seq1( + , πΉ) β β
β§ βπ₯ β β βπ§ β ran seq1( + , πΉ)π§ β€ π₯) β§ (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) β
β) β ((sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
sup(ran seq1( + , πΉ),
β, < ) β βπ¦ β ran seq1( + , πΉ)(sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
π¦)) |
77 | 14, 22, 66, 75, 76 | syl31anc 1374 |
. . . 4
β’ (seq1( +
, πΉ) β dom β
β ((sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
sup(ran seq1( + , πΉ),
β, < ) β βπ¦ β ran seq1( + , πΉ)(sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
π¦)) |
78 | 72, 77 | mpbid 231 |
. . 3
β’ (seq1( +
, πΉ) β dom β
β βπ¦ β ran
seq1( + , πΉ)(sup(ran seq1(
+ , πΉ), β, < )
β (1 / 2)) < π¦) |
79 | | breq2 5113 |
. . . . 5
β’ (π¦ = (seq1( + , πΉ)βπ) β ((sup(ran seq1( + , πΉ), β, < ) β (1 /
2)) < π¦ β (sup(ran
seq1( + , πΉ), β, <
) β (1 / 2)) < (seq1( + , πΉ)βπ))) |
80 | 79 | rexrn 7041 |
. . . 4
β’ (seq1( +
, πΉ) Fn β β
(βπ¦ β ran seq1(
+ , πΉ)(sup(ran seq1( + ,
πΉ), β, < ) β
(1 / 2)) < π¦ β
βπ β β
(sup(ran seq1( + , πΉ),
β, < ) β (1 / 2)) < (seq1( + , πΉ)βπ))) |
81 | 12, 61, 80 | mp2b 10 |
. . 3
β’
(βπ¦ β ran
seq1( + , πΉ)(sup(ran seq1(
+ , πΉ), β, < )
β (1 / 2)) < π¦
β βπ β
β (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
(seq1( + , πΉ)βπ)) |
82 | 78, 81 | sylib 217 |
. 2
β’ (seq1( +
, πΉ) β dom β
β βπ β
β (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
(seq1( + , πΉ)βπ)) |
83 | | 2re 12235 |
. . . . . 6
β’ 2 β
β |
84 | | 2nn 12234 |
. . . . . . . . 9
β’ 2 β
β |
85 | | nnmulcl 12185 |
. . . . . . . . 9
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
86 | 84, 29, 85 | sylancr 588 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2 Β· π)
β β) |
87 | 86 | peano2nnd 12178 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2 Β· π) + 1)
β β) |
88 | 87 | nnnn0d 12481 |
. . . . . 6
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2 Β· π) + 1)
β β0) |
89 | | reexpcl 13993 |
. . . . . 6
β’ ((2
β β β§ ((2 Β· π) + 1) β β0) β
(2β((2 Β· π) +
1)) β β) |
90 | 83, 88, 89 | sylancr 588 |
. . . . 5
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β((2 Β· π) + 1)) β β) |
91 | 90 | ltnrd 11297 |
. . . 4
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Β¬ (2β((2 Β· π) + 1)) < (2β((2 Β· π) + 1))) |
92 | 29 | adantr 482 |
. . . . . . 7
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) β π β β) |
93 | | peano2nn 12173 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β) |
94 | 93 | adantl 483 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (π + 1) β
β) |
95 | 94 | nnnn0d 12481 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (π + 1) β
β0) |
96 | | nnexpcl 13989 |
. . . . . . . . . 10
β’ ((2
β β β§ (π +
1) β β0) β (2β(π + 1)) β β) |
97 | 84, 95, 96 | sylancr 588 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β(π + 1))
β β) |
98 | 97 | nnsqcld 14156 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2β(π +
1))β2) β β) |
99 | 98 | adantr 482 |
. . . . . . 7
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) β ((2β(π + 1))β2) β
β) |
100 | | breq1 5112 |
. . . . . . . . . . 11
β’ (π = π€ β (π β₯ π β π€ β₯ π)) |
101 | 100 | notbid 318 |
. . . . . . . . . 10
β’ (π = π€ β (Β¬ π β₯ π β Β¬ π€ β₯ π)) |
102 | 101 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ β
(β β (1...π))
Β¬ π β₯ π β βπ€ β (β β
(1...π)) Β¬ π€ β₯ π) |
103 | | breq2 5113 |
. . . . . . . . . . 11
β’ (π = π β (π€ β₯ π β π€ β₯ π)) |
104 | 103 | notbid 318 |
. . . . . . . . . 10
β’ (π = π β (Β¬ π€ β₯ π β Β¬ π€ β₯ π)) |
105 | 104 | ralbidv 3171 |
. . . . . . . . 9
β’ (π = π β (βπ€ β (β β (1...π)) Β¬ π€ β₯ π β βπ€ β (β β (1...π)) Β¬ π€ β₯ π)) |
106 | 102, 105 | bitrid 283 |
. . . . . . . 8
β’ (π = π β (βπ β (β β (1...π)) Β¬ π β₯ π β βπ€ β (β β (1...π)) Β¬ π€ β₯ π)) |
107 | 106 | cbvrabv 3416 |
. . . . . . 7
β’ {π β (1...((2β(π + 1))β2)) β£
βπ β (β
β (1...π)) Β¬
π β₯ π} = {π β (1...((2β(π + 1))β2)) β£ βπ€ β (β β
(1...π)) Β¬ π€ β₯ π} |
108 | | simpll 766 |
. . . . . . 7
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) β seq1( + , πΉ) β dom β
) |
109 | | eleq1w 2817 |
. . . . . . . . . 10
β’ (π = π β (π β β β π β β)) |
110 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = π β (1 / π) = (1 / π)) |
111 | 109, 110 | ifbieq1d 4514 |
. . . . . . . . 9
β’ (π = π β if(π β β, (1 / π), 0) = if(π β β, (1 / π), 0)) |
112 | 111 | cbvsumv 15589 |
. . . . . . . 8
β’
Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) = Ξ£π β (β€β₯β(π + 1))if(π β β, (1 / π), 0) |
113 | | simpr 486 |
. . . . . . . 8
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) β Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) |
114 | 112, 113 | eqbrtrid 5144 |
. . . . . . 7
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) β Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) |
115 | | eqid 2733 |
. . . . . . 7
β’ (π€ β β β¦ {π β (1...((2β(π + 1))β2)) β£ (π€ β β β§ π€ β₯ π)}) = (π€ β β β¦ {π β (1...((2β(π + 1))β2)) β£ (π€ β β β§ π€ β₯ π)}) |
116 | 8, 92, 99, 107, 108, 114, 115 | prmreclem5 16800 |
. . . . . 6
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2)) β (((2β(π + 1))β2) / 2) <
((2βπ) Β·
(ββ((2β(π
+ 1))β2)))) |
117 | 116 | ex 414 |
. . . . 5
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2) β (((2β(π + 1))β2) / 2) <
((2βπ) Β·
(ββ((2β(π
+ 1))β2))))) |
118 | | eqid 2733 |
. . . . . . . . 9
β’
(β€β₯β(π + 1)) = (β€β₯β(π + 1)) |
119 | 94 | nnzd 12534 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (π + 1) β
β€) |
120 | | eluznn 12851 |
. . . . . . . . . . 11
β’ (((π + 1) β β β§ π β
(β€β₯β(π + 1))) β π β β) |
121 | 94, 120 | sylan 581 |
. . . . . . . . . 10
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β
(β€β₯β(π + 1))) β π β β) |
122 | 121, 41 | syl 17 |
. . . . . . . . 9
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β
(β€β₯β(π + 1))) β (πΉβπ) = if(π β β, (1 / π), 0)) |
123 | 39 | a1i 11 |
. . . . . . . . 9
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β
(β€β₯β(π + 1))) β if(π β β, (1 / π), 0) β β) |
124 | | simpl 484 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β seq1( + , πΉ) β
dom β ) |
125 | 41 | adantl 483 |
. . . . . . . . . . . 12
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β β)
β (πΉβπ) = if(π β β, (1 / π), 0)) |
126 | 39 | recni 11177 |
. . . . . . . . . . . . 13
β’ if(π β β, (1 / π), 0) β
β |
127 | 126 | a1i 11 |
. . . . . . . . . . . 12
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β β)
β if(π β β,
(1 / π), 0) β
β) |
128 | 125, 127 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β β)
β (πΉβπ) β
β) |
129 | 1, 94, 128 | iserex 15550 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (seq1( + , πΉ) β
dom β β seq(π +
1)( + , πΉ) β dom
β )) |
130 | 124, 129 | mpbid 231 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β seq(π + 1)( + ,
πΉ) β dom β
) |
131 | 118, 119,
122, 123, 130 | isumrecl 15658 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) β β) |
132 | 73 | a1i 11 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (1 / 2) β β) |
133 | | elfznn 13479 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β) |
134 | 133 | adantl 483 |
. . . . . . . . . . 11
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β (1...π)) β π β β) |
135 | 134, 41 | syl 17 |
. . . . . . . . . 10
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β (1...π)) β (πΉβπ) = if(π β β, (1 / π), 0)) |
136 | 29, 1 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β π β
(β€β₯β1)) |
137 | 126 | a1i 11 |
. . . . . . . . . 10
β’ (((seq1(
+ , πΉ) β dom β
β§ π β β)
β§ π β (1...π)) β if(π β β, (1 / π), 0) β β) |
138 | 135, 136,
137 | fsumser 15623 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
(1...π)if(π β β, (1 / π), 0) = (seq1( + , πΉ)βπ)) |
139 | 138, 27 | eqeltrd 2834 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
(1...π)if(π β β, (1 / π), 0) β
β) |
140 | 131, 132,
139 | ltadd2d 11319 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2) β (Ξ£π β (1...π)if(π β β, (1 / π), 0) + Ξ£π β (β€β₯β(π + 1))if(π β β, (1 / π), 0)) < (Ξ£π β (1...π)if(π β β, (1 / π), 0) + (1 / 2)))) |
141 | 1, 118, 94, 125, 127, 124 | isumsplit 15733 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
β if(π β
β, (1 / π), 0) =
(Ξ£π β
(1...((π + 1) β
1))if(π β β, (1
/ π), 0) + Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0))) |
142 | | nncn 12169 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
143 | 142 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β π β
β) |
144 | | ax-1cn 11117 |
. . . . . . . . . . . . 13
β’ 1 β
β |
145 | | pncan 11415 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
146 | 143, 144,
145 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((π + 1) β 1)
= π) |
147 | 146 | oveq2d 7377 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (1...((π + 1)
β 1)) = (1...π)) |
148 | 147 | sumeq1d 15594 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
(1...((π + 1) β
1))if(π β β, (1
/ π), 0) = Ξ£π β (1...π)if(π β β, (1 / π), 0)) |
149 | 148 | oveq1d 7376 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
(1...((π + 1) β
1))if(π β β, (1
/ π), 0) + Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0)) = (Ξ£π β (1...π)if(π β β, (1 / π), 0) + Ξ£π β (β€β₯β(π + 1))if(π β β, (1 / π), 0))) |
150 | 141, 149 | eqtrd 2773 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
β if(π β
β, (1 / π), 0) =
(Ξ£π β (1...π)if(π β β, (1 / π), 0) + Ξ£π β (β€β₯β(π + 1))if(π β β, (1 / π), 0))) |
151 | 150 | breq1d 5119 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
β if(π β
β, (1 / π), 0) <
(Ξ£π β (1...π)if(π β β, (1 / π), 0) + (1 / 2)) β (Ξ£π β (1...π)if(π β β, (1 / π), 0) + Ξ£π β (β€β₯β(π + 1))if(π β β, (1 / π), 0)) < (Ξ£π β (1...π)if(π β β, (1 / π), 0) + (1 / 2)))) |
152 | 140, 151 | bitr4d 282 |
. . . . . 6
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2) β Ξ£π β β if(π β β, (1 / π), 0) < (Ξ£π β (1...π)if(π β β, (1 / π), 0) + (1 / 2)))) |
153 | | eqid 2733 |
. . . . . . . . . 10
β’ seq1( + ,
πΉ) = seq1( + , πΉ) |
154 | 1, 153, 23, 42, 43, 54, 60 | isumsup 15740 |
. . . . . . . . 9
β’ (seq1( +
, πΉ) β dom β
β Ξ£π β
β if(π β
β, (1 / π), 0) =
sup(ran seq1( + , πΉ),
β, < )) |
155 | 154, 67 | eqeltrd 2834 |
. . . . . . . 8
β’ (seq1( +
, πΉ) β dom β
β Ξ£π β
β if(π β
β, (1 / π), 0) β
β) |
156 | 155 | adantr 482 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
β if(π β
β, (1 / π), 0) β
β) |
157 | 156, 132,
139 | ltsubaddd 11759 |
. . . . . 6
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((Ξ£π β
β if(π β
β, (1 / π), 0)
β (1 / 2)) < Ξ£π β (1...π)if(π β β, (1 / π), 0) β Ξ£π β β if(π β β, (1 / π), 0) < (Ξ£π β (1...π)if(π β β, (1 / π), 0) + (1 / 2)))) |
158 | 154 | adantr 482 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Ξ£π β
β if(π β
β, (1 / π), 0) =
sup(ran seq1( + , πΉ),
β, < )) |
159 | 158 | oveq1d 7376 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
β if(π β
β, (1 / π), 0)
β (1 / 2)) = (sup(ran seq1( + , πΉ), β, < ) β (1 /
2))) |
160 | 159, 138 | breq12d 5122 |
. . . . . 6
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((Ξ£π β
β if(π β
β, (1 / π), 0)
β (1 / 2)) < Ξ£π β (1...π)if(π β β, (1 / π), 0) β (sup(ran seq1( + , πΉ), β, < ) β (1 /
2)) < (seq1( + , πΉ)βπ))) |
161 | 152, 157,
160 | 3bitr2d 307 |
. . . . 5
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (Ξ£π β
(β€β₯β(π + 1))if(π β β, (1 / π), 0) < (1 / 2) β (sup(ran seq1( + ,
πΉ), β, < ) β
(1 / 2)) < (seq1( + , πΉ)βπ))) |
162 | | 2cn 12236 |
. . . . . . . . . . . . 13
β’ 2 β
β |
163 | 162 | a1i 11 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β 2 β β) |
164 | 144 | a1i 11 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β 1 β β) |
165 | 163, 143,
164 | adddid 11187 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2 Β· (π + 1))
= ((2 Β· π) + (2
Β· 1))) |
166 | 94 | nncnd 12177 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (π + 1) β
β) |
167 | | mulcom 11145 |
. . . . . . . . . . . 12
β’ (((π + 1) β β β§ 2
β β) β ((π
+ 1) Β· 2) = (2 Β· (π + 1))) |
168 | 166, 162,
167 | sylancl 587 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((π + 1) Β· 2)
= (2 Β· (π +
1))) |
169 | 86 | nncnd 12177 |
. . . . . . . . . . . . 13
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2 Β· π)
β β) |
170 | 169, 164,
164 | addassd 11185 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (((2 Β· π) +
1) + 1) = ((2 Β· π) +
(1 + 1))) |
171 | 144 | 2timesi 12299 |
. . . . . . . . . . . . 13
β’ (2
Β· 1) = (1 + 1) |
172 | 171 | oveq2i 7372 |
. . . . . . . . . . . 12
β’ ((2
Β· π) + (2 Β·
1)) = ((2 Β· π) + (1
+ 1)) |
173 | 170, 172 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (((2 Β· π) +
1) + 1) = ((2 Β· π) +
(2 Β· 1))) |
174 | 165, 168,
173 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((π + 1) Β· 2)
= (((2 Β· π) + 1) +
1)) |
175 | 174 | oveq2d 7377 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β((π + 1)
Β· 2)) = (2β(((2 Β· π) + 1) + 1))) |
176 | | 2nn0 12438 |
. . . . . . . . . . 11
β’ 2 β
β0 |
177 | 176 | a1i 11 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β 2 β β0) |
178 | 163, 177,
95 | expmuld 14063 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β((π + 1)
Β· 2)) = ((2β(π
+ 1))β2)) |
179 | | expp1 13983 |
. . . . . . . . . 10
β’ ((2
β β β§ ((2 Β· π) + 1) β β0) β
(2β(((2 Β· π) +
1) + 1)) = ((2β((2 Β· π) + 1)) Β· 2)) |
180 | 162, 88, 179 | sylancr 588 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β(((2 Β· π) + 1) + 1)) = ((2β((2 Β· π) + 1)) Β·
2)) |
181 | 175, 178,
180 | 3eqtr3d 2781 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2β(π +
1))β2) = ((2β((2 Β· π) + 1)) Β· 2)) |
182 | 181 | oveq1d 7376 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (((2β(π +
1))β2) / 2) = (((2β((2 Β· π) + 1)) Β· 2) / 2)) |
183 | | expcl 13994 |
. . . . . . . . 9
β’ ((2
β β β§ ((2 Β· π) + 1) β β0) β
(2β((2 Β· π) +
1)) β β) |
184 | 162, 88, 183 | sylancr 588 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β((2 Β· π) + 1)) β β) |
185 | | 2ne0 12265 |
. . . . . . . . 9
β’ 2 β
0 |
186 | | divcan4 11848 |
. . . . . . . . 9
β’
(((2β((2 Β· π) + 1)) β β β§ 2 β β
β§ 2 β 0) β (((2β((2 Β· π) + 1)) Β· 2) / 2) = (2β((2
Β· π) +
1))) |
187 | 162, 185,
186 | mp3an23 1454 |
. . . . . . . 8
β’
((2β((2 Β· π) + 1)) β β β (((2β((2
Β· π) + 1)) Β·
2) / 2) = (2β((2 Β· π) + 1))) |
188 | 184, 187 | syl 17 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (((2β((2 Β· π) + 1)) Β· 2) / 2) = (2β((2
Β· π) +
1))) |
189 | 182, 188 | eqtrd 2773 |
. . . . . 6
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (((2β(π +
1))β2) / 2) = (2β((2 Β· π) + 1))) |
190 | | nnnn0 12428 |
. . . . . . . . 9
β’ (π β β β π β
β0) |
191 | 190 | adantl 483 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β π β
β0) |
192 | 163, 95, 191 | expaddd 14062 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β(π + (π + 1))) = ((2βπ) Β· (2β(π + 1)))) |
193 | 143 | 2timesd 12404 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2 Β· π) =
(π + π)) |
194 | 193 | oveq1d 7376 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2 Β· π) + 1)
= ((π + π) + 1)) |
195 | 143, 143,
164 | addassd 11185 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((π + π) + 1) = (π + (π + 1))) |
196 | 194, 195 | eqtrd 2773 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2 Β· π) + 1)
= (π + (π + 1))) |
197 | 196 | oveq2d 7377 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β((2 Β· π) + 1)) = (2β(π + (π + 1)))) |
198 | 97 | nnrpd 12963 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (2β(π + 1))
β β+) |
199 | 198 | rprege0d 12972 |
. . . . . . . . 9
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2β(π + 1))
β β β§ 0 β€ (2β(π + 1)))) |
200 | | sqrtsq 15163 |
. . . . . . . . 9
β’
(((2β(π + 1))
β β β§ 0 β€ (2β(π + 1))) β (ββ((2β(π + 1))β2)) = (2β(π + 1))) |
201 | 199, 200 | syl 17 |
. . . . . . . 8
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β (ββ((2β(π + 1))β2)) = (2β(π + 1))) |
202 | 201 | oveq2d 7377 |
. . . . . . 7
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2βπ) Β·
(ββ((2β(π
+ 1))β2))) = ((2βπ) Β· (2β(π + 1)))) |
203 | 192, 197,
202 | 3eqtr4rd 2784 |
. . . . . 6
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((2βπ) Β·
(ββ((2β(π
+ 1))β2))) = (2β((2 Β· π) + 1))) |
204 | 189, 203 | breq12d 5122 |
. . . . 5
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((((2β(π +
1))β2) / 2) < ((2βπ) Β· (ββ((2β(π + 1))β2))) β
(2β((2 Β· π) +
1)) < (2β((2 Β· π) + 1)))) |
205 | 117, 161,
204 | 3imtr3d 293 |
. . . 4
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β ((sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
(seq1( + , πΉ)βπ) β (2β((2 Β·
π) + 1)) < (2β((2
Β· π) +
1)))) |
206 | 91, 205 | mtod 197 |
. . 3
β’ ((seq1( +
, πΉ) β dom β
β§ π β β)
β Β¬ (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
(seq1( + , πΉ)βπ)) |
207 | 206 | nrexdv 3143 |
. 2
β’ (seq1( +
, πΉ) β dom β
β Β¬ βπ
β β (sup(ran seq1( + , πΉ), β, < ) β (1 / 2)) <
(seq1( + , πΉ)βπ)) |
208 | 82, 207 | pm2.65i 193 |
1
β’ Β¬
seq1( + , πΉ) β dom
β |