Step | Hyp | Ref
| Expression |
1 | | climinf.5 |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ) |
2 | 1 | frnd 6677 |
. . . . . . . . . . 11
β’ (π β ran πΉ β β) |
3 | 1 | ffnd 6670 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn π) |
4 | | climinf.4 |
. . . . . . . . . . . . . . 15
β’ (π β π β β€) |
5 | | uzid 12779 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β π β
(β€β₯βπ)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β (β€β₯βπ)) |
7 | | climinf.3 |
. . . . . . . . . . . . . 14
β’ π =
(β€β₯βπ) |
8 | 6, 7 | eleqtrrdi 2849 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
9 | | fnfvelrn 7032 |
. . . . . . . . . . . . 13
β’ ((πΉ Fn π β§ π β π) β (πΉβπ) β ran πΉ) |
10 | 3, 8, 9 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΉβπ) β ran πΉ) |
11 | 10 | ne0d 4296 |
. . . . . . . . . . 11
β’ (π β ran πΉ β β
) |
12 | | climinf.7 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) |
13 | | breq2 5110 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (πΉβπ) β (π₯ β€ π¦ β π₯ β€ (πΉβπ))) |
14 | 13 | ralrn 7039 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn π β (βπ¦ β ran πΉ π₯ β€ π¦ β βπ β π π₯ β€ (πΉβπ))) |
15 | 14 | rexbidv 3176 |
. . . . . . . . . . . . 13
β’ (πΉ Fn π β (βπ₯ β β βπ¦ β ran πΉ π₯ β€ π¦ β βπ₯ β β βπ β π π₯ β€ (πΉβπ))) |
16 | 3, 15 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (βπ₯ β β βπ¦ β ran πΉ π₯ β€ π¦ β βπ₯ β β βπ β π π₯ β€ (πΉβπ))) |
17 | 12, 16 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β βπ¦ β ran πΉ π₯ β€ π¦) |
18 | 2, 11, 17 | 3jca 1129 |
. . . . . . . . . 10
β’ (π β (ran πΉ β β β§ ran πΉ β β
β§ βπ₯ β β βπ¦ β ran πΉ π₯ β€ π¦)) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β β+) β (ran
πΉ β β β§ ran
πΉ β β
β§
βπ₯ β β
βπ¦ β ran πΉ π₯ β€ π¦)) |
20 | | infrecl 12138 |
. . . . . . . . 9
β’ ((ran
πΉ β β β§ ran
πΉ β β
β§
βπ₯ β β
βπ¦ β ran πΉ π₯ β€ π¦) β inf(ran πΉ, β, < ) β
β) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β inf(ran
πΉ, β, < ) β
β) |
22 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β π¦ β
β+) |
23 | 21, 22 | ltaddrpd 12991 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β inf(ran
πΉ, β, < ) <
(inf(ran πΉ, β, < )
+ π¦)) |
24 | | rpre 12924 |
. . . . . . . . . 10
β’ (π¦ β β+
β π¦ β
β) |
25 | 24 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π¦ β β+) β π¦ β
β) |
26 | 21, 25 | readdcld 11185 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β (inf(ran
πΉ, β, < ) + π¦) β
β) |
27 | | infrglb 43838 |
. . . . . . . 8
β’ (((ran
πΉ β β β§ ran
πΉ β β
β§
βπ₯ β β
βπ¦ β ran πΉ π₯ β€ π¦) β§ (inf(ran πΉ, β, < ) + π¦) β β) β (inf(ran πΉ, β, < ) < (inf(ran
πΉ, β, < ) + π¦) β βπ β ran πΉ π < (inf(ran πΉ, β, < ) + π¦))) |
28 | 19, 26, 27 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β (inf(ran
πΉ, β, < ) <
(inf(ran πΉ, β, < )
+ π¦) β βπ β ran πΉ π < (inf(ran πΉ, β, < ) + π¦))) |
29 | 23, 28 | mpbid 231 |
. . . . . 6
β’ ((π β§ π¦ β β+) β
βπ β ran πΉ π < (inf(ran πΉ, β, < ) + π¦)) |
30 | 2 | sselda 3945 |
. . . . . . . . . . 11
β’ ((π β§ π β ran πΉ) β π β β) |
31 | 30 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β π β β) |
32 | 21 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β inf(ran πΉ, β, < ) β
β) |
33 | 24 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β π¦ β β) |
34 | 32, 33 | readdcld 11185 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β (inf(ran πΉ, β, < ) + π¦) β β) |
35 | 31, 34, 33 | ltsub1d 11765 |
. . . . . . . . 9
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β (π < (inf(ran πΉ, β, < ) + π¦) β (π β π¦) < ((inf(ran πΉ, β, < ) + π¦) β π¦))) |
36 | 2, 11, 17, 20 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β inf(ran πΉ, β, < ) β
β) |
37 | 36 | recnd 11184 |
. . . . . . . . . . . 12
β’ (π β inf(ran πΉ, β, < ) β
β) |
38 | 37 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β inf(ran πΉ, β, < ) β
β) |
39 | 33 | recnd 11184 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β π¦ β β) |
40 | 38, 39 | pncand 11514 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β ((inf(ran πΉ, β, < ) + π¦) β π¦) = inf(ran πΉ, β, < )) |
41 | 40 | breq2d 5118 |
. . . . . . . . 9
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β ((π β π¦) < ((inf(ran πΉ, β, < ) + π¦) β π¦) β (π β π¦) < inf(ran πΉ, β, < ))) |
42 | 35, 41 | bitrd 279 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β (π < (inf(ran πΉ, β, < ) + π¦) β (π β π¦) < inf(ran πΉ, β, < ))) |
43 | 42 | biimpd 228 |
. . . . . . 7
β’ (((π β§ π¦ β β+) β§ π β ran πΉ) β (π < (inf(ran πΉ, β, < ) + π¦) β (π β π¦) < inf(ran πΉ, β, < ))) |
44 | 43 | reximdva 3166 |
. . . . . 6
β’ ((π β§ π¦ β β+) β
(βπ β ran πΉ π < (inf(ran πΉ, β, < ) + π¦) β βπ β ran πΉ(π β π¦) < inf(ran πΉ, β, < ))) |
45 | 29, 44 | mpd 15 |
. . . . 5
β’ ((π β§ π¦ β β+) β
βπ β ran πΉ(π β π¦) < inf(ran πΉ, β, < )) |
46 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = (πΉβπ) β (π β π¦) = ((πΉβπ) β π¦)) |
47 | 46 | breq1d 5116 |
. . . . . . . 8
β’ (π = (πΉβπ) β ((π β π¦) < inf(ran πΉ, β, < ) β ((πΉβπ) β π¦) < inf(ran πΉ, β, < ))) |
48 | 47 | rexrn 7038 |
. . . . . . 7
β’ (πΉ Fn π β (βπ β ran πΉ(π β π¦) < inf(ran πΉ, β, < ) β βπ β π ((πΉβπ) β π¦) < inf(ran πΉ, β, < ))) |
49 | 3, 48 | syl 17 |
. . . . . 6
β’ (π β (βπ β ran πΉ(π β π¦) < inf(ran πΉ, β, < ) β βπ β π ((πΉβπ) β π¦) < inf(ran πΉ, β, < ))) |
50 | 49 | biimpa 478 |
. . . . 5
β’ ((π β§ βπ β ran πΉ(π β π¦) < inf(ran πΉ, β, < )) β βπ β π ((πΉβπ) β π¦) < inf(ran πΉ, β, < )) |
51 | 45, 50 | syldan 592 |
. . . 4
β’ ((π β§ π¦ β β+) β
βπ β π ((πΉβπ) β π¦) < inf(ran πΉ, β, < )) |
52 | 1 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β+) β πΉ:πβΆβ) |
53 | 7 | uztrn2 12783 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
54 | | ffvelcdm 7033 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆβ β§ π β π) β (πΉβπ) β β) |
55 | 52, 53, 54 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β β) |
56 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
57 | | ffvelcdm 7033 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆβ β§ π β π) β (πΉβπ) β β) |
58 | 52, 56, 57 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β β) |
59 | 36 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β inf(ran πΉ, β, < ) β
β) |
60 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
61 | | fzssuz 13483 |
. . . . . . . . . . . . . 14
β’ (π...π) β (β€β₯βπ) |
62 | | uzss 12787 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
63 | 62, 7 | sseqtrrdi 3996 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β π) |
64 | 63, 7 | eleq2s 2856 |
. . . . . . . . . . . . . . 15
β’ (π β π β (β€β₯βπ) β π) |
65 | 64 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β
(β€β₯βπ) β π) |
66 | 61, 65 | sstrid 3956 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (π...π) β π) |
67 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:πβΆβ β§ π β π) β (πΉβπ) β β) |
68 | 67 | ralrimiva 3144 |
. . . . . . . . . . . . . . 15
β’ (πΉ:πβΆβ β βπ β π (πΉβπ) β β) |
69 | 1, 68 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β βπ β π (πΉβπ) β β) |
70 | 69 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β βπ β π (πΉβπ) β β) |
71 | | ssralv 4011 |
. . . . . . . . . . . . 13
β’ ((π...π) β π β (βπ β π (πΉβπ) β β β βπ β (π...π)(πΉβπ) β β)) |
72 | 66, 70, 71 | sylc 65 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β βπ β (π...π)(πΉβπ) β β) |
73 | 72 | r19.21bi 3235 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΉβπ) β β) |
74 | | fzssuz 13483 |
. . . . . . . . . . . . . 14
β’ (π...(π β 1)) β
(β€β₯βπ) |
75 | 74, 65 | sstrid 3956 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (π...(π β 1)) β π) |
76 | 75 | sselda 3945 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β π β π) |
77 | | climinf.6 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) |
78 | 77 | ralrimiva 3144 |
. . . . . . . . . . . . . 14
β’ (π β βπ β π (πΉβ(π + 1)) β€ (πΉβπ)) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β βπ β π (πΉβ(π + 1)) β€ (πΉβπ)) |
80 | | fvoveq1 7381 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
81 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
82 | 80, 81 | breq12d 5119 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβ(π + 1)) β€ (πΉβπ) β (πΉβ(π + 1)) β€ (πΉβπ))) |
83 | 82 | rspccva 3581 |
. . . . . . . . . . . . 13
β’
((βπ β
π (πΉβ(π + 1)) β€ (πΉβπ) β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) |
84 | 79, 83 | sylan 581 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) |
85 | 76, 84 | syldan 592 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
86 | 60, 73, 85 | monoord2 13940 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β€ (πΉβπ)) |
87 | 55, 58, 59, 86 | lesub1dd 11772 |
. . . . . . . . 9
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β ((πΉβπ) β inf(ran πΉ, β, < )) β€ ((πΉβπ) β inf(ran πΉ, β, < ))) |
88 | 55, 59 | resubcld 11584 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β ((πΉβπ) β inf(ran πΉ, β, < )) β
β) |
89 | 58, 59 | resubcld 11584 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β ((πΉβπ) β inf(ran πΉ, β, < )) β
β) |
90 | 24 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β π¦ β β) |
91 | | lelttr 11246 |
. . . . . . . . . 10
β’ ((((πΉβπ) β inf(ran πΉ, β, < )) β β β§
((πΉβπ) β inf(ran πΉ, β, < )) β
β β§ π¦ β
β) β ((((πΉβπ) β inf(ran πΉ, β, < )) β€ ((πΉβπ) β inf(ran πΉ, β, < )) β§ ((πΉβπ) β inf(ran πΉ, β, < )) < π¦) β ((πΉβπ) β inf(ran πΉ, β, < )) < π¦)) |
92 | 88, 89, 90, 91 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β ((((πΉβπ) β inf(ran πΉ, β, < )) β€ ((πΉβπ) β inf(ran πΉ, β, < )) β§ ((πΉβπ) β inf(ran πΉ, β, < )) < π¦) β ((πΉβπ) β inf(ran πΉ, β, < )) < π¦)) |
93 | 87, 92 | mpand 694 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (((πΉβπ) β inf(ran πΉ, β, < )) < π¦ β ((πΉβπ) β inf(ran πΉ, β, < )) < π¦)) |
94 | | ltsub23 11636 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ π¦ β β β§ inf(ran πΉ, β, < ) β
β) β (((πΉβπ) β π¦) < inf(ran πΉ, β, < ) β ((πΉβπ) β inf(ran πΉ, β, < )) < π¦)) |
95 | 58, 90, 59, 94 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (((πΉβπ) β π¦) < inf(ran πΉ, β, < ) β ((πΉβπ) β inf(ran πΉ, β, < )) < π¦)) |
96 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β ran πΉ β β) |
97 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β+) β πΉ Fn π) |
98 | | fnfvelrn 7032 |
. . . . . . . . . . . 12
β’ ((πΉ Fn π β§ π β π) β (πΉβπ) β ran πΉ) |
99 | 97, 53, 98 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β ran πΉ) |
100 | 96, 99 | sseldd 3946 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β β) |
101 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β βπ₯ β β βπ¦ β ran πΉ π₯ β€ π¦) |
102 | | infrelb 12141 |
. . . . . . . . . . 11
β’ ((ran
πΉ β β β§
βπ₯ β β
βπ¦ β ran πΉ π₯ β€ π¦ β§ (πΉβπ) β ran πΉ) β inf(ran πΉ, β, < ) β€ (πΉβπ)) |
103 | 96, 101, 99, 102 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β inf(ran πΉ, β, < ) β€ (πΉβπ)) |
104 | 59, 100, 103 | abssubge0d 15317 |
. . . . . . . . 9
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (absβ((πΉβπ) β inf(ran πΉ, β, < ))) = ((πΉβπ) β inf(ran πΉ, β, < ))) |
105 | 104 | breq1d 5116 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β ((absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦ β ((πΉβπ) β inf(ran πΉ, β, < )) < π¦)) |
106 | 93, 95, 105 | 3imtr4d 294 |
. . . . . . 7
β’ (((π β§ π¦ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (((πΉβπ) β π¦) < inf(ran πΉ, β, < ) β (absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦)) |
107 | 106 | anassrs 469 |
. . . . . 6
β’ ((((π β§ π¦ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (((πΉβπ) β π¦) < inf(ran πΉ, β, < ) β (absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦)) |
108 | 107 | ralrimdva 3152 |
. . . . 5
β’ (((π β§ π¦ β β+) β§ π β π) β (((πΉβπ) β π¦) < inf(ran πΉ, β, < ) β βπ β
(β€β₯βπ)(absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦)) |
109 | 108 | reximdva 3166 |
. . . 4
β’ ((π β§ π¦ β β+) β
(βπ β π ((πΉβπ) β π¦) < inf(ran πΉ, β, < ) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦)) |
110 | 51, 109 | mpd 15 |
. . 3
β’ ((π β§ π¦ β β+) β
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦) |
111 | 110 | ralrimiva 3144 |
. 2
β’ (π β βπ¦ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦) |
112 | 7 | fvexi 6857 |
. . . 4
β’ π β V |
113 | | fex 7177 |
. . . 4
β’ ((πΉ:πβΆβ β§ π β V) β πΉ β V) |
114 | 1, 112, 113 | sylancl 587 |
. . 3
β’ (π β πΉ β V) |
115 | | eqidd 2738 |
. . 3
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
116 | 1 | ffvelcdmda 7036 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
117 | 116 | recnd 11184 |
. . 3
β’ ((π β§ π β π) β (πΉβπ) β β) |
118 | 7, 4, 114, 115, 37, 117 | clim2c 15388 |
. 2
β’ (π β (πΉ β inf(ran πΉ, β, < ) β βπ¦ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β inf(ran πΉ, β, < ))) < π¦)) |
119 | 111, 118 | mpbird 257 |
1
β’ (π β πΉ β inf(ran πΉ, β, < )) |