Theorem knoppndvlem3

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

	Ref	Expression
Hypothesis	knoppndvlem3.c	|- ( ph -> C e. ( -u 1 (,) 1 ) )
Assertion	knoppndvlem3	|- ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem3.c	|- ( ph -> C e. ( -u 1 (,) 1 ) )
2		elioore	|- ( C e. ( -u 1 (,) 1 ) -> C e. RR )
3	1 2	syl	|- ( ph -> C e. RR )
4		eliooord	|- ( C e. ( -u 1 (,) 1 ) -> ( -u 1 < C /\ C < 1 ) )
5	1 4	syl	|- ( ph -> ( -u 1 < C /\ C < 1 ) )
6		1red	|- ( ph -> 1 e. RR )
7	3 6	absltd	|- ( ph -> ( ( abs ` C ) < 1 <-> ( -u 1 < C /\ C < 1 ) ) )
8	5 7	mpbird	|- ( ph -> ( abs ` C ) < 1 )
9	3 8	jca	|- ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )