Metamath Proof Explorer

Theorem divlimc

Description: Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses divlimc.f ⊢ F = x ∈ A ⟼ B
divlimc.g ⊢ G = x ∈ A ⟼ C
divlimc.h ⊢ H = x ∈ A ⟼ B C
divlimc.b ⊢ φ ∧ x ∈ A → B ∈ ℂ
divlimc.c ⊢ φ ∧ x ∈ A → C ∈ ℂ ∖ 0
divlimc.x ⊢ φ → X ∈ F lim ℂ D
divlimc.y ⊢ φ → Y ∈ G lim ℂ D
divlimc.yne0 ⊢ φ → Y ≠ 0
divlimc.cne0 ⊢ φ ∧ x ∈ A → C ≠ 0
Assertion divlimc ⊢ φ → X Y ∈ H lim ℂ D

Proof

Step Hyp Ref Expression
1 divlimc.f ⊢ F = x ∈ A ⟼ B
2 divlimc.g ⊢ G = x ∈ A ⟼ C
3 divlimc.h ⊢ H = x ∈ A ⟼ B C
4 divlimc.b ⊢ φ ∧ x ∈ A → B ∈ ℂ
5 divlimc.c ⊢ φ ∧ x ∈ A → C ∈ ℂ ∖ 0
6 divlimc.x ⊢ φ → X ∈ F lim ℂ D
7 divlimc.y ⊢ φ → Y ∈ G lim ℂ D
8 divlimc.yne0 ⊢ φ → Y ≠ 0
9 divlimc.cne0 ⊢ φ ∧ x ∈ A → C ≠ 0
10 eqid ⊢ x ∈ A ⟼ 1 C = x ∈ A ⟼ 1 C
11 eqid ⊢ x ∈ A ⟼ B ⁢ 1 C = x ∈ A ⟼ B ⁢ 1 C
12 5 eldifad ⊢ φ ∧ x ∈ A → C ∈ ℂ
13 12 9 reccld ⊢ φ ∧ x ∈ A → 1 C ∈ ℂ
14 2 10 5 7 8 reclimc ⊢ φ → 1 Y ∈ x ∈ A ⟼ 1 C lim ℂ D
15 1 10 11 4 13 6 14 mullimc ⊢ φ → X ⁢ 1 Y ∈ x ∈ A ⟼ B ⁢ 1 C lim ℂ D
16 limccl ⊢ F lim ℂ D ⊆ ℂ
17 16 6 sselid ⊢ φ → X ∈ ℂ
18 limccl ⊢ G lim ℂ D ⊆ ℂ
19 18 7 sselid ⊢ φ → Y ∈ ℂ
20 17 19 8 divrecd ⊢ φ → X Y = X ⁢ 1 Y
21 4 12 9 divrecd ⊢ φ ∧ x ∈ A → B C = B ⁢ 1 C
22 21 mpteq2dva ⊢ φ → x ∈ A ⟼ B C = x ∈ A ⟼ B ⁢ 1 C
23 3 22 syl5eq ⊢ φ → H = x ∈ A ⟼ B ⁢ 1 C
24 23 oveq1d ⊢ φ → H lim ℂ D = x ∈ A ⟼ B ⁢ 1 C lim ℂ D
25 15 20 24 3eltr4d ⊢ φ → X Y ∈ H lim ℂ D