Theorem cnndvlem2

Description: Lemma for cnndv . (Contributed by Asger C. Ipsen, 26-Aug-2021)

	Ref	Expression
Hypotheses	cnndvlem2.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
	cnndvlem2.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( T ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) )
	cnndvlem2.w	|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
Assertion	cnndvlem2	|- E. f ( f e. ( RR -cn-> RR ) /\ dom ( RR _D f ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		cnndvlem2.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		cnndvlem2.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( T ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) )
3		cnndvlem2.w	|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4	1 2 3	cnndvlem1	|- ( W e. ( RR -cn-> RR ) /\ dom ( RR _D W ) = (/) )
5		reex	|- RR e. _V
6	5	mptex	|- ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) ) e. _V
7	3 6	eqeltri	|- W e. _V
8		eleq1	|- ( f = W -> ( f e. ( RR -cn-> RR ) <-> W e. ( RR -cn-> RR ) ) )
9		oveq2	|- ( f = W -> ( RR _D f ) = ( RR _D W ) )
10	9	dmeqd	|- ( f = W -> dom ( RR _D f ) = dom ( RR _D W ) )
11	10	eqeq1d	|- ( f = W -> ( dom ( RR _D f ) = (/) <-> dom ( RR _D W ) = (/) ) )
12	8 11	anbi12d	|- ( f = W -> ( ( f e. ( RR -cn-> RR ) /\ dom ( RR _D f ) = (/) ) <-> ( W e. ( RR -cn-> RR ) /\ dom ( RR _D W ) = (/) ) ) )
13	7 12	spcev	|- ( ( W e. ( RR -cn-> RR ) /\ dom ( RR _D W ) = (/) ) -> E. f ( f e. ( RR -cn-> RR ) /\ dom ( RR _D f ) = (/) ) )
14	4 13	ax-mp	|- E. f ( f e. ( RR -cn-> RR ) /\ dom ( RR _D f ) = (/) )