Description: Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lo1eq.1 | |
|
lo1eq.2 | |
||
lo1eq.3 | |
||
lo1eq.4 | |
||
Assertion | lo1eq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lo1eq.1 | |
|
2 | lo1eq.2 | |
|
3 | lo1eq.3 | |
|
4 | lo1eq.4 | |
|
5 | lo1dm | |
|
6 | eqid | |
|
7 | 6 1 | dmmptd | |
8 | 7 | sseq1d | |
9 | 5 8 | syl5ib | |
10 | lo1dm | |
|
11 | eqid | |
|
12 | 11 2 | dmmptd | |
13 | 12 | sseq1d | |
14 | 10 13 | syl5ib | |
15 | simpr | |
|
16 | elin | |
|
17 | 15 16 | sylib | |
18 | 17 | simpld | |
19 | 17 | simprd | |
20 | elicopnf | |
|
21 | 3 20 | syl | |
22 | 21 | biimpa | |
23 | 19 22 | syldan | |
24 | 23 | simprd | |
25 | 18 24 | jca | |
26 | 25 4 | syldan | |
27 | 26 | mpteq2dva | |
28 | inss1 | |
|
29 | resmpt | |
|
30 | 28 29 | ax-mp | |
31 | resmpt | |
|
32 | 28 31 | ax-mp | |
33 | 27 30 32 | 3eqtr4g | |
34 | resres | |
|
35 | resres | |
|
36 | 33 34 35 | 3eqtr4g | |
37 | ssid | |
|
38 | resmpt | |
|
39 | reseq1 | |
|
40 | 37 38 39 | mp2b | |
41 | resmpt | |
|
42 | reseq1 | |
|
43 | 37 41 42 | mp2b | |
44 | 36 40 43 | 3eqtr3g | |
45 | 44 | eleq1d | |
46 | 45 | adantr | |
47 | 1 | fmpttd | |
48 | 47 | adantr | |
49 | simpr | |
|
50 | 3 | adantr | |
51 | 48 49 50 | lo1resb | |
52 | 2 | fmpttd | |
53 | 52 | adantr | |
54 | 53 49 50 | lo1resb | |
55 | 46 51 54 | 3bitr4d | |
56 | 55 | ex | |
57 | 9 14 56 | pm5.21ndd | |