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 ⊢φ→∀z∈AB∈ℂ
rlim2.2 ⊢φ→A⊆ℝ
rlim2.3 ⊢φ→C∈ℂ
Assertion rlim2lt ⊢φ→z∈A⟼B⇝ℝC↔∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−C<x

Proof

Step Hyp Ref Expression
1 rlim2.1 ⊢φ→∀z∈AB∈ℂ
2 rlim2.2 ⊢φ→A⊆ℝ
3 rlim2.3 ⊢φ→C∈ℂ
4 1 2 3 rlim2 ⊢φ→z∈A⟼B⇝ℝC↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B−C<x
5 simplr ⊢A⊆ℝ∧y∈ℝ∧z∈A→y∈ℝ
6 simpl ⊢A⊆ℝ∧y∈ℝ→A⊆ℝ
7 6 sselda ⊢A⊆ℝ∧y∈ℝ∧z∈A→z∈ℝ
8 ltle ⊢y∈ℝ∧z∈ℝ→y<z→y≤z
9 5 7 8 syl2anc ⊢A⊆ℝ∧y∈ℝ∧z∈A→y<z→y≤z
10 9 imim1d ⊢A⊆ℝ∧y∈ℝ∧z∈A→y≤z→B−C<x→y<z→B−C<x
11 10 ralimdva ⊢A⊆ℝ∧y∈ℝ→∀z∈Ay≤z→B−C<x→∀z∈Ay<z→B−C<x
12 2 11 sylan ⊢φ∧y∈ℝ→∀z∈Ay≤z→B−C<x→∀z∈Ay<z→B−C<x
13 12 reximdva ⊢φ→∃y∈ℝ∀z∈Ay≤z→B−C<x→∃y∈ℝ∀z∈Ay<z→B−C<x
14 13 ralimdv ⊢φ→∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B−C<x→∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−C<x
15 4 14 sylbid ⊢φ→z∈A⟼B⇝ℝC→∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−C<x
16 peano2re ⊢y∈ℝ→y+1∈ℝ
17 16 adantl ⊢φ∧y∈ℝ→y+1∈ℝ
18 ltp1 ⊢y∈ℝ→y<y+1
19 18 ad2antlr ⊢A⊆ℝ∧y∈ℝ∧z∈A→y<y+1
20 16 ad2antlr ⊢A⊆ℝ∧y∈ℝ∧z∈A→y+1∈ℝ
21 ltletr ⊢y∈ℝ∧y+1∈ℝ∧z∈ℝ→y<y+1∧y+1≤z→y<z
22 5 20 7 21 syl3anc ⊢A⊆ℝ∧y∈ℝ∧z∈A→y<y+1∧y+1≤z→y<z
23 19 22 mpand ⊢A⊆ℝ∧y∈ℝ∧z∈A→y+1≤z→y<z
24 23 imim1d ⊢A⊆ℝ∧y∈ℝ∧z∈A→y<z→B−C<x→y+1≤z→B−C<x
25 24 ralimdva ⊢A⊆ℝ∧y∈ℝ→∀z∈Ay<z→B−C<x→∀z∈Ay+1≤z→B−C<x
26 2 25 sylan ⊢φ∧y∈ℝ→∀z∈Ay<z→B−C<x→∀z∈Ay+1≤z→B−C<x
27 breq1 ⊢w=y+1→w≤z↔y+1≤z
28 27 rspceaimv ⊢y+1∈ℝ∧∀z∈Ay+1≤z→B−C<x→∃w∈ℝ∀z∈Aw≤z→B−C<x
29 17 26 28 syl6an ⊢φ∧y∈ℝ→∀z∈Ay<z→B−C<x→∃w∈ℝ∀z∈Aw≤z→B−C<x
30 29 rexlimdva ⊢φ→∃y∈ℝ∀z∈Ay<z→B−C<x→∃w∈ℝ∀z∈Aw≤z→B−C<x
31 30 ralimdv ⊢φ→∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−C<x→∀x∈ℝ+∃w∈ℝ∀z∈Aw≤z→B−C<x
32 1 2 3 rlim2 ⊢φ→z∈A⟼B⇝ℝC↔∀x∈ℝ+∃w∈ℝ∀z∈Aw≤z→B−C<x
33 31 32 sylibrd ⊢φ→∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−C<x→z∈A⟼B⇝ℝC
34 15 33 impbid ⊢φ→z∈A⟼B⇝ℝC↔∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−C<x