Theorem 0nonelalab

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

	Ref	Expression
Hypotheses	0nonelaleb.1	|- ( ph -> A e. RR )
	0nonelaleb.2	|- ( ph -> B e. RR )
	0nonelaleb.3	|- ( ph -> 0 < A )
	0nonelaleb.4	|- ( ph -> A <_ B )
	0nonelalab.5	|- ( ph -> C e. ( A (,) B ) )
Assertion	0nonelalab	|- ( ph -> 0 =/= C )

Proof

Step	Hyp	Ref	Expression
1		0nonelaleb.1	|- ( ph -> A e. RR )
2		0nonelaleb.2	|- ( ph -> B e. RR )
3		0nonelaleb.3	|- ( ph -> 0 < A )
4		0nonelaleb.4	|- ( ph -> A <_ B )
5		0nonelalab.5	|- ( ph -> C e. ( A (,) B ) )
6		0red	|- ( ph -> 0 e. RR )
7		elioore	|- ( C e. ( A (,) B ) -> C e. RR )
8	5 7	syl	|- ( ph -> C e. RR )
9	1	rexrd	|- ( ph -> A e. RR* )
10	2	rexrd	|- ( ph -> B e. RR* )
11		elioo2	|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
12	9 10 11	syl2anc	|- ( ph -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
13	5 12	mpbid	|- ( ph -> ( C e. RR /\ A < C /\ C < B ) )
14	13	simp2d	|- ( ph -> A < C )
15	6 1 8 3 14	lttrd	|- ( ph -> 0 < C )
16	6 15	ltned	|- ( ph -> 0 =/= C )