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 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
rlim2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
rlim2.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion rlim2lt ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 rlim2.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
2 rlim2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 rlim2.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 1 2 3 rlim2 ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
5 simplr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
6 simpl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → 𝐴 ⊆ ℝ )
7 6 sselda ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
8 ltle ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 < 𝑧 → 𝑦 ≤ 𝑧 ) )
9 5 7 8 syl2anc ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 < 𝑧 → 𝑦 ≤ 𝑧 ) )
10 9 imim1d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
11 10 ralimdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
12 2 11 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
13 12 reximdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
14 13 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
15 4 14 sylbid ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
16 peano2re ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 1 ) ∈ ℝ )
18 ltp1 ⊢ ( 𝑦 ∈ ℝ → 𝑦 < ( 𝑦 + 1 ) )
19 18 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 < ( 𝑦 + 1 ) )
20 16 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 + 1 ) ∈ ℝ )
21 ltletr ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) )
22 5 20 7 21 syl3anc ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) )
23 19 22 mpand ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → 𝑦 < 𝑧 ) )
24 23 imim1d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
25 24 ralimdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
26 2 25 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
27 breq1 ⊢ ( 𝑤 = ( 𝑦 + 1 ) → ( 𝑤 ≤ 𝑧 ↔ ( 𝑦 + 1 ) ≤ 𝑧 ) )
28 27 rspceaimv ⊢ ( ( ( 𝑦 + 1 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) )
29 17 26 28 syl6an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
30 29 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
31 30 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
32 1 2 3 rlim2 ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
33 31 32 sylibrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ) )
34 15 33 impbid ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )