Metamath Proof Explorer


Theorem lo1eq

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 φxAB
lo1eq.2 φxAC
lo1eq.3 φD
lo1eq.4 φxADxB=C
Assertion lo1eq φxAB𝑂1xAC𝑂1

Proof

Step Hyp Ref Expression
1 lo1eq.1 φxAB
2 lo1eq.2 φxAC
3 lo1eq.3 φD
4 lo1eq.4 φxADxB=C
5 lo1dm xAB𝑂1domxAB
6 eqid xAB=xAB
7 6 1 dmmptd φdomxAB=A
8 7 sseq1d φdomxABA
9 5 8 syl5ib φxAB𝑂1A
10 lo1dm xAC𝑂1domxAC
11 eqid xAC=xAC
12 11 2 dmmptd φdomxAC=A
13 12 sseq1d φdomxACA
14 10 13 syl5ib φxAC𝑂1A
15 simpr φxAD+∞xAD+∞
16 elin xAD+∞xAxD+∞
17 15 16 sylib φxAD+∞xAxD+∞
18 17 simpld φxAD+∞xA
19 17 simprd φxAD+∞xD+∞
20 elicopnf DxD+∞xDx
21 3 20 syl φxD+∞xDx
22 21 biimpa φxD+∞xDx
23 19 22 syldan φxAD+∞xDx
24 23 simprd φxAD+∞Dx
25 18 24 jca φxAD+∞xADx
26 25 4 syldan φxAD+∞B=C
27 26 mpteq2dva φxAD+∞B=xAD+∞C
28 inss1 AD+∞A
29 resmpt AD+∞AxABAD+∞=xAD+∞B
30 28 29 ax-mp xABAD+∞=xAD+∞B
31 resmpt AD+∞AxACAD+∞=xAD+∞C
32 28 31 ax-mp xACAD+∞=xAD+∞C
33 27 30 32 3eqtr4g φxABAD+∞=xACAD+∞
34 resres xABAD+∞=xABAD+∞
35 resres xACAD+∞=xACAD+∞
36 33 34 35 3eqtr4g φxABAD+∞=xACAD+∞
37 ssid AA
38 resmpt AAxABA=xAB
39 reseq1 xABA=xABxABAD+∞=xABD+∞
40 37 38 39 mp2b xABAD+∞=xABD+∞
41 resmpt AAxACA=xAC
42 reseq1 xACA=xACxACAD+∞=xACD+∞
43 37 41 42 mp2b xACAD+∞=xACD+∞
44 36 40 43 3eqtr3g φxABD+∞=xACD+∞
45 44 eleq1d φxABD+∞𝑂1xACD+∞𝑂1
46 45 adantr φAxABD+∞𝑂1xACD+∞𝑂1
47 1 fmpttd φxAB:A
48 47 adantr φAxAB:A
49 simpr φAA
50 3 adantr φAD
51 48 49 50 lo1resb φAxAB𝑂1xABD+∞𝑂1
52 2 fmpttd φxAC:A
53 52 adantr φAxAC:A
54 53 49 50 lo1resb φAxAC𝑂1xACD+∞𝑂1
55 46 51 54 3bitr4d φAxAB𝑂1xAC𝑂1
56 55 ex φAxAB𝑂1xAC𝑂1
57 9 14 56 pm5.21ndd φxAB𝑂1xAC𝑂1