Metamath Proof Explorer

Theorem neglimc

Description: Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses neglimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
neglimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
neglimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
neglimc.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) )
Assertion neglimc ( 𝜑 → - 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 neglimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 neglimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
3 neglimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 neglimc.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) )
5 limccl ⊢ ( 𝐹 limℂ 𝐷 ) ⊆ ℂ
6 5 4 sselid ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
7 6 negcld ⊢ ( 𝜑 → - 𝐶 ∈ ℂ )
8 3 1 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
9 1 3 4 limcmptdm ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
10 limcrcl ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
11 4 10 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
12 11 simp3d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
13 8 9 12 ellimc3 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ) ) )
14 4 13 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ) )
15 14 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) )
16 15 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) )
17 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) → 𝜑 )
18 17 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) ) → 𝜑 )
19 simp1r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) ) → 𝑣 ∈ 𝐴 )
20 simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) ) → ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) )
21 simp2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) ) → ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) )
22 20 21 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 )
23 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑣 ∈ 𝐴 )
24 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
25 2 24 nfcxfr ⊢ Ⅎ 𝑥 𝐺
26 nfcv ⊢ Ⅎ 𝑥 𝑣
27 25 26 nffv ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑣 )
28 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
29 1 28 nfcxfr ⊢ Ⅎ 𝑥 𝐹
30 29 26 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑣 )
31 30 nfneg ⊢ Ⅎ 𝑥 - ( 𝐹 ‘ 𝑣 )
32 27 31 nfeq ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 )
33 23 32 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 ) )
34 eleq1w ⊢ ( 𝑥 = 𝑣 → ( 𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴 ) )
35 34 anbi2d ⊢ ( 𝑥 = 𝑣 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ) )
36 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑣 ) )
37 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
38 37 negeqd ⊢ ( 𝑥 = 𝑣 → - ( 𝐹 ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑣 ) )
39 36 38 eqeq12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐺 ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 ) ) )
40 35 39 imbi12d ⊢ ( 𝑥 = 𝑣 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 ) ) ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
42 3 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℂ )
43 2 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ - 𝐵 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = - 𝐵 )
44 41 42 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = - 𝐵 )
45 1 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
46 41 3 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
47 46 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( 𝐹 ‘ 𝑥 ) = - 𝐵 )
48 44 47 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) )
49 33 40 48 chvarfv ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 ) )
50 49 oveq1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) = ( - ( 𝐹 ‘ 𝑣 ) − - 𝐶 ) )
51 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ ℂ )
52 6 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
53 51 52 negsubdi3d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → - ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) = ( - ( 𝐹 ‘ 𝑣 ) − - 𝐶 ) )
54 50 53 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) = - ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) )
55 54 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) = ( abs ‘ - ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) )
56 51 52 subcld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ∈ ℂ )
57 56 absnegd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ - ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) )
58 55 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 )
61 59 60 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 )
62 18 19 22 61 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 )
63 62 3exp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) → ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 ) ) )
64 63 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 ) ) )
65 64 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐶 ) ) < 𝑦 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 ) ) )
66 16 65 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 ) )
67 66 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 ) )
68 42 2 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
69 68 9 12 ellimc3 ⊢ ( 𝜑 → ( - 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) ↔ ( - 𝐶 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − - 𝐶 ) ) < 𝑦 ) ) ) )
70 7 67 69 mpbir2and ⊢ ( 𝜑 → - 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) )