Theorem rlim0lt

Description: Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

	Ref	Expression
Hypotheses	rlim0.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
	rlim0.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
Assertion	rlim0lt	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlim0.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
2		rlim0.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
4	1 2 3	rlim2lt	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 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 ‘ 𝐵 ) < 𝑥 ) ) )