Theorem stoweidlem60 27676

Description: This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all t in T, there is a j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here F is used to represent f in the paper, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Hypotheses

Ref	Expression
stoweidlem60.1	|- F/_ t F
stoweidlem60.2	|- F/ t ph
stoweidlem60.3	|- K = ( topGen ` ran (,) )
stoweidlem60.4	|- T = U. J
stoweidlem60.5	|- C = ( J Cn K )
stoweidlem60.6	|- D = ( j e. ( 0 ... n ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
stoweidlem60.7	|- B = ( j e. ( 0 ... n ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
stoweidlem60.8	|- ( ph -> J e. Comp )
stoweidlem60.9	|- ( ph -> T =/= (/) )
stoweidlem60.10	|- ( ph -> A C_ C )
stoweidlem60.11	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem60.12	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem60.13	|- ( ( ph /\ y e. RR ) -> ( t e. T |-> y ) e. A )
stoweidlem60.14	|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
stoweidlem60.15	|- ( ph -> F e. C )
stoweidlem60.16	|- ( ph -> A. t e. T 0 <_ ( F ` t ) )
stoweidlem60.17	|- ( ph -> E e. RR+ )
stoweidlem60.18	|- ( ph -> E < ( 1 / 3 ) )

Assertion

Ref	Expression
stoweidlem60	|- ( ph -> E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )

Distinct variable groups:   f, g, j, n, t, A, q, r   y, f, j, n, q, r, t, A   B, f, g   D, f, g   f, E, g, j, n, t   f, J, g, r, t   T, f, g, j, n, t   ph, f, g, j, n   g, F, j, n   B, q, r, y   D, q, r, y   T, q, r, y   ph, q, r, y   E, r, y   t, K

Allowed substitution hints:   ph( t)   B( t, j, n)   C( y, t, f, g, j, n, r, q)   D( t, j, n)   E( q)   F( y, t, f, r, q)   J( y, j, n, q)   K( y, f, g, j, n, r, q)

Proof of Theorem stoweidlem60

Dummy variables i x m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem60.1	. . . . . . . 8 |- F/_ t F
2		stoweidlem60.2	. . . . . . . 8 |- F/ t ph
3		stoweidlem60.3	. . . . . . . 8 |- K = ( topGen ` ran (,) )
4		stoweidlem60.8	. . . . . . . 8 |- ( ph -> J e. Comp )
5		stoweidlem60.4	. . . . . . . 8 |- T = U. J
6		stoweidlem60.9	. . . . . . . 8 |- ( ph -> T =/= (/) )
7		stoweidlem60.5	. . . . . . . 8 |- C = ( J Cn K )
8		stoweidlem60.15	. . . . . . . 8 |- ( ph -> F e. C )
9	1, 2, 3, 4, 5, 6, 7, 8	rfcnnnub 27574	. . . . . . 7 |- ( ph -> E. m e. NN A. t e. T ( F ` t ) < m )
10		nnre 9963	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR )
11	10	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. NN ) -> m e. RR )
12		stoweidlem60.17	. . . . . . . . . . . . . . . 16 |- ( ph -> E e. RR+ )
13	12	rpred 10604	. . . . . . . . . . . . . . 15 |- ( ph -> E e. RR )
14	13	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. NN ) -> E e. RR )
15	12	rpne0d 10609	. . . . . . . . . . . . . . 15 |- ( ph -> E =/= 0 )
16	15	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. NN ) -> E =/= 0 )
17	11, 14, 16	redivcld 9798	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. NN ) -> ( m / E ) e. RR )
18		1re 9046	. . . . . . . . . . . . . 14 |- 1 e. RR
19	18	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. NN ) -> 1 e. RR )
20	17, 19	readdcld 9071	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN ) -> ( ( m / E ) + 1 ) e. RR )
21	20	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) -> ( ( m / E ) + 1 ) e. RR )
22		arch 10174	. . . . . . . . . . 11 |- ( ( ( m / E ) + 1 ) e. RR -> E. n e. NN ( ( m / E ) + 1 ) < n )
23	21, 22	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) -> E. n e. NN ( ( m / E ) + 1 ) < n )
24		nfv 1626	. . . . . . . . . . . . . . . . 17 |- F/ t m e. NN
25	2, 24	nfan 1842	. . . . . . . . . . . . . . . 16 |- F/ t ( ph /\ m e. NN )
26		nfra1 2716	. . . . . . . . . . . . . . . 16 |- F/ t A. t e. T ( F ` t ) < m
27	25, 26	nfan 1842	. . . . . . . . . . . . . . 15 |- F/ t ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m )
28		nfv 1626	. . . . . . . . . . . . . . 15 |- F/ t n e. NN
29	27, 28	nfan 1842	. . . . . . . . . . . . . 14 |- F/ t ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN )
30		nfv 1626	. . . . . . . . . . . . . 14 |- F/ t ( ( m / E ) + 1 ) < n
31	29, 30	nfan 1842	. . . . . . . . . . . . 13 |- F/ t ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n )
32		simp-5l 745	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ph )
33	3, 5, 7, 8	fcnre 27563	. . . . . . . . . . . . . . . . 17 |- ( ph -> F : T --> RR )
34	33	fnvinran 27552	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
35	32, 34	sylancom 649	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( F ` t ) e. RR )
36		simp-5r 746	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> m e. NN )
37	36	nnred 9971	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> m e. RR )
38		simpllr 736	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> n e. NN )
39	38	nnred 9971	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> n e. RR )
40	18	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> 1 e. RR )
41	39, 40	resubcld 9421	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( n - 1 ) e. RR )
42	32, 13	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> E e. RR )
43	41, 42	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( ( n - 1 ) x. E ) e. RR )
44		simpllr 736	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> A. t e. T ( F ` t ) < m )
45	44	r19.21bi 2764	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( F ` t ) < m )
46		simplr 732	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( ( m / E ) + 1 ) < n )
47		simpr 448	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( ( m / E ) + 1 ) < n )
48		simpl1 960	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ph )
49		simpl2 961	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> m e. NN )
50	48, 49, 17	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( m / E ) e. RR )
51	18	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> 1 e. RR )
52		simpl3 962	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> n e. NN )
53	52	nnred 9971	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> n e. RR )
54	50, 51, 53	ltaddsubd 9582	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( ( ( m / E ) + 1 ) < n <-> ( m / E ) < ( n - 1 ) ) )
55	47, 54	mpbid 202	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( m / E ) < ( n - 1 ) )
56	10	3ad2ant2 979	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. NN /\ n e. NN ) -> m e. RR )
57	56	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> m e. RR )
58	53, 51	resubcld 9421	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( n - 1 ) e. RR )
59	13	3ad2ant1 978	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. NN /\ n e. NN ) -> E e. RR )
60	59	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> E e. RR )
61	12	rpgt0d 10607	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 < E )
62	48, 61	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> 0 < E )
63		ltdivmul2 9841	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. RR /\ ( n - 1 ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( m / E ) < ( n - 1 ) <-> m < ( ( n - 1 ) x. E ) ) )
64	57, 58, 60, 62, 63	syl112anc 1188	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( ( m / E ) < ( n - 1 ) <-> m < ( ( n - 1 ) x. E ) ) )
65	55, 64	mpbid 202	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> m < ( ( n - 1 ) x. E ) )
66	32, 36, 38, 46, 65	syl31anc 1187	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> m < ( ( n - 1 ) x. E ) )
67	35, 37, 43, 45, 66	lttrd 9187	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( F ` t ) < ( ( n - 1 ) x. E ) )
68	67	ex 424	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( t e. T -> ( F ` t ) < ( ( n - 1 ) x. E ) ) )
69	31, 68	ralrimi 2747	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
70	69	ex 424	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) -> ( ( ( m / E ) + 1 ) < n -> A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
71	70	reximdva 2778	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) -> ( E. n e. NN ( ( m / E ) + 1 ) < n -> E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
72	23, 71	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) -> E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
73	72	ex 424	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( A. t e. T ( F ` t ) < m -> E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
74	73	rexlimdva 2790	. . . . . . 7 |- ( ph -> ( E. m e. NN A. t e. T ( F ` t ) < m -> E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
75	9, 74	mpd 15	. . . . . 6 |- ( ph -> E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
76		df-rex 2672	. . . . . 6 |- ( E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) <-> E. n ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
77	75, 76	sylib 189	. . . . 5 |- ( ph -> E. n ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
78		simpr 448	. . . . . . . . 9 |- ( ( ph /\ ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) ) -> ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
79	2, 28	nfan 1842	. . . . . . . . . . 11 |- F/ t ( ph /\ n e. NN )
80		stoweidlem60.6	. . . . . . . . . . 11 |- D = ( j e. ( 0 ... n ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
81		stoweidlem60.7	. . . . . . . . . . 11 |- B = ( j e. ( 0 ... n ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
82		eqid 2404	. . . . . . . . . . 11 |- { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) } = { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) }
83		eqid 2404	. . . . . . . . . . 11 |- ( j e. ( 0 ... n ) |-> { y e. { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) } | ( A. t e. ( D ` j ) ( y ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( y ` t ) ) } ) = ( j e. ( 0 ... n ) |-> { y e. { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) } | ( A. t e. ( D ` j ) ( y ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( y ` t ) ) } )
84	4	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> J e. Comp )
85		stoweidlem60.10	. . . . . . . . . . . 12 |- ( ph -> A C_ C )
86	85	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> A C_ C )
87		stoweidlem60.11	. . . . . . . . . . . 12 |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
88	87	3adant1r 1177	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
89		stoweidlem60.12	. . . . . . . . . . . 12 |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
90	89	3adant1r 1177	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
91		stoweidlem60.13	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( t e. T |-> y ) e. A )
92	91	adantlr 696	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ y e. RR ) -> ( t e. T |-> y ) e. A )
93		stoweidlem60.14	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
94	93	adantlr 696	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
95	8	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> F e. C )
96	12	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> E e. RR+ )
97		stoweidlem60.18	. . . . . . . . . . . 12 |- ( ph -> E < ( 1 / 3 ) )
98	97	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> E < ( 1 / 3 ) )
99		simpr 448	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> n e. NN )
100	1, 79, 3, 5, 7, 80, 81, 82, 83, 84, 86, 88, 90, 92, 94, 95, 96, 98, 99	stoweidlem59 27675	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> E. x ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) )
101	100	adantrr 698	. . . . . . . . 9 |- ( ( ph /\ ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) ) -> E. x ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) )
102		19.42v 1924	. . . . . . . . 9 |- ( E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) <-> ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ E. x ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) )
103	78, 101, 102	sylanbrc 646	. . . . . . . 8 |- ( ( ph /\ ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) ) -> E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) )
104		3anass 940	. . . . . . . . 9 |- ( ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) <-> ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) )
105	104	exbii 1589	. . . . . . . 8 |- ( E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) <-> E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ ( x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) )
106	103, 105	sylibr 204	. . . . . . 7 |- ( ( ph /\ ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) ) -> E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) )
107	106	ex 424	. . . . . 6 |- ( ph -> ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) -> E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) )
108	107	eximdv 1629	. . . . 5 |- ( ph -> ( E. n ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) -> E. n E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) )
109	77, 108	mpd 15	. . . 4 |- ( ph -> E. n E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) )
110		simpl 444	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> ph )
111		simpr1l 1014	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> n e. NN )
112		simpr2 964	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> x : ( 0 ... n ) --> A )
113		nfv 1626	. . . . . . . . . 10 |- F/ t x : ( 0 ... n ) --> A
114	2, 28, 113	nf3an 1845	. . . . . . . . 9 |- F/ t ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A )
115		simp2 958	. . . . . . . . 9 |- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> n e. NN )
116		simp3 959	. . . . . . . . 9 |- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> x : ( 0 ... n ) --> A )
117		simp1 957	. . . . . . . . . 10 |- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> ph )
118	117, 87	syl3an1 1217	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
119	117, 89	syl3an1 1217	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
120	91	3ad2antl1 1119	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ y e. RR ) -> ( t e. T |-> y ) e. A )
121	12	3ad2ant1 978	. . . . . . . . . 10 |- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> E e. RR+ )
122	121	rpred 10604	. . . . . . . . 9 |- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> E e. RR )
123	85	sselda 3308	. . . . . . . . . . 11 |- ( ( ph /\ f e. A ) -> f e. C )
124	3, 5, 7, 123	fcnre 27563	. . . . . . . . . 10 |- ( ( ph /\ f e. A ) -> f : T --> RR )
125	124	3ad2antl1 1119	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ f e. A ) -> f : T --> RR )
126	114, 115, 116, 118, 119, 120, 122, 125	stoweidlem17 27633	. . . . . . . 8 |- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) e. A )
127	110, 111, 112, 126	syl3anc 1184	. . . . . . 7 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) e. A )
128		nfv 1626	. . . . . . . . 9 |- F/ j ph
129		nfv 1626	. . . . . . . . . 10 |- F/ j ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
130		nfv 1626	. . . . . . . . . 10 |- F/ j x : ( 0 ... n ) --> A
131		nfra1 2716	. . . . . . . . . 10 |- F/ j A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
132	129, 130, 131	nf3an 1845	. . . . . . . . 9 |- F/ j ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
133	128, 132	nfan 1842	. . . . . . . 8 |- F/ j ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) )
134		nfra1 2716	. . . . . . . . . . 11 |- F/ t A. t e. T ( F ` t ) < ( ( n - 1 ) x. E )
135	28, 134	nfan 1842	. . . . . . . . . 10 |- F/ t ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
136		nfcv 2540	. . . . . . . . . . 11 |- F/_ t ( 0 ... n )
137		nfra1 2716	. . . . . . . . . . . 12 |- F/ t A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 )
138		nfra1 2716	. . . . . . . . . . . 12 |- F/ t A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n )
139		nfra1 2716	. . . . . . . . . . . 12 |- F/ t A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t )
140	137, 138, 139	nf3an 1845	. . . . . . . . . . 11 |- F/ t ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
141	136, 140	nfral 2719	. . . . . . . . . 10 |- F/ t A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
142	135, 113, 141	nf3an 1845	. . . . . . . . 9 |- F/ t ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
143	2, 142	nfan 1842	. . . . . . . 8 |- F/ t ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) )
144		eqid 2404	. . . . . . . 8 |- ( t e. T |-> { j e. ( 1 ... n ) | t e. ( D ` j ) } ) = ( t e. T |-> { j e. ( 1 ... n ) | t e. ( D ` j ) } )
145		uniexg 4665	. . . . . . . . . . 11 |- ( J e. Comp -> U. J e. _V )
146	4, 145	syl 16	. . . . . . . . . 10 |- ( ph -> U. J e. _V )
147	5, 146	syl5eqel 2488	. . . . . . . . 9 |- ( ph -> T e. _V )
148	147	adantr 452	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> T e. _V )
149	33	adantr 452	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> F : T --> RR )
150		stoweidlem60.16	. . . . . . . . . 10 |- ( ph -> A. t e. T 0 <_ ( F ` t ) )
151	150	r19.21bi 2764	. . . . . . . . 9 |- ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )
152	151	adantlr 696	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ t e. T ) -> 0 <_ ( F ` t ) )
153		simpr1r 1015	. . . . . . . . 9 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
154	153	r19.21bi 2764	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ t e. T ) -> ( F ` t ) < ( ( n - 1 ) x. E ) )
155	12	adantr 452	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> E e. RR+ )
156	97	adantr 452	. . . . . . . 8 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> E < ( 1 / 3 ) )
157		simpll 731	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) ) -> ph )
158		simplr2 1000	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) ) -> x : ( 0 ... n ) --> A )
159		simpr 448	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) ) -> j e. ( 0 ... n ) )
160		simp1 957	. . . . . . . . . 10 |- ( ( ph /\ x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ph )
161		ffvelrn 5827	. . . . . . . . . . 11 |- ( ( x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ( x ` j ) e. A )
162	161	3adant1 975	. . . . . . . . . 10 |- ( ( ph /\ x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ( x ` j ) e. A )
163	85	sselda 3308	. . . . . . . . . . 11 |- ( ( ph /\ ( x ` j ) e. A ) -> ( x ` j ) e. C )
164	3, 5, 7, 163	fcnre 27563	. . . . . . . . . 10 |- ( ( ph /\ ( x ` j ) e. A ) -> ( x ` j ) : T --> RR )
165	160, 162, 164	syl2anc 643	. . . . . . . . 9 |- ( ( ph /\ x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ( x ` j ) : T --> RR )
166	157, 158, 159, 165	syl3anc 1184	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) ) -> ( x ` j ) : T --> RR )
167		simp1r3 1055	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
168		r19.26-3 2800	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) <-> ( A. j e. ( 0 ... n ) A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. j e. ( 0 ... n ) A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. j e. ( 0 ... n ) A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
169	168	simp1bi 972	. . . . . . . . . 10 |- ( A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) -> A. j e. ( 0 ... n ) A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) )
170		simpl 444	. . . . . . . . . . . 12 |- ( ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> 0 <_ ( ( x ` j ) ` t ) )
171	170	ralimi 2741	. . . . . . . . . . 11 |- ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> A. t e. T 0 <_ ( ( x ` j ) ` t ) )
172	171	ralimi 2741	. . . . . . . . . 10 |- ( A. j e. ( 0 ... n ) A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> A. j e. ( 0 ... n ) A. t e. T 0 <_ ( ( x ` j ) ` t ) )
173	167, 169, 172	3syl 19	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> A. j e. ( 0 ... n ) A. t e. T 0 <_ ( ( x ` j ) ` t ) )
174		simp2 958	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> j e. ( 0 ... n ) )
175		simp3 959	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> t e. T )
176		rsp 2726	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... n ) A. t e. T 0 <_ ( ( x ` j ) ` t ) -> ( j e. ( 0 ... n ) -> A. t e. T 0 <_ ( ( x ` j ) ` t ) ) )
177	176	imp 419	. . . . . . . . . 10 |- ( ( A. j e. ( 0 ... n ) A. t e. T 0 <_ ( ( x ` j ) ` t ) /\ j e. ( 0 ... n ) ) -> A. t e. T 0 <_ ( ( x ` j ) ` t ) )
178	177	r19.21bi 2764	. . . . . . . . 9 |- ( ( ( A. j e. ( 0 ... n ) A. t e. T 0 <_ ( ( x ` j ) ` t ) /\ j e. ( 0 ... n ) ) /\ t e. T ) -> 0 <_ ( ( x ` j ) ` t ) )
179	173, 174, 175, 178	syl21anc 1183	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> 0 <_ ( ( x ` j ) ` t ) )
180		simpr 448	. . . . . . . . . . . 12 |- ( ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> ( ( x ` j ) ` t ) <_ 1 )
181	180	ralimi 2741	. . . . . . . . . . 11 |- ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> A. t e. T ( ( x ` j ) ` t ) <_ 1 )
182	181	ralimi 2741	. . . . . . . . . 10 |- ( A. j e. ( 0 ... n ) A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> A. j e. ( 0 ... n ) A. t e. T ( ( x ` j ) ` t ) <_ 1 )
183	167, 169, 182	3syl 19	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> A. j e. ( 0 ... n ) A. t e. T ( ( x ` j ) ` t ) <_ 1 )
184		rsp 2726	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... n ) A. t e. T ( ( x ` j ) ` t ) <_ 1 -> ( j e. ( 0 ... n ) -> A. t e. T ( ( x ` j ) ` t ) <_ 1 ) )
185	184	imp 419	. . . . . . . . . 10 |- ( ( A. j e. ( 0 ... n ) A. t e. T ( ( x ` j ) ` t ) <_ 1 /\ j e. ( 0 ... n ) ) -> A. t e. T ( ( x ` j ) ` t ) <_ 1 )
186	185	r19.21bi 2764	. . . . . . . . 9 |- ( ( ( A. j e. ( 0 ... n ) A. t e. T ( ( x ` j ) ` t ) <_ 1 /\ j e. ( 0 ... n ) ) /\ t e. T ) -> ( ( x ` j ) ` t ) <_ 1 )
187	183, 174, 175, 186	syl21anc 1183	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. T ) -> ( ( x ` j ) ` t ) <_ 1 )
188		simp1r3 1055	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( D ` j ) ) -> A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
189	168	simp2bi 973	. . . . . . . . . 10 |- ( A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) -> A. j e. ( 0 ... n ) A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) )
190	188, 189	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( D ` j ) ) -> A. j e. ( 0 ... n ) A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) )
191		simp2 958	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( D ` j ) ) -> j e. ( 0 ... n ) )
192		simp3 959	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( D ` j ) ) -> t e. ( D ` j ) )
193		rsp 2726	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... n ) A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) -> ( j e. ( 0 ... n ) -> A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) ) )
194	193	imp 419	. . . . . . . . . 10 |- ( ( A. j e. ( 0 ... n ) A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ j e. ( 0 ... n ) ) -> A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) )
195	194	r19.21bi 2764	. . . . . . . . 9 |- ( ( ( A. j e. ( 0 ... n ) A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ j e. ( 0 ... n ) ) /\ t e. ( D ` j ) ) -> ( ( x ` j ) ` t ) < ( E / n ) )
196	190, 191, 192, 195	syl21anc 1183	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( D ` j ) ) -> ( ( x ` j ) ` t ) < ( E / n ) )
197		simp1r3 1055	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( B ` j ) ) -> A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
198	168	simp3bi 974	. . . . . . . . . 10 |- ( A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) -> A. j e. ( 0 ... n ) A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
199	197, 198	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( B ` j ) ) -> A. j e. ( 0 ... n ) A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
200		simp2 958	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( B ` j ) ) -> j e. ( 0 ... n ) )
201		simp3 959	. . . . . . . . 9 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( B ` j ) ) -> t e. ( B ` j ) )
202		rsp 2726	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... n ) A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) -> ( j e. ( 0 ... n ) -> A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) )
203	202	imp 419	. . . . . . . . . 10 |- ( ( A. j e. ( 0 ... n ) A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) /\ j e. ( 0 ... n ) ) -> A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
204	203	r19.21bi 2764	. . . . . . . . 9 |- ( ( ( A. j e. ( 0 ... n ) A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) /\ j e. ( 0 ... n ) ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
205	199, 200, 201, 204	syl21anc 1183	. . . . . . . 8 |- ( ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) /\ j e. ( 0 ... n ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) )
206	1, 133, 143, 80, 81, 144, 111, 148, 149, 152, 154, 155, 156, 166, 179, 187, 196, 205	stoweidlem34 27650	. . . . . . 7 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) ) )
207		nfmpt1 4258	. . . . . . . . . 10 |- F/_ t ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) )
208	207	nfeq2 2551	. . . . . . . . 9 |- F/ t g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) )
209		fveq1 5686	. . . . . . . . . . . . 13 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( g ` t ) = ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) )
210	209	breq1d 4182	. . . . . . . . . . . 12 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) <-> ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) ) )
211	209	breq2d 4184	. . . . . . . . . . . 12 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) <-> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) )
212	210, 211	anbi12d 692	. . . . . . . . . . 11 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) <-> ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) ) )
213	212	anbi2d 685	. . . . . . . . . 10 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) <-> ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) ) ) )
214	213	rexbidv 2687	. . . . . . . . 9 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) <-> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) ) ) )
215	208, 214	ralbid 2684	. . . . . . . 8 |- ( g = ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) -> ( A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) <-> A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) ) ) )
216	215	rspcev 3012	. . . . . . 7 |- ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) e. A /\ A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) ` t ) ) ) ) -> E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )
217	127, 206, 216	syl2anc 643	. . . . . 6 |- ( ( ph /\ ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) ) -> E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )
218	217	ex 424	. . . . 5 |- ( ph -> ( ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) -> E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) )
219	218	2eximdv 1631	. . . 4 |- ( ph -> ( E. n E. x ( ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) /\ x : ( 0 ... n ) --> A /\ A. j e. ( 0 ... n ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n ) /\ A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t ) ) ) -> E. n E. x E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) )