Theorem 0nonelalab

Description: Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024)

	Ref	Expression
Hypotheses	0nonelaleb.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	0nonelaleb.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	0nonelaleb.3	⊢ ( 𝜑 → 0 < 𝐴 )
	0nonelaleb.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	0nonelalab.5	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
Assertion	0nonelalab	⊢ ( 𝜑 → 0 ≠ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		0nonelaleb.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		0nonelaleb.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		0nonelaleb.3	⊢ ( 𝜑 → 0 < 𝐴 )
4		0nonelaleb.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		0nonelalab.5	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
6		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
7		elioore	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → 𝐶 ∈ ℝ )
8	5 7	syl	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
9	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
10	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
11		elioo2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
12	9 10 11	syl2anc	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
13	5 12	mpbid	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
14	13	simp2d	⊢ ( 𝜑 → 𝐴 < 𝐶 )
15	6 1 8 3 14	lttrd	⊢ ( 𝜑 → 0 < 𝐶 )
16	6 15	ltned	⊢ ( 𝜑 → 0 ≠ 𝐶 )