Metamath Proof Explorer

Theorem knoppndvlem3

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem3.c ⊢φ→C∈−11
2 elioore ⊢C∈−11→C∈ℝ
3 1 2 syl ⊢φ→C∈ℝ
4 eliooord ⊢C∈−11→−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