Metamath Proof Explorer

Theorem rlim0

Description: Express the predicate B ( z ) converges to 0 . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

Ref Expression
Hypotheses rlim0.1 ⊢φ→∀z∈AB∈ℂ
rlim0.2 ⊢φ→A⊆ℝ
Assertion rlim0 ⊢φ→z∈A⟼B⇝ℝ0↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B<x

Proof

Step Hyp Ref Expression
1 rlim0.1 ⊢φ→∀z∈AB∈ℂ
2 rlim0.2 ⊢φ→A⊆ℝ
3 0cnd ⊢φ→0∈ℂ
4 1 2 3 rlim2 ⊢φ→z∈A⟼B⇝ℝ0↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B−0<x
5 subid1 ⊢B∈ℂ→B−0=B
6 5 fveq2d ⊢B∈ℂ→B−0=B
7 6 breq1d ⊢B∈ℂ→B−0<x↔B<x
8 7 imbi2d ⊢B∈ℂ→y≤z→B−0<x↔y≤z→B<x
9 8 ralimi ⊢∀z∈AB∈ℂ→∀z∈Ay≤z→B−0<x↔y≤z→B<x
10 ralbi ⊢∀z∈Ay≤z→B−0<x↔y≤z→B<x→∀z∈Ay≤z→B−0<x↔∀z∈Ay≤z→B<x
11 1 9 10 3syl ⊢φ→∀z∈Ay≤z→B−0<x↔∀z∈Ay≤z→B<x
12 11 rexbidv ⊢φ→∃y∈ℝ∀z∈Ay≤z→B−0<x↔∃y∈ℝ∀z∈Ay≤z→B<x
13 12 ralbidv ⊢φ→∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B−0<x↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B<x
14 4 13 bitrd ⊢φ→z∈A⟼B⇝ℝ0↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B<x