Metamath Proof Explorer

Theorem rlimmulOLD

Description: Obsolete version of rlimmul as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses rlimadd.3 ⊢ φ ∧ x ∈ A → B ∈ V
rlimadd.4 ⊢ φ ∧ x ∈ A → C ∈ V
rlimadd.5 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
rlimadd.6 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
Assertion rlimmulOLD ⊢ φ → x ∈ A ⟼ B ⁢ C ⇝ℝ D ⁢ E

Proof

Step Hyp Ref Expression
1 rlimadd.3 ⊢ φ ∧ x ∈ A → B ∈ V
2 rlimadd.4 ⊢ φ ∧ x ∈ A → C ∈ V
3 rlimadd.5 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
4 rlimadd.6 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
5 1 3 rlimmptrcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
6 2 4 rlimmptrcl ⊢ φ ∧ x ∈ A → C ∈ ℂ
7 rlimcl ⊢ x ∈ A ⟼ B ⇝ℝ D → D ∈ ℂ
8 3 7 syl ⊢ φ → D ∈ ℂ
9 rlimcl ⊢ x ∈ A ⟼ C ⇝ℝ E → E ∈ ℂ
10 4 9 syl ⊢ φ → E ∈ ℂ
11 ax-mulf ⊢ × : ℂ × ℂ ⟶ ℂ
12 11 a1i ⊢ φ → × : ℂ × ℂ ⟶ ℂ
13 simpr ⊢ φ ∧ y ∈ ℝ + → y ∈ ℝ +
14 8 adantr ⊢ φ ∧ y ∈ ℝ + → D ∈ ℂ
15 10 adantr ⊢ φ ∧ y ∈ ℝ + → E ∈ ℂ
16 mulcn2 ⊢ y ∈ ℝ + ∧ D ∈ ℂ ∧ E ∈ ℂ → ∃ z ∈ ℝ + ∃ w ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − D < z ∧ v − E < w → u ⁢ v − D ⁢ E < y
17 13 14 15 16 syl3anc ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ ℝ + ∃ w ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − D < z ∧ v − E < w → u ⁢ v − D ⁢ E < y
18 5 6 8 10 3 4 12 17 rlimcn2 ⊢ φ → x ∈ A ⟼ B ⁢ C ⇝ℝ D ⁢ E