Metamath Proof Explorer

Theorem knoppndvlem3

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021)

Ref Expression
Hypothesis knoppndvlem3.c ⊢ φ → C ∈ − 1 1
Assertion knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1

Proof

Step Hyp Ref Expression
1 knoppndvlem3.c ⊢ φ → C ∈ − 1 1
2 elioore ⊢ C ∈ − 1 1 → C ∈ ℝ
3 1 2 syl ⊢ φ → C ∈ ℝ
4 eliooord ⊢ C ∈ − 1 1 → − 1 < C ∧ C < 1
5 1 4 syl ⊢ φ → − 1 < C ∧ C < 1
6 1red ⊢ φ → 1 ∈ ℝ
7 3 6 absltd ⊢ φ → C < 1 ↔ − 1 < C ∧ C < 1
8 5 7 mpbird ⊢ φ → C < 1
9 3 8 jca ⊢ φ → C ∈ ℝ ∧ C < 1