Theorem knoppndvlem3

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

	Ref	Expression
Hypothesis	knoppndvlem3.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
Assertion	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem3.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
2		elioore	⊢ ( 𝐶 ∈ ( - 1 (,) 1 ) → 𝐶 ∈ ℝ )
3	1 2	syl	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		eliooord	⊢ ( 𝐶 ∈ ( - 1 (,) 1 ) → ( - 1 < 𝐶 ∧ 𝐶 < 1 ) )
5	1 4	syl	⊢ ( 𝜑 → ( - 1 < 𝐶 ∧ 𝐶 < 1 ) )
6		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
7	3 6	absltd	⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) < 1 ↔ ( - 1 < 𝐶 ∧ 𝐶 < 1 ) ) )
8	5 7	mpbird	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
9	3 8	jca	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )