Theorem mbfi1fseqlem6 19565

Description: Lemma for mbfi1fseq 19566. Verify that G converges pointwise to F, and wrap up the existence quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
mbfi1fseq.1	|- ( ph -> F e. MblFn )
mbfi1fseq.2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
mbfi1fseq.3	|- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
mbfi1fseq.4	|- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )

Assertion

Ref	Expression
mbfi1fseqlem6	|- ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0 p o R <_ ( g ` n ) /\ ( g ` n ) o R <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )

Distinct variable groups:   g, m, n, x, y, F   g, G, n, x   m, J   ph, m, n, x, y

Allowed substitution hints:   ph( g)   G( y, m)   J( x, y, g, n)

Proof of Theorem mbfi1fseqlem6

Dummy variables j k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	. . 3 |- ( ph -> F e. MblFn )
2		mbfi1fseq.2	. . 3 |- ( ph -> F : RR --> ( 0 [,) +oo ) )
3		mbfi1fseq.3	. . 3 |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
4		mbfi1fseq.4	. . 3 |- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )
5	1, 2, 3, 4	mbfi1fseqlem4 19563	. 2 |- ( ph -> G : NN --> dom S.1 )
6	1, 2, 3, 4	mbfi1fseqlem5 19564	. . 3 |- ( ( ph /\ n e. NN ) -> ( 0 p o R <_ ( G ` n ) /\ ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) )
7	6	ralrimiva 2749	. 2 |- ( ph -> A. n e. NN ( 0 p o R <_ ( G ` n ) /\ ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) )
8		simpr 448	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> x e. RR )
9	8	recnd 9070	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> x e. CC )
10	9	abscld 12193	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( abs ` x ) e. RR )
11	2	ffvelrnda 5829	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
12		elrege0 10963	. . . . . . . 8 |- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
13	11, 12	sylib 189	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
14	13	simpld 446	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
15	10, 14	readdcld 9071	. . . . 5 |- ( ( ph /\ x e. RR ) -> ( ( abs ` x ) + ( F ` x ) ) e. RR )
16		arch 10174	. . . . 5 |- ( ( ( abs ` x ) + ( F ` x ) ) e. RR -> E. k e. NN ( ( abs ` x ) + ( F ` x ) ) < k )
17	15, 16	syl 16	. . . 4 |- ( ( ph /\ x e. RR ) -> E. k e. NN ( ( abs ` x ) + ( F ` x ) ) < k )
18		eqid 2404	. . . . 5 |- ( ZZ>= ` k ) = ( ZZ>= ` k )
19		nnz 10259	. . . . . 6 |- ( k e. NN -> k e. ZZ )
20	19	ad2antrl 709	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> k e. ZZ )
21		nnuz 10477	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
22		1z 10267	. . . . . . . . 9 |- 1 e. ZZ
23	22	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> 1 e. ZZ )
24		1re 9046	. . . . . . . . . . . 12 |- 1 e. RR
25	24	rehalfcli 10172	. . . . . . . . . . 11 |- ( 1 / 2 ) e. RR
26	25	recni 9058	. . . . . . . . . 10 |- ( 1 / 2 ) e. CC
27	26	a1i 11	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( 1 / 2 ) e. CC )
28		0re 9047	. . . . . . . . . . . . 13 |- 0 e. RR
29		halfgt0 10144	. . . . . . . . . . . . 13 |- 0 < ( 1 / 2 )
30	28, 25, 29	ltleii 9152	. . . . . . . . . . . 12 |- 0 <_ ( 1 / 2 )
31		absid 12056	. . . . . . . . . . . 12 |- ( ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) ) -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
32	25, 30, 31	mp2an 654	. . . . . . . . . . 11 |- ( abs ` ( 1 / 2 ) ) = ( 1 / 2 )
33		halflt1 10145	. . . . . . . . . . 11 |- ( 1 / 2 ) < 1
34	32, 33	eqbrtri 4191	. . . . . . . . . 10 |- ( abs ` ( 1 / 2 ) ) < 1
35	34	a1i 11	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( abs ` ( 1 / 2 ) ) < 1 )
36	27, 35	expcnv 12598	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ~~> 0 )
37	14	recnd 9070	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. CC )
38		nnex 9962	. . . . . . . . . 10 |- NN e. _V
39	38	mptex 5925	. . . . . . . . 9 |- ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) e. _V
40	39	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) e. _V )
41		nnnn0 10184	. . . . . . . . . . 11 |- ( j e. NN -> j e. NN0 )
42	41	adantl 453	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> j e. NN0 )
43		oveq2 6048	. . . . . . . . . . 11 |- ( n = j -> ( ( 1 / 2 ) ^ n ) = ( ( 1 / 2 ) ^ j ) )
44		eqid 2404	. . . . . . . . . . 11 |- ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) = ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) )
45		ovex 6065	. . . . . . . . . . 11 |- ( ( 1 / 2 ) ^ j ) e. _V
46	43, 44, 45	fvmpt 5765	. . . . . . . . . 10 |- ( j e. NN0 -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) = ( ( 1 / 2 ) ^ j ) )
47	42, 46	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) = ( ( 1 / 2 ) ^ j ) )
48		expcl 11354	. . . . . . . . . 10 |- ( ( ( 1 / 2 ) e. CC /\ j e. NN0 ) -> ( ( 1 / 2 ) ^ j ) e. CC )
49	26, 42, 48	sylancr 645	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( 1 / 2 ) ^ j ) e. CC )
50	47, 49	eqeltrd 2478	. . . . . . . 8 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) e. CC )
51	43	oveq2d 6056	. . . . . . . . . . 11 |- ( n = j -> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
52		eqid 2404	. . . . . . . . . . 11 |- ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) = ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) )
53		ovex 6065	. . . . . . . . . . 11 |- ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) e. _V
54	51, 52, 53	fvmpt 5765	. . . . . . . . . 10 |- ( j e. NN -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
55	54	adantl 453	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
56	47	oveq2d 6056	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( F ` x ) - ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
57	55, 56	eqtr4d 2439	. . . . . . . 8 |- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` j ) ) )
58	21, 23, 36, 37, 40, 50, 57	climsubc2 12387	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ~~> ( ( F ` x ) - 0 ) )
59	37	subid1d 9356	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( ( F ` x ) - 0 ) = ( F ` x ) )
60	58, 59	breqtrd 4196	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ~~> ( F ` x ) )
61	60	adantr 452	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ~~> ( F ` x ) )
62	38	mptex 5925	. . . . . 6 |- ( n e. NN |-> ( ( G ` n ) ` x ) ) e. _V
63	62	a1i 11	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> ( n e. NN |-> ( ( G ` n ) ` x ) ) e. _V )
64		simprl 733	. . . . . . . 8 |- ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> k e. NN )
65	21	uztrn2 10459	. . . . . . . 8 |- ( ( k e. NN /\ j e. ( ZZ>= ` k ) ) -> j e. NN )
66	64, 65	sylan 458	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. NN )
67	66, 54	syl 16	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) = ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) )
68	14	ad2antrr 707	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) e. RR )
69	66, 41	syl 16	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. NN0 )
70		reexpcl 11353	. . . . . . . 8 |- ( ( ( 1 / 2 ) e. RR /\ j e. NN0 ) -> ( ( 1 / 2 ) ^ j ) e. RR )
71	25, 69, 70	sylancr 645	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( 1 / 2 ) ^ j ) e. RR )
72	68, 71	resubcld 9421	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) e. RR )
73	67, 72	eqeltrd 2478	. . . . 5 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) e. RR )
74		fveq2 5687	. . . . . . . . 9 |- ( n = j -> ( G ` n ) = ( G ` j ) )
75	74	fveq1d 5689	. . . . . . . 8 |- ( n = j -> ( ( G ` n ) ` x ) = ( ( G ` j ) ` x ) )
76		eqid 2404	. . . . . . . 8 |- ( n e. NN |-> ( ( G ` n ) ` x ) ) = ( n e. NN |-> ( ( G ` n ) ` x ) )
77		fvex 5701	. . . . . . . 8 |- ( ( G ` j ) ` x ) e. _V
78	75, 76, 77	fvmpt 5765	. . . . . . 7 |- ( j e. NN -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = ( ( G ` j ) ` x ) )
79	66, 78	syl 16	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = ( ( G ` j ) ` x ) )
80	5	ad3antrrr 711	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> G : NN --> dom S.1 )
81	80, 66	ffvelrnd 5830	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( G ` j ) e. dom S.1 )
82		i1ff 19521	. . . . . . . 8 |- ( ( G ` j ) e. dom S.1 -> ( G ` j ) : RR --> RR )
83	81, 82	syl 16	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( G ` j ) : RR --> RR )
84	8	ad2antrr 707	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x e. RR )
85	83, 84	ffvelrnd 5830	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( G ` j ) ` x ) e. RR )
86	79, 85	eqeltrd 2478	. . . . 5 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) e. RR )
87	37	ad2antrr 707	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) e. CC )
88		2nn 10089	. . . . . . . . . . . . . 14 |- 2 e. NN
89		nnexpcl 11349	. . . . . . . . . . . . . 14 |- ( ( 2 e. NN /\ j e. NN0 ) -> ( 2 ^ j ) e. NN )
90	88, 69, 89	sylancr 645	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) e. NN )
91	90	nnred 9971	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) e. RR )
92	91	recnd 9070	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) e. CC )
93	90	nnne0d 10000	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 2 ^ j ) =/= 0 )
94	87, 92, 93	divcan4d 9752	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) = ( F ` x ) )
95	94	eqcomd 2409	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) = ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) )
96		2cn 10026	. . . . . . . . . . 11 |- 2 e. CC
97	96	a1i 11	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 2 e. CC )
98		2ne0 10039	. . . . . . . . . . 11 |- 2 =/= 0
99	98	a1i 11	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 2 =/= 0 )
100		eluzelz 10452	. . . . . . . . . . 11 |- ( j e. ( ZZ>= ` k ) -> j e. ZZ )
101	100	adantl 453	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. ZZ )
102	97, 99, 101	exprecd 11486	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( 1 / 2 ) ^ j ) = ( 1 / ( 2 ^ j ) ) )
103	95, 102	oveq12d 6058	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) = ( ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) - ( 1 / ( 2 ^ j ) ) ) )
104	68, 91	remulcld 9072	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) x. ( 2 ^ j ) ) e. RR )
105	104	recnd 9070	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) x. ( 2 ^ j ) ) e. CC )
106		ax-1cn 9004	. . . . . . . . . 10 |- 1 e. CC
107	106	a1i 11	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 1 e. CC )
108	105, 107, 92, 93	divsubdird 9785	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) = ( ( ( ( F ` x ) x. ( 2 ^ j ) ) / ( 2 ^ j ) ) - ( 1 / ( 2 ^ j ) ) ) )
109	103, 108	eqtr4d 2439	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) = ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) )
110		fllep1 11165	. . . . . . . . . 10 |- ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( ( F ` x ) x. ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) + 1 ) )
111	104, 110	syl 16	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) x. ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) + 1 ) )
112	24	a1i 11	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 1 e. RR )
113		reflcl 11160	. . . . . . . . . . 11 |- ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR )
114	104, 113	syl 16	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR )
115	104, 112, 114	lesubaddd 9579	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <-> ( ( F ` x ) x. ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) + 1 ) ) )
116	111, 115	mpbird 224	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) )
117		peano2rem 9323	. . . . . . . . . 10 |- ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) e. RR )
118	104, 117	syl 16	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) e. RR )
119	90	nngt0d 9999	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 0 < ( 2 ^ j ) )
120		lediv1 9831	. . . . . . . . 9 |- ( ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) e. RR /\ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR /\ ( ( 2 ^ j ) e. RR /\ 0 < ( 2 ^ j ) ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <-> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) )
121	118, 114, 91, 119, 120	syl112anc 1188	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <-> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) )
122	116, 121	mpbid 202	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( ( F ` x ) x. ( 2 ^ j ) ) - 1 ) / ( 2 ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
123	109, 122	eqbrtrd 4192	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) - ( ( 1 / 2 ) ^ j ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
124	1, 2, 3, 4	mbfi1fseqlem2 19561	. . . . . . . . . 10 |- ( j e. NN -> ( G ` j ) = ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) )
125	66, 124	syl 16	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( G ` j ) = ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) )
126	125	fveq1d 5689	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( G ` j ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) ` x ) )
127		ovex 6065	. . . . . . . . . . 11 |- ( j J x ) e. _V
128		vex 2919	. . . . . . . . . . 11 |- j e. _V
129	127, 128	ifex 3757	. . . . . . . . . 10 |- if ( ( j J x ) <_ j , ( j J x ) , j ) e. _V
130		c0ex 9041	. . . . . . . . . 10 |- 0 e. _V
131	129, 130	ifex 3757	. . . . . . . . 9 |- if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) e. _V
132		eqid 2404	. . . . . . . . . 10 |- ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
133	132	fvmpt2 5771	. . . . . . . . 9 |- ( ( x e. RR /\ if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) ` x ) = if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
134	84, 131, 133	sylancl 644	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( x e. RR |-> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) ) ` x ) = if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
135	79, 126, 134	3eqtrd 2440	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) )
136	10	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( abs ` x ) e. RR )
137	15	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) e. RR )
138	66	nnred 9971	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> j e. RR )
139	11	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) e. ( 0 [,) +oo ) )
140	139, 12	sylib 189	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
141	140	simprd 450	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 0 <_ ( F ` x ) )
142	136, 68	addge01d 9570	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 0 <_ ( F ` x ) <-> ( abs ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) ) )
143	141, 142	mpbid 202	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( abs ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) )
144	64	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> k e. NN )
145	144	nnred 9971	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> k e. RR )
146		simplrr 738	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) < k )
147	137, 145, 146	ltled 9177	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) <_ k )
148		eluzle 10454	. . . . . . . . . . . . . 14 |- ( j e. ( ZZ>= ` k ) -> k <_ j )
149	148	adantl 453	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> k <_ j )
150	137, 145, 138, 147, 149	letrd 9183	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) + ( F ` x ) ) <_ j )
151	136, 137, 138, 143, 150	letrd 9183	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( abs ` x ) <_ j )
152	84, 138	absled 12188	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( abs ` x ) <_ j <-> ( -u j <_ x /\ x <_ j ) ) )
153	151, 152	mpbid 202	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( -u j <_ x /\ x <_ j ) )
154	153	simpld 446	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> -u j <_ x )
155	153	simprd 450	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x <_ j )
156	138	renegcld 9420	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> -u j e. RR )
157		elicc2 10931	. . . . . . . . . 10 |- ( ( -u j e. RR /\ j e. RR ) -> ( x e. ( -u j [,] j ) <-> ( x e. RR /\ -u j <_ x /\ x <_ j ) ) )
158	156, 138, 157	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( x e. ( -u j [,] j ) <-> ( x e. RR /\ -u j <_ x /\ x <_ j ) ) )
159	84, 154, 155, 158	mpbir3and 1137	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x e. ( -u j [,] j ) )
160		iftrue 3705	. . . . . . . 8 |- ( x e. ( -u j [,] j ) -> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) = if ( ( j J x ) <_ j , ( j J x ) , j ) )
161	159, 160	syl 16	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> if ( x e. ( -u j [,] j ) , if ( ( j J x ) <_ j , ( j J x ) , j ) , 0 ) = if ( ( j J x ) <_ j , ( j J x ) , j ) )
162		simpr 448	. . . . . . . . . . . . . . . 16 |- ( ( m = j /\ y = x ) -> y = x )
163	162	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( ( m = j /\ y = x ) -> ( F ` y ) = ( F ` x ) )
164		simpl 444	. . . . . . . . . . . . . . . 16 |- ( ( m = j /\ y = x ) -> m = j )
165	164	oveq2d 6056	. . . . . . . . . . . . . . 15 |- ( ( m = j /\ y = x ) -> ( 2 ^ m ) = ( 2 ^ j ) )
166	163, 165	oveq12d 6058	. . . . . . . . . . . . . 14 |- ( ( m = j /\ y = x ) -> ( ( F ` y ) x. ( 2 ^ m ) ) = ( ( F ` x ) x. ( 2 ^ j ) ) )
167	166	fveq2d 5691	. . . . . . . . . . . . 13 |- ( ( m = j /\ y = x ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) )
168	167, 165	oveq12d 6058	. . . . . . . . . . . 12 |- ( ( m = j /\ y = x ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
169		ovex 6065	. . . . . . . . . . . 12 |- ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) e. _V
170	168, 3, 169	ovmpt2a 6163	. . . . . . . . . . 11 |- ( ( j e. NN /\ x e. RR ) -> ( j J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
171	66, 84, 170	syl2anc 643	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( j J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
172	114, 90	nndivred 10004	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) e. RR )
173		flle 11163	. . . . . . . . . . . . 13 |- ( ( ( F ` x ) x. ( 2 ^ j ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) )
174	104, 173	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) )
175		ledivmul2 9843	. . . . . . . . . . . . 13 |- ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) e. RR /\ ( F ` x ) e. RR /\ ( ( 2 ^ j ) e. RR /\ 0 < ( 2 ^ j ) ) ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ ( F ` x ) <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) ) )
176	114, 68, 91, 119, 175	syl112anc 1188	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ ( F ` x ) <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) <_ ( ( F ` x ) x. ( 2 ^ j ) ) ) )
177	174, 176	mpbird 224	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ ( F ` x ) )
178	9	ad2antrr 707	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> x e. CC )
179	178	absge0d 12201	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> 0 <_ ( abs ` x ) )
180	68, 136	addge02d 9571	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( 0 <_ ( abs ` x ) <-> ( F ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) ) )
181	179, 180	mpbid 202	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) <_ ( ( abs ` x ) + ( F ` x ) ) )
182	68, 137, 138, 181, 150	letrd 9183	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` x ) <_ j )
183	172, 68, 138, 177, 182	letrd 9183	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) <_ j )
184	171, 183	eqbrtrd 4192	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( j J x ) <_ j )
185		iftrue 3705	. . . . . . . . 9 |- ( ( j J x ) <_ j -> if ( ( j J x ) <_ j , ( j J x ) , j ) = ( j J x ) )
186	184, 185	syl 16	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> if ( ( j J x ) <_ j , ( j J x ) , j ) = ( j J x ) )
187	186, 171	eqtrd 2436	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> if ( ( j J x ) <_ j , ( j J x ) , j ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
188	135, 161, 187	3eqtrd 2440	. . . . . 6 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) )
189	123, 67, 188	3brtr4d 4202	. . . . 5 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( F ` x ) - ( ( 1 / 2 ) ^ n ) ) ) ` j ) <_ ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) )
190	188, 177	eqbrtrd 4192	. . . . 5 |- ( ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) /\ j e. ( ZZ>= ` k ) ) -> ( ( n e. NN |-> ( ( G ` n ) ` x ) ) ` j ) <_ ( F ` x ) )
191	18, 20, 61, 63, 73, 86, 189, 190	climsqz 12389	. . . 4 |- ( ( ( ph /\ x e. RR ) /\ ( k e. NN /\ ( ( abs ` x ) + ( F ` x ) ) < k ) ) -> ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) )
192	17, 191	rexlimddv 2794	. . 3 |- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) )
193	192	ralrimiva 2749	. 2 |- ( ph -> A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) )
194	38	mptex 5925	. . . 4 |- ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) ) e. _V
195	4, 194	eqeltri 2474	. . 3 |- G e. _V
196		feq1 5535	. . . 4 |- ( g = G -> ( g : NN --> dom S.1 <-> G : NN --> dom S.1 ) )
197		fveq1 5686	. . . . . . 7 |- ( g = G -> ( g ` n ) = ( G ` n ) )
198	197	breq2d 4184	. . . . . 6 |- ( g = G -> ( 0 p o R <_ ( g ` n ) <-> 0 p o R <_ ( G ` n ) ) )
199		fveq1 5686	. . . . . . 7 |- ( g = G -> ( g ` ( n + 1 ) ) = ( G ` ( n + 1 ) ) )
200	197, 199	breq12d 4185	. . . . . 6 |- ( g = G -> ( ( g ` n ) o R <_ ( g ` ( n + 1 ) ) <-> ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) )
201	198, 200	anbi12d 692	. . . . 5 |- ( g = G -> ( ( 0 p o R <_ ( g ` n ) /\ ( g ` n ) o R <_ ( g ` ( n + 1 ) ) ) <-> ( 0 p o R <_ ( G ` n ) /\ ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) ) )
202	201	ralbidv 2686	. . . 4 |- ( g = G -> ( A. n e. NN ( 0 p o R <_ ( g ` n ) /\ ( g ` n ) o R <_ ( g ` ( n + 1 ) ) ) <-> A. n e. NN ( 0 p o R <_ ( G ` n ) /\ ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) ) )
203	197	fveq1d 5689	. . . . . . 7 |- ( g = G -> ( ( g ` n ) ` x ) = ( ( G ` n ) ` x ) )
204	203	mpteq2dv 4256	. . . . . 6 |- ( g = G -> ( n e. NN |-> ( ( g ` n ) ` x ) ) = ( n e. NN |-> ( ( G ` n ) ` x ) ) )
205	204	breq1d 4182	. . . . 5 |- ( g = G -> ( ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) <-> ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) )
206	205	ralbidv 2686	. . . 4 |- ( g = G -> ( A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) <-> A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) )
207	196, 202, 206	3anbi123d 1254	. . 3 |- ( g = G -> ( ( g : NN --> dom S.1 /\ A. n e. NN ( 0 p o R <_ ( g ` n ) /\ ( g ` n ) o R <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) <-> ( G : NN --> dom S.1 /\ A. n e. NN ( 0 p o R <_ ( G ` n ) /\ ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
208	195, 207	spcev 3003	. 2 |- ( ( G : NN --> dom S.1 /\ A. n e. NN ( 0 p o R <_ ( G ` n ) /\ ( G ` n ) o R <_ ( G ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( G ` n ) ` x ) ) ~~> ( F ` x ) ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0 p o R <_ ( g ` n ) /\ ( g ` n ) o R <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
209	5, 7, 193, 208	syl3anc 1184	1 |- ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0 p o R <_ ( g ` n ) /\ ( g ` n ) o R <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   ifcif 3699   class class class wbr 4172   e. cmpt 4226   dom cdm 4837   -->wf 5409   ` cfv 5413  (class class class)co 6040   e. cmpt2 6042   o Rcofr 6263   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   +oocpnf 9073   < clt 9076   <_ cle 9077   - cmin 9247   -ucneg 9248   / cdiv 9633   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   [,)cico 10874   [,]cicc 10875   |_cfl 11156   ^cexp 11337   abscabs 11994   ~~> cli 12233  MblFncmbf 19459   S.1citg1 19460   0 pc0p 19514

This theorem is referenced by:  mbfi1fseq  19566

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-ofr 6265  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-rlim 12238  df-sum 12435  df-rest 13605  df-topgen 13622  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-top 16918  df-bases 16920  df-topon 16921  df-cmp 17404  df-ovol 19314  df-vol 19315  df-mbf 19465  df-itg1 19466  df-0p 19515