Theorem 0nonelalab

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

	Ref	Expression
Hypotheses	0nonelaleb.1	$$⊢\phi \to A\in ℝ$$
	0nonelaleb.2	$$⊢\phi \to B\in ℝ$$
	0nonelaleb.3	$$⊢\phi \to 0<A$$
	0nonelaleb.4	$$⊢\phi \to A\le B$$
	0nonelalab.5	$$⊢\phi \to C\in \left(A,B\right)$$
Assertion	0nonelalab	$$⊢\phi \to 0\ne C$$

Proof

Step	Hyp	Ref	Expression
1		0nonelaleb.1	$$⊢\phi \to A\in ℝ$$
2		0nonelaleb.2	$$⊢\phi \to B\in ℝ$$
3		0nonelaleb.3	$$⊢\phi \to 0<A$$
4		0nonelaleb.4	$$⊢\phi \to A\le B$$
5		0nonelalab.5	$$⊢\phi \to C\in \left(A,B\right)$$
6		0red	$$⊢\phi \to 0\in ℝ$$
7		elioore	$$⊢C\in \left(A,B\right)\to C\in ℝ$$
8	5 7	syl	$$⊢\phi \to C\in ℝ$$
9	1	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
10	2	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
11		elioo2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(C\in \left(A,B\right)\leftrightarrow \left(C\in ℝ\wedge A<C\wedge C<B\right)\right)$$
12	9 10 11	syl2anc	$$⊢\phi \to \left(C\in \left(A,B\right)\leftrightarrow \left(C\in ℝ\wedge A<C\wedge C<B\right)\right)$$
13	5 12	mpbid	$$⊢\phi \to \left(C\in ℝ\wedge A<C\wedge C<B\right)$$
14	13	simp2d	$$⊢\phi \to A<C$$
15	6 1 8 3 14	lttrd	$$⊢\phi \to 0<C$$
16	6 15	ltned	$$⊢\phi \to 0\ne C$$