# Metamath Proof Explorer

## Theorem rlim2lt

Description: Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Hypotheses rlim2.1 ${⊢}{\phi }\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
rlim2.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
rlim2.3 ${⊢}{\phi }\to {C}\in ℂ$
Assertion rlim2lt

### Proof

Step Hyp Ref Expression
1 rlim2.1 ${⊢}{\phi }\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
2 rlim2.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
3 rlim2.3 ${⊢}{\phi }\to {C}\in ℂ$
4 1 2 3 rlim2
5 simplr ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to {y}\in ℝ$
6 simpl ${⊢}\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\to {A}\subseteq ℝ$
7 6 sselda ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to {z}\in ℝ$
8 ltle ${⊢}\left({y}\in ℝ\wedge {z}\in ℝ\right)\to \left({y}<{z}\to {y}\le {z}\right)$
9 5 7 8 syl2anc ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to \left({y}<{z}\to {y}\le {z}\right)$
10 9 imim1d ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to \left(\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\to \left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\right)$
11 10 ralimdva ${⊢}\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\right)$
12 2 11 sylan ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\right)$
13 12 reximdva ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\right)$
14 13 ralimdv ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\right)$
15 4 14 sylbid
16 peano2re ${⊢}{y}\in ℝ\to {y}+1\in ℝ$
17 16 adantl ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to {y}+1\in ℝ$
18 ltp1 ${⊢}{y}\in ℝ\to {y}<{y}+1$
19 18 ad2antlr ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to {y}<{y}+1$
20 16 ad2antlr ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to {y}+1\in ℝ$
21 ltletr ${⊢}\left({y}\in ℝ\wedge {y}+1\in ℝ\wedge {z}\in ℝ\right)\to \left(\left({y}<{y}+1\wedge {y}+1\le {z}\right)\to {y}<{z}\right)$
22 5 20 7 21 syl3anc ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to \left(\left({y}<{y}+1\wedge {y}+1\le {z}\right)\to {y}<{z}\right)$
23 19 22 mpand ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to \left({y}+1\le {z}\to {y}<{z}\right)$
24 23 imim1d ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to \left(\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\to \left({y}+1\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
25 24 ralimdva ${⊢}\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}+1\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
26 2 25 sylan ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}+1\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
27 breq1 ${⊢}{w}={y}+1\to \left({w}\le {z}↔{y}+1\le {z}\right)$
28 27 rspceaimv ${⊢}\left({y}+1\in ℝ\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}+1\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\le {z}\to \left|{B}-{C}\right|<{x}\right)$
29 17 26 28 syl6an ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
30 29 rexlimdva ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
31 30 ralimdv ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{z}\to \left|{B}-{C}\right|<{x}\right)\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
32 1 2 3 rlim2
33 31 32 sylibrd
34 15 33 impbid