Metamath Proof Explorer


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 ≠ 𝐶 )