Metamath Proof Explorer

Theorem rlimeq

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimeq.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
rlimeq.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
rlimeq.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
rlimeq.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 = 𝐶 )
Assertion rlimeq ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ) )

Proof

Step Hyp Ref Expression
1 rlimeq.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
2 rlimeq.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
3 rlimeq.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
4 rlimeq.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 = 𝐶 )
5 rlimss ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 6 1 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
8 7 sseq1d ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
9 5 8 syl5ib ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 → 𝐴 ⊆ ℝ ) )
10 rlimss ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ℝ )
11 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
12 11 2 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = 𝐴 )
13 12 sseq1d ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
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 breq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) ⇝𝑟 𝐸 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) ⇝𝑟 𝐸 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) ⇝𝑟 𝐸 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) ⇝𝑟 𝐸 ) )
47 1 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
49 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
50 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝐷 ∈ ℝ )
51 48 49 50 rlimresb ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) ⇝𝑟 𝐸 ) )
52 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
54 53 49 50 rlimresb ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) ⇝𝑟 𝐸 ) )
55 46 51 54 3bitr4d ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ) )
56 55 ex ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ) ) )
57 9 14 56 pm5.21ndd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐸 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ) )