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