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 ( 𝜑 → ∀ 𝑧𝐴 𝐵 ∈ ℂ )
rlim0.2 ( 𝜑𝐴 ⊆ ℝ )
Assertion rlim0 ( 𝜑 → ( ( 𝑧𝐴𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 rlim0.1 ( 𝜑 → ∀ 𝑧𝐴 𝐵 ∈ ℂ )
2 rlim0.2 ( 𝜑𝐴 ⊆ ℝ )
3 0cnd ( 𝜑 → 0 ∈ ℂ )
4 1 2 3 rlim2 ( 𝜑 → ( ( 𝑧𝐴𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ) )
5 subid1 ( 𝐵 ∈ ℂ → ( 𝐵 − 0 ) = 𝐵 )
6 5 fveq2d ( 𝐵 ∈ ℂ → ( abs ‘ ( 𝐵 − 0 ) ) = ( abs ‘ 𝐵 ) )
7 6 breq1d ( 𝐵 ∈ ℂ → ( ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ( abs ‘ 𝐵 ) < 𝑥 ) )
8 7 imbi2d ( 𝐵 ∈ ℂ → ( ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )
9 8 ralimi ( ∀ 𝑧𝐴 𝐵 ∈ ℂ → ∀ 𝑧𝐴 ( ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )
10 ralbi ( ∀ 𝑧𝐴 ( ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) → ( ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )
11 1 9 10 3syl ( 𝜑 → ( ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )
12 11 rexbidv ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )
13 12 ralbidv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )
14 4 13 bitrd ( 𝜑 → ( ( 𝑧𝐴𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀ 𝑧𝐴 ( 𝑦𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )