Metamath Proof Explorer


Theorem 0nonelalab

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

Ref Expression
Hypotheses 0nonelaleb.1 φ A
0nonelaleb.2 φ B
0nonelaleb.3 φ 0 < A
0nonelaleb.4 φ A B
0nonelalab.5 φ C A B
Assertion 0nonelalab φ 0 C

Proof

Step Hyp Ref Expression
1 0nonelaleb.1 φ A
2 0nonelaleb.2 φ B
3 0nonelaleb.3 φ 0 < A
4 0nonelaleb.4 φ A B
5 0nonelalab.5 φ C A B
6 0red φ 0
7 elioore C A B C
8 5 7 syl φ C
9 1 rexrd φ A *
10 2 rexrd φ B *
11 elioo2 A * B * C A B C A < C C < B
12 9 10 11 syl2anc φ C A B C A < C C < B
13 5 12 mpbid φ C A < C C < B
14 13 simp2d φ A < C
15 6 1 8 3 14 lttrd φ 0 < C
16 6 15 ltned φ 0 C