Step | Hyp | Ref
| Expression |
1 | | nnuz 12814 |
. . . . 5
β’ β =
(β€β₯β1) |
2 | | 1zzd 12542 |
. . . . 5
β’ (πΉ:ββΆ(0[,)+β)
β 1 β β€) |
3 | | rge0ssre 13382 |
. . . . . . 7
β’
(0[,)+β) β β |
4 | | fss 6689 |
. . . . . . 7
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
5 | 3, 4 | mpan2 690 |
. . . . . 6
β’ (πΉ:ββΆ(0[,)+β)
β πΉ:ββΆβ) |
6 | 5 | ffvelcdmda 7039 |
. . . . 5
β’ ((πΉ:ββΆ(0[,)+β)
β§ π β β)
β (πΉβπ) β
β) |
7 | 1, 2, 6 | serfre 13946 |
. . . 4
β’ (πΉ:ββΆ(0[,)+β)
β seq1( + , πΉ):ββΆβ) |
8 | 7 | frnd 6680 |
. . 3
β’ (πΉ:ββΆ(0[,)+β)
β ran seq1( + , πΉ)
β β) |
9 | 8 | adantr 482 |
. 2
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β ran seq1( + , πΉ) β β) |
10 | | 1nn 12172 |
. . . . 5
β’ 1 β
β |
11 | | fdm 6681 |
. . . . 5
β’ (seq1( +
, πΉ):ββΆβ
β dom seq1( + , πΉ) =
β) |
12 | 10, 11 | eleqtrrid 2841 |
. . . 4
β’ (seq1( +
, πΉ):ββΆβ
β 1 β dom seq1( + , πΉ)) |
13 | | ne0i 4298 |
. . . . 5
β’ (1 β
dom seq1( + , πΉ) β dom
seq1( + , πΉ) β
β
) |
14 | | dm0rn0 5884 |
. . . . . 6
β’ (dom
seq1( + , πΉ) = β
β ran seq1( + , πΉ) =
β
) |
15 | 14 | necon3bii 2993 |
. . . . 5
β’ (dom
seq1( + , πΉ) β β
β ran seq1( + , πΉ)
β β
) |
16 | 13, 15 | sylib 217 |
. . . 4
β’ (1 β
dom seq1( + , πΉ) β ran
seq1( + , πΉ) β
β
) |
17 | 7, 12, 16 | 3syl 18 |
. . 3
β’ (πΉ:ββΆ(0[,)+β)
β ran seq1( + , πΉ)
β β
) |
18 | 17 | adantr 482 |
. 2
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β ran seq1( + , πΉ) β β
) |
19 | | 1zzd 12542 |
. . . . 5
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β 1 β β€) |
20 | | climdm 15445 |
. . . . . . 7
β’ (seq1( +
, πΉ) β dom β
β seq1( + , πΉ) β
( β βseq1( + , πΉ))) |
21 | 20 | biimpi 215 |
. . . . . 6
β’ (seq1( +
, πΉ) β dom β
β seq1( + , πΉ) β
( β βseq1( + , πΉ))) |
22 | 21 | adantl 483 |
. . . . 5
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β seq1( + , πΉ) β ( β βseq1( + , πΉ))) |
23 | 7 | adantr 482 |
. . . . . 6
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β seq1( + , πΉ):ββΆβ) |
24 | 23 | ffvelcdmda 7039 |
. . . . 5
β’ (((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β (seq1( + , πΉ)βπ) β β) |
25 | 1, 19, 22, 24 | climrecl 15474 |
. . . 4
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β ( β βseq1( + , πΉ)) β β) |
26 | | simpr 486 |
. . . . . 6
β’ (((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β π
β β) |
27 | 22 | adantr 482 |
. . . . . 6
β’ (((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β seq1( + , πΉ) β ( β βseq1( + , πΉ))) |
28 | | simplll 774 |
. . . . . . 7
β’ ((((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β§ π
β β) β πΉ:ββΆ(0[,)+β)) |
29 | | ffvelcdm 7036 |
. . . . . . . 8
β’ ((πΉ:ββΆ(0[,)+β)
β§ π β β)
β (πΉβπ) β
(0[,)+β)) |
30 | 3, 29 | sselid 3946 |
. . . . . . 7
β’ ((πΉ:ββΆ(0[,)+β)
β§ π β β)
β (πΉβπ) β
β) |
31 | 28, 30 | sylancom 589 |
. . . . . 6
β’ ((((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β§ π
β β) β (πΉβπ) β β) |
32 | | elrege0 13380 |
. . . . . . . . . 10
β’ ((πΉβπ) β (0[,)+β) β ((πΉβπ) β β β§ 0 β€ (πΉβπ))) |
33 | 32 | simprbi 498 |
. . . . . . . . 9
β’ ((πΉβπ) β (0[,)+β) β 0 β€ (πΉβπ)) |
34 | 29, 33 | syl 17 |
. . . . . . . 8
β’ ((πΉ:ββΆ(0[,)+β)
β§ π β β)
β 0 β€ (πΉβπ)) |
35 | 34 | adantlr 714 |
. . . . . . 7
β’ (((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β 0 β€ (πΉβπ)) |
36 | 35 | adantlr 714 |
. . . . . 6
β’ ((((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β§ π
β β) β 0 β€ (πΉβπ)) |
37 | 1, 26, 27, 31, 36 | climserle 15556 |
. . . . 5
β’ (((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β§ π
β β) β (seq1( + , πΉ)βπ) β€ ( β βseq1( + , πΉ))) |
38 | 37 | ralrimiva 3140 |
. . . 4
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β βπ β β (seq1( + , πΉ)βπ) β€ ( β βseq1( + , πΉ))) |
39 | | brralrspcev 5169 |
. . . 4
β’ (((
β βseq1( + , πΉ)) β β β§ βπ β β (seq1( + , πΉ)βπ) β€ ( β βseq1( + , πΉ))) β βπ₯ β β βπ β β (seq1( + , πΉ)βπ) β€ π₯) |
40 | 25, 38, 39 | syl2anc 585 |
. . 3
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β βπ₯ β β βπ β β (seq1( + , πΉ)βπ) β€ π₯) |
41 | | ffn 6672 |
. . . . . 6
β’ (seq1( +
, πΉ):ββΆβ
β seq1( + , πΉ) Fn
β) |
42 | | breq1 5112 |
. . . . . . 7
β’ (π§ = (seq1( + , πΉ)βπ) β (π§ β€ π₯ β (seq1( + , πΉ)βπ) β€ π₯)) |
43 | 42 | ralrn 7042 |
. . . . . 6
β’ (seq1( +
, πΉ) Fn β β
(βπ§ β ran seq1(
+ , πΉ)π§ β€ π₯ β βπ β β (seq1( + , πΉ)βπ) β€ π₯)) |
44 | 7, 41, 43 | 3syl 18 |
. . . . 5
β’ (πΉ:ββΆ(0[,)+β)
β (βπ§ β
ran seq1( + , πΉ)π§ β€ π₯ β βπ β β (seq1( + , πΉ)βπ) β€ π₯)) |
45 | 44 | rexbidv 3172 |
. . . 4
β’ (πΉ:ββΆ(0[,)+β)
β (βπ₯ β
β βπ§ β
ran seq1( + , πΉ)π§ β€ π₯ β βπ₯ β β βπ β β (seq1( + , πΉ)βπ) β€ π₯)) |
46 | 45 | adantr 482 |
. . 3
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β (βπ₯ β β βπ§ β ran seq1( + , πΉ)π§ β€ π₯ β βπ₯ β β βπ β β (seq1( + , πΉ)βπ) β€ π₯)) |
47 | 40, 46 | mpbird 257 |
. 2
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β βπ₯ β β βπ§ β ran seq1( + , πΉ)π§ β€ π₯) |
48 | | suprcl 12123 |
. 2
β’ ((ran
seq1( + , πΉ) β
β β§ ran seq1( + , πΉ) β β
β§ βπ₯ β β βπ§ β ran seq1( + , πΉ)π§ β€ π₯) β sup(ran seq1( + , πΉ), β, < ) β
β) |
49 | 9, 18, 47, 48 | syl3anc 1372 |
1
β’ ((πΉ:ββΆ(0[,)+β)
β§ seq1( + , πΉ) β
dom β ) β sup(ran seq1( + , πΉ), β, < ) β
β) |