Step | Hyp | Ref
| Expression |
1 | | xrltso 13071 |
. . . 4
β’ < Or
β* |
2 | 1 | supex 9409 |
. . 3
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β V |
3 | 2 | a1i 11 |
. 2
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
sup(((πΉ β (π[,)+β)) β©
β*), β*, < ) β V) |
4 | | limsupval.1 |
. . 3
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
5 | 4 | a1i 11 |
. 2
β’ ((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
6 | 4 | limsupgval 15371 |
. . . 4
β’ (π β β β (πΊβπ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
7 | 6 | adantl 483 |
. . 3
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (πΊβπ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
8 | | simpl3 1194 |
. . . . . . 7
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (lim
supβπΉ) <
+β) |
9 | | limsupgre.z |
. . . . . . . . . . 11
β’ π =
(β€β₯βπ) |
10 | | uzssz 12794 |
. . . . . . . . . . 11
β’
(β€β₯βπ) β β€ |
11 | 9, 10 | eqsstri 3982 |
. . . . . . . . . 10
β’ π β
β€ |
12 | | zssre 12516 |
. . . . . . . . . 10
β’ β€
β β |
13 | 11, 12 | sstri 3957 |
. . . . . . . . 9
β’ π β
β |
14 | 13 | a1i 11 |
. . . . . . . 8
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β
β) |
15 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β πΉ:πβΆβ) |
16 | | ressxr 11209 |
. . . . . . . . 9
β’ β
β β* |
17 | | fss 6691 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ β β
β*) β πΉ:πβΆβ*) |
18 | 15, 16, 17 | sylancl 587 |
. . . . . . . 8
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β πΉ:πβΆβ*) |
19 | | pnfxr 11219 |
. . . . . . . . 9
β’ +β
β β* |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β +β
β β*) |
21 | 4 | limsuplt 15374 |
. . . . . . . 8
β’ ((π β β β§ πΉ:πβΆβ* β§ +β
β β*) β ((lim supβπΉ) < +β β βπ β β (πΊβπ) < +β)) |
22 | 14, 18, 20, 21 | syl3anc 1372 |
. . . . . . 7
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β ((lim
supβπΉ) < +β
β βπ β
β (πΊβπ) <
+β)) |
23 | 8, 22 | mpbid 231 |
. . . . . 6
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
βπ β β
(πΊβπ) < +β) |
24 | | fzfi 13888 |
. . . . . . . 8
β’ (π...(ββπ)) β Fin |
25 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β§ (π β β β§ (πΊβπ) < +β)) β πΉ:πβΆβ) |
26 | | elfzuz 13448 |
. . . . . . . . . . 11
β’ (π β (π...(ββπ)) β π β (β€β₯βπ)) |
27 | 26, 9 | eleqtrrdi 2844 |
. . . . . . . . . 10
β’ (π β (π...(ββπ)) β π β π) |
28 | | ffvelcdm 7038 |
. . . . . . . . . 10
β’ ((πΉ:πβΆβ β§ π β π) β (πΉβπ) β β) |
29 | 25, 27, 28 | syl2an 597 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ π β (π...(ββπ))) β (πΉβπ) β β) |
30 | 29 | ralrimiva 3140 |
. . . . . . . 8
β’ ((((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β§ (π β β β§ (πΊβπ) < +β)) β βπ β (π...(ββπ))(πΉβπ) β β) |
31 | | fimaxre3 12111 |
. . . . . . . 8
β’ (((π...(ββπ)) β Fin β§
βπ β (π...(ββπ))(πΉβπ) β β) β βπ β β βπ β (π...(ββπ))(πΉβπ) β€ π) |
32 | 24, 30, 31 | sylancr 588 |
. . . . . . 7
β’ ((((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β§ (π β β β§ (πΊβπ) < +β)) β βπ β β βπ β (π...(ββπ))(πΉβπ) β€ π) |
33 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β
β) |
34 | 33 | ad2antrr 725 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π β β) |
35 | 4 | limsupgf 15370 |
. . . . . . . . . 10
β’ πΊ:ββΆβ* |
36 | 35 | ffvelcdmi 7040 |
. . . . . . . . 9
β’ (π β β β (πΊβπ) β
β*) |
37 | 34, 36 | syl 17 |
. . . . . . . 8
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (πΊβπ) β
β*) |
38 | | simprl 770 |
. . . . . . . . . 10
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π β β) |
39 | 16, 38 | sselid 3946 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π β β*) |
40 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β§ (π β β β§ (πΊβπ) < +β)) β π β β) |
41 | 40 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π β β) |
42 | 35 | ffvelcdmi 7040 |
. . . . . . . . . 10
β’ (π β β β (πΊβπ) β
β*) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (πΊβπ) β
β*) |
44 | 39, 43 | ifcld 4538 |
. . . . . . . 8
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β if((πΊβπ) β€ π, π, (πΊβπ)) β
β*) |
45 | 19 | a1i 11 |
. . . . . . . 8
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β +β β
β*) |
46 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β β) |
47 | 13 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π β β) |
48 | 47 | sselda 3948 |
. . . . . . . . . . . 12
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β β) |
49 | 43 | xrleidd 13082 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (πΊβπ) β€ (πΊβπ)) |
50 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β πΉ:πβΆβ*) |
51 | 4 | limsupgle 15372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ πΉ:πβΆβ*) β§ π β β β§ (πΊβπ) β β*) β ((πΊβπ) β€ (πΊβπ) β βπ β π (π β€ π β (πΉβπ) β€ (πΊβπ)))) |
52 | 47, 50, 41, 43, 51 | syl211anc 1377 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β ((πΊβπ) β€ (πΊβπ) β βπ β π (π β€ π β (πΉβπ) β€ (πΊβπ)))) |
53 | 49, 52 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β βπ β π (π β€ π β (πΉβπ) β€ (πΊβπ))) |
54 | 53 | r19.21bi 3233 |
. . . . . . . . . . . . . 14
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (π β€ π β (πΉβπ) β€ (πΊβπ))) |
55 | 54 | imp 408 |
. . . . . . . . . . . . 13
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β (πΉβπ) β€ (πΊβπ)) |
56 | 46, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (πΊβπ) β
β*) |
57 | 39 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β β*) |
58 | | xrmax1 13105 |
. . . . . . . . . . . . . . . 16
β’ (((πΊβπ) β β* β§ π β β*)
β (πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
59 | 56, 57, 58 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
60 | 50 | ffvelcdmda 7041 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (πΉβπ) β
β*) |
61 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β if((πΊβπ) β€ π, π, (πΊβπ)) β
β*) |
62 | | xrletr 13088 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β β* β§ (πΊβπ) β β* β§ if((πΊβπ) β€ π, π, (πΊβπ)) β β*) β
(((πΉβπ) β€ (πΊβπ) β§ (πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
63 | 60, 56, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (((πΉβπ) β€ (πΊβπ) β§ (πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
64 | 59, 63 | mpan2d 693 |
. . . . . . . . . . . . . 14
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β ((πΉβπ) β€ (πΊβπ) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β ((πΉβπ) β€ (πΊβπ) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
66 | 55, 65 | mpd 15 |
. . . . . . . . . . . 12
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
67 | | fveq2 6848 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
68 | 67 | breq1d 5121 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ) β€ π β (πΉβπ) β€ π)) |
69 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β βπ β (π...(ββπ))(πΉβπ) β€ π) |
70 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β βπ β (π...(ββπ))(πΉβπ) β€ π) |
71 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β π) |
72 | 71, 9 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β (β€β₯βπ)) |
73 | 41 | flcld 13714 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (ββπ) β β€) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (ββπ) β β€) |
75 | | elfz5 13444 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯βπ) β§ (ββπ) β β€) β (π β (π...(ββπ)) β π β€ (ββπ))) |
76 | 72, 74, 75 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (π β (π...(ββπ)) β π β€ (ββπ))) |
77 | 11, 71 | sselid 3946 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β β€) |
78 | | flge 13721 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β€) β (π β€ π β π β€ (ββπ))) |
79 | 46, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (π β€ π β π β€ (ββπ))) |
80 | 76, 79 | bitr4d 282 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (π β (π...(ββπ)) β π β€ π)) |
81 | 80 | biimpar 479 |
. . . . . . . . . . . . . 14
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β π β (π...(ββπ))) |
82 | 68, 70, 81 | rspcdva 3584 |
. . . . . . . . . . . . 13
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β (πΉβπ) β€ π) |
83 | | xrmax2 13106 |
. . . . . . . . . . . . . . . . 17
β’ (((πΊβπ) β β* β§ π β β*)
β π β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
84 | 43, 39, 83 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
85 | 84 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β π β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
86 | | xrletr 13088 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β β* β§ π β β*
β§ if((πΊβπ) β€ π, π, (πΊβπ)) β β*) β
(((πΉβπ) β€ π β§ π β€ if((πΊβπ) β€ π, π, (πΊβπ))) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
87 | 60, 57, 61, 86 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (((πΉβπ) β€ π β§ π β€ if((πΊβπ) β€ π, π, (πΊβπ))) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
88 | 85, 87 | mpan2d 693 |
. . . . . . . . . . . . . 14
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β ((πΉβπ) β€ π β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β ((πΉβπ) β€ π β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
90 | 82, 89 | mpd 15 |
. . . . . . . . . . . 12
β’
(((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β§ π β€ π) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
91 | 46, 48, 66, 90 | lecasei 11271 |
. . . . . . . . . . 11
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
92 | 91 | a1d 25 |
. . . . . . . . . 10
β’
((((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β§ π β π) β (π β€ π β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
93 | 92 | ralrimiva 3140 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β βπ β π (π β€ π β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)))) |
94 | 4 | limsupgle 15372 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:πβΆβ*) β§ π β β β§ if((πΊβπ) β€ π, π, (πΊβπ)) β β*) β ((πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)) β βπ β π (π β€ π β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))))) |
95 | 47, 50, 34, 44, 94 | syl211anc 1377 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β ((πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ)) β βπ β π (π β€ π β (πΉβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))))) |
96 | 93, 95 | mpbird 257 |
. . . . . . . 8
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (πΊβπ) β€ if((πΊβπ) β€ π, π, (πΊβπ))) |
97 | 38 | ltpnfd 13052 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β π < +β) |
98 | | simplrr 777 |
. . . . . . . . 9
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (πΊβπ) < +β) |
99 | | breq1 5114 |
. . . . . . . . . 10
β’ (π = if((πΊβπ) β€ π, π, (πΊβπ)) β (π < +β β if((πΊβπ) β€ π, π, (πΊβπ)) < +β)) |
100 | | breq1 5114 |
. . . . . . . . . 10
β’ ((πΊβπ) = if((πΊβπ) β€ π, π, (πΊβπ)) β ((πΊβπ) < +β β if((πΊβπ) β€ π, π, (πΊβπ)) < +β)) |
101 | 99, 100 | ifboth 4531 |
. . . . . . . . 9
β’ ((π < +β β§ (πΊβπ) < +β) β if((πΊβπ) β€ π, π, (πΊβπ)) < +β) |
102 | 97, 98, 101 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β if((πΊβπ) β€ π, π, (πΊβπ)) < +β) |
103 | 37, 44, 45, 96, 102 | xrlelttrd 13090 |
. . . . . . 7
β’
(((((π β
β€ β§ πΉ:πβΆβ β§ (lim
supβπΉ) < +β)
β§ π β β)
β§ (π β β
β§ (πΊβπ) < +β)) β§ (π β β β§
βπ β (π...(ββπ))(πΉβπ) β€ π)) β (πΊβπ) < +β) |
104 | 32, 103 | rexlimddv 3155 |
. . . . . 6
β’ ((((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β§ (π β β β§ (πΊβπ) < +β)) β (πΊβπ) < +β) |
105 | 23, 104 | rexlimddv 3155 |
. . . . 5
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (πΊβπ) < +β) |
106 | 7, 105 | eqbrtrrd 5135 |
. . . 4
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
sup(((πΉ β (π[,)+β)) β©
β*), β*, < ) <
+β) |
107 | | imassrn 6030 |
. . . . . . . . 9
β’ (πΉ β (π[,)+β)) β ran πΉ |
108 | 15 | frnd 6682 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β ran
πΉ β
β) |
109 | 107, 108 | sstrid 3959 |
. . . . . . . 8
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (πΉ β (π[,)+β)) β
β) |
110 | 109, 16 | sstrdi 3960 |
. . . . . . 7
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (πΉ β (π[,)+β)) β
β*) |
111 | | df-ss 3931 |
. . . . . . 7
β’ ((πΉ β (π[,)+β)) β β*
β ((πΉ β (π[,)+β)) β©
β*) = (πΉ
β (π[,)+β))) |
112 | 110, 111 | sylib 217 |
. . . . . 6
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β ((πΉ β (π[,)+β)) β© β*) =
(πΉ β (π[,)+β))) |
113 | 112, 109 | eqsstrd 3986 |
. . . . 5
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β ((πΉ β (π[,)+β)) β© β*)
β β) |
114 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β
β€) |
115 | | flcl 13711 |
. . . . . . . . . . . . . 14
β’ (π β β β
(ββπ) β
β€) |
116 | 115 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
(ββπ) β
β€) |
117 | 116 | peano2zd 12620 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
((ββπ) + 1)
β β€) |
118 | 117, 114 | ifcld 4538 |
. . . . . . . . . . 11
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β β€) |
119 | 114 | zred 12617 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β
β) |
120 | 117 | zred 12617 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
((ββπ) + 1)
β β) |
121 | | max1 13115 |
. . . . . . . . . . . 12
β’ ((π β β β§
((ββπ) + 1)
β β) β π
β€ if(π β€
((ββπ) + 1),
((ββπ) + 1),
π)) |
122 | 119, 120,
121 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β€ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π)) |
123 | | eluz2 12779 |
. . . . . . . . . . 11
β’ (if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β (β€β₯βπ) β (π β β€ β§ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β β€ β§ π β€ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π))) |
124 | 114, 118,
122, 123 | syl3anbrc 1344 |
. . . . . . . . . 10
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β (β€β₯βπ)) |
125 | 124, 9 | eleqtrrdi 2844 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β π) |
126 | 15 | fdmd 6685 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β dom
πΉ = π) |
127 | 125, 126 | eleqtrrd 2836 |
. . . . . . . 8
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β dom πΉ) |
128 | 118 | zred 12617 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β β) |
129 | | fllep1 13717 |
. . . . . . . . . . 11
β’ (π β β β π β€ ((ββπ) + 1)) |
130 | 129 | adantl 483 |
. . . . . . . . . 10
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β€ ((ββπ) + 1)) |
131 | | max2 13117 |
. . . . . . . . . . 11
β’ ((π β β β§
((ββπ) + 1)
β β) β ((ββπ) + 1) β€ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π)) |
132 | 119, 120,
131 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
((ββπ) + 1)
β€ if(π β€
((ββπ) + 1),
((ββπ) + 1),
π)) |
133 | 33, 120, 128, 130, 132 | letrd 11322 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β π β€ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π)) |
134 | | elicopnf 13373 |
. . . . . . . . . 10
β’ (π β β β (if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β (π[,)+β) β (if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β β β§ π β€ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π)))) |
135 | 134 | adantl 483 |
. . . . . . . . 9
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
(if(π β€
((ββπ) + 1),
((ββπ) + 1),
π) β (π[,)+β) β (if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β β β§ π β€ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π)))) |
136 | 128, 133,
135 | mpbir2and 712 |
. . . . . . . 8
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β (π[,)+β)) |
137 | | inelcm 4430 |
. . . . . . . 8
β’
((if(π β€
((ββπ) + 1),
((ββπ) + 1),
π) β dom πΉ β§ if(π β€ ((ββπ) + 1), ((ββπ) + 1), π) β (π[,)+β)) β (dom πΉ β© (π[,)+β)) β β
) |
138 | 127, 136,
137 | syl2anc 585 |
. . . . . . 7
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (dom
πΉ β© (π[,)+β)) β β
) |
139 | | imadisj 6038 |
. . . . . . . 8
β’ ((πΉ β (π[,)+β)) = β
β (dom πΉ β© (π[,)+β)) = β
) |
140 | 139 | necon3bii 2993 |
. . . . . . 7
β’ ((πΉ β (π[,)+β)) β β
β (dom πΉ β© (π[,)+β)) β β
) |
141 | 138, 140 | sylibr 233 |
. . . . . 6
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (πΉ β (π[,)+β)) β β
) |
142 | 112, 141 | eqnetrd 3008 |
. . . . 5
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β ((πΉ β (π[,)+β)) β© β*) β
β
) |
143 | | supxrre1 13260 |
. . . . 5
β’ ((((πΉ β (π[,)+β)) β© β*)
β β β§ ((πΉ
β (π[,)+β))
β© β*) β β
) β (sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < +β)) |
144 | 113, 142,
143 | syl2anc 585 |
. . . 4
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
(sup(((πΉ β (π[,)+β)) β©
β*), β*, < ) β β β
sup(((πΉ β (π[,)+β)) β©
β*), β*, < ) <
+β)) |
145 | 106, 144 | mpbird 257 |
. . 3
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β
sup(((πΉ β (π[,)+β)) β©
β*), β*, < ) β
β) |
146 | 7, 145 | eqeltrd 2833 |
. 2
β’ (((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β§ π β β) β (πΊβπ) β β) |
147 | 3, 5, 146 | fmpt2d 7077 |
1
β’ ((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β πΊ:ββΆβ) |