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 ‘ ( 𝐵𝐶 ) ) < 𝑥 ) ) )