stoweidlem60

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)

	Ref	Expression
Hypotheses	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	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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem60.1	\|- F/_ t F
2		stoweidlem60.2	\|- F/ t ph
3		stoweidlem60.3	\|- K = ( topGen ` ran (,) )
4		stoweidlem60.4	\|- T = U. J
5		stoweidlem60.5	\|- C = ( J Cn K )
6		stoweidlem60.6	\|- D = ( j e. ( 0 ... n ) \|-> { t e. T \| ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
7		stoweidlem60.7	\|- B = ( j e. ( 0 ... n ) \|-> { t e. T \| ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
8		stoweidlem60.8	\|- ( ph -> J e. Comp )
9		stoweidlem60.9	\|- ( ph -> T =/= (/) )
10		stoweidlem60.10	\|- ( ph -> A C_ C )
11		stoweidlem60.11	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
12		stoweidlem60.12	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
13		stoweidlem60.13	\|- ( ( ph /\ y e. RR ) -> ( t e. T \|-> y ) e. A )
14		stoweidlem60.14	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
15		stoweidlem60.15	\|- ( ph -> F e. C )
16		stoweidlem60.16	\|- ( ph -> A. t e. T 0 <_ ( F ` t ) )
17		stoweidlem60.17	\|- ( ph -> E e. RR+ )
18		stoweidlem60.18	\|- ( ph -> E < ( 1 / 3 ) )
19		nnre	\|- ( m e. NN -> m e. RR )
20	19	adantl	\|- ( ( ph /\ m e. NN ) -> m e. RR )
21	17	rpred	\|- ( ph -> E e. RR )
22	21	adantr	\|- ( ( ph /\ m e. NN ) -> E e. RR )
23	17	rpne0d	\|- ( ph -> E =/= 0 )
24	23	adantr	\|- ( ( ph /\ m e. NN ) -> E =/= 0 )
25	20 22 24	redivcld	\|- ( ( ph /\ m e. NN ) -> ( m / E ) e. RR )
26		1red	\|- ( ( ph /\ m e. NN ) -> 1 e. RR )
27	25 26	readdcld	\|- ( ( ph /\ m e. NN ) -> ( ( m / E ) + 1 ) e. RR )
28	27	adantr	\|- ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) -> ( ( m / E ) + 1 ) e. RR )
29		arch	\|- ( ( ( m / E ) + 1 ) e. RR -> E. n e. NN ( ( m / E ) + 1 ) < n )
30	28 29	syl	\|- ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) -> E. n e. NN ( ( m / E ) + 1 ) < n )
31		nfv	\|- F/ t m e. NN
32	2 31	nfan	\|- F/ t ( ph /\ m e. NN )
33		nfra1	\|- F/ t A. t e. T ( F ` t ) < m
34	32 33	nfan	\|- F/ t ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m )
35		nfv	\|- F/ t n e. NN
36	34 35	nfan	\|- F/ t ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN )
37		nfv	\|- F/ t ( ( m / E ) + 1 ) < n
38	36 37	nfan	\|- F/ t ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n )
39		simp-5l	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ph )
40	3 4 5 15	fcnre	\|- ( ph -> F : T --> RR )
41	40	ffvelrnda	\|- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
42	39 41	sylancom	\|- ( ( ( ( ( ( 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 )
43		simp-5r	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> m e. NN )
44	43	nnred	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> m e. RR )
45		simpllr	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> n e. NN )
46	45	nnred	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> n e. RR )
47		1red	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> 1 e. RR )
48	46 47	resubcld	\|- ( ( ( ( ( ( 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 )
49	39 21	syl	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> E e. RR )
50	48 49	remulcld	\|- ( ( ( ( ( ( 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 )
51		simpllr	\|- ( ( ( ( ( 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 )
52	51	r19.21bi	\|- ( ( ( ( ( ( ph /\ m e. NN ) /\ A. t e. T ( F ` t ) < m ) /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) /\ t e. T ) -> ( F ` t ) < m )
53		simplr	\|- ( ( ( ( ( ( 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 )
54		simpr	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( ( m / E ) + 1 ) < n )
55		simpl1	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ph )
56		simpl2	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> m e. NN )
57	55 56 25	syl2anc	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( m / E ) e. RR )
58		1red	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> 1 e. RR )
59		simpl3	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> n e. NN )
60	59	nnred	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> n e. RR )
61	57 58 60	ltaddsubd	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( ( ( m / E ) + 1 ) < n <-> ( m / E ) < ( n - 1 ) ) )
62	54 61	mpbid	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( m / E ) < ( n - 1 ) )
63	19	3ad2ant2	\|- ( ( ph /\ m e. NN /\ n e. NN ) -> m e. RR )
64	63	adantr	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> m e. RR )
65	60 58	resubcld	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( n - 1 ) e. RR )
66	21	3ad2ant1	\|- ( ( ph /\ m e. NN /\ n e. NN ) -> E e. RR )
67	66	adantr	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> E e. RR )
68	17	rpgt0d	\|- ( ph -> 0 < E )
69	55 68	syl	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> 0 < E )
70		ltdivmul2	\|- ( ( m e. RR /\ ( n - 1 ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( m / E ) < ( n - 1 ) <-> m < ( ( n - 1 ) x. E ) ) )
71	64 65 67 69 70	syl112anc	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> ( ( m / E ) < ( n - 1 ) <-> m < ( ( n - 1 ) x. E ) ) )
72	62 71	mpbid	\|- ( ( ( ph /\ m e. NN /\ n e. NN ) /\ ( ( m / E ) + 1 ) < n ) -> m < ( ( n - 1 ) x. E ) )
73	39 43 45 53 72	syl31anc	\|- ( ( ( ( ( ( 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 ) )
74	42 44 50 52 73	lttrd	\|- ( ( ( ( ( ( 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 ) )
75	74	ex	\|- ( ( ( ( ( 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 ) ) )
76	38 75	ralrimi	\|- ( ( ( ( ( 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 ) )
77	76	ex	\|- ( ( ( ( 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 ) ) )
78	77	reximdva	\|- ( ( ( 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 ) ) )
79	30 78	mpd	\|- ( ( ( 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 ) )
80	1 2 3 8 4 9 5 15	rfcnnnub	\|- ( ph -> E. m e. NN A. t e. T ( F ` t ) < m )
81	79 80	r19.29a	\|- ( ph -> E. n e. NN A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
82		df-rex	\|- ( 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 ) ) )
83	81 82	sylib	\|- ( ph -> E. n ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) ) )
84		simpr	\|- ( ( 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 ) ) )
85	2 35	nfan	\|- F/ t ( ph /\ n e. NN )
86		eqid	\|- { 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 ) }
87		eqid	\|- ( 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 ) ) } )
88	8	adantr	\|- ( ( ph /\ n e. NN ) -> J e. Comp )
89	10	adantr	\|- ( ( ph /\ n e. NN ) -> A C_ C )
90	11	3adant1r	\|- ( ( ( ph /\ n e. NN ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
91	12	3adant1r	\|- ( ( ( ph /\ n e. NN ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
92	13	adantlr	\|- ( ( ( ph /\ n e. NN ) /\ y e. RR ) -> ( t e. T \|-> y ) e. A )
93	14	adantlr	\|- ( ( ( ph /\ n e. NN ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
94	15	adantr	\|- ( ( ph /\ n e. NN ) -> F e. C )
95	17	adantr	\|- ( ( ph /\ n e. NN ) -> E e. RR+ )
96	18	adantr	\|- ( ( ph /\ n e. NN ) -> E < ( 1 / 3 ) )
97		simpr	\|- ( ( ph /\ n e. NN ) -> n e. NN )
98	1 85 3 4 5 6 7 86 87 88 89 90 91 92 93 94 95 96 97	stoweidlem59	\|- ( ( 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 ) ) ) )
99	98	adantrr	\|- ( ( 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 ) ) ) )
100		19.42v	\|- ( 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 ) ) ) ) )
101	84 99 100	sylanbrc	\|- ( ( 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 ) ) ) ) )
102		3anass	\|- ( ( ( 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 ) ) ) ) )
103	102	exbii	\|- ( 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 ) ) ) ) )
104	101 103	sylibr	\|- ( ( 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 ) ) ) )
105	104	ex	\|- ( 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 ) ) ) ) )
106	105	eximdv	\|- ( 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 ) ) ) ) )
107	83 106	mpd	\|- ( 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 ) ) ) )
108		simpl	\|- ( ( 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 )
109		simpr1l	\|- ( ( 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 )
110		simpr2	\|- ( ( 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 )
111		nfv	\|- F/ t x : ( 0 ... n ) --> A
112	2 35 111	nf3an	\|- F/ t ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A )
113		simp2	\|- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> n e. NN )
114		simp3	\|- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> x : ( 0 ... n ) --> A )
115		simp1	\|- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> ph )
116	115 11	syl3an1	\|- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
117	115 12	syl3an1	\|- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
118	13	3ad2antl1	\|- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ y e. RR ) -> ( t e. T \|-> y ) e. A )
119	17	3ad2ant1	\|- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> E e. RR+ )
120	119	rpred	\|- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> E e. RR )
121	10	sselda	\|- ( ( ph /\ f e. A ) -> f e. C )
122	3 4 5 121	fcnre	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
123	122	3ad2antl1	\|- ( ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) /\ f e. A ) -> f : T --> RR )
124	112 113 114 116 117 118 120 123	stoweidlem17	\|- ( ( ph /\ n e. NN /\ x : ( 0 ... n ) --> A ) -> ( t e. T \|-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) ) e. A )
125	108 109 110 124	syl3anc	\|- ( ( 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 )
126		nfv	\|- F/ j ph
127		nfv	\|- F/ j ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
128		nfv	\|- F/ j x : ( 0 ... n ) --> A
129		nfra1	\|- 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 ) )
130	127 128 129	nf3an	\|- 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 ) ) )
131	126 130	nfan	\|- 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 ) ) ) )
132		nfra1	\|- F/ t A. t e. T ( F ` t ) < ( ( n - 1 ) x. E )
133	35 132	nfan	\|- F/ t ( n e. NN /\ A. t e. T ( F ` t ) < ( ( n - 1 ) x. E ) )
134		nfcv	\|- F/_ t ( 0 ... n )
135		nfra1	\|- F/ t A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 )
136		nfra1	\|- F/ t A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / n )
137		nfra1	\|- F/ t A. t e. ( B ` j ) ( 1 - ( E / n ) ) < ( ( x ` j ) ` t )
138	135 136 137	nf3an	\|- 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 ) )
139	134 138	nfralw	\|- 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 ) )
140	133 111 139	nf3an	\|- 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 ) ) )
141	2 140	nfan	\|- 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 ) ) ) )
142		eqid	\|- ( t e. T \|-> { j e. ( 1 ... n ) \| t e. ( D ` j ) } ) = ( t e. T \|-> { j e. ( 1 ... n ) \| t e. ( D ` j ) } )
143	8	uniexd	\|- ( ph -> U. J e. _V )
144	4 143	eqeltrid	\|- ( ph -> T e. _V )
145	144	adantr	\|- ( ( 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 )
146	40	adantr	\|- ( ( 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 )
147	16	r19.21bi	\|- ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )
148	147	adantlr	\|- ( ( ( 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 ) )
149		simpr1r	\|- ( ( 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 ) )
150	149	r19.21bi	\|- ( ( ( 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 ) )
151	17	adantr	\|- ( ( 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+ )
152	18	adantr	\|- ( ( 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 ) )
153		simpll	\|- ( ( ( 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 )
154		simplr2	\|- ( ( ( 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 )
155		simpr	\|- ( ( ( 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 ) )
156		simp1	\|- ( ( ph /\ x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ph )
157		ffvelrn	\|- ( ( x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ( x ` j ) e. A )
158	157	3adant1	\|- ( ( ph /\ x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ( x ` j ) e. A )
159	10	sselda	\|- ( ( ph /\ ( x ` j ) e. A ) -> ( x ` j ) e. C )
160	3 4 5 159	fcnre	\|- ( ( ph /\ ( x ` j ) e. A ) -> ( x ` j ) : T --> RR )
161	156 158 160	syl2anc	\|- ( ( ph /\ x : ( 0 ... n ) --> A /\ j e. ( 0 ... n ) ) -> ( x ` j ) : T --> RR )
162	153 154 155 161	syl3anc	\|- ( ( ( 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 )
163		simp1r3	\|- ( ( ( 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 ) ) )
164		r19.26-3	\|- ( 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 ) ) )
165	164	simp1bi	\|- ( 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 ) )
166		simpl	\|- ( ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> 0 <_ ( ( x ` j ) ` t ) )
167	166	2ralimi	\|- ( 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 ) )
168	163 165 167	3syl	\|- ( ( ( 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 ) )
169		simp2	\|- ( ( ( 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 ) )
170		simp3	\|- ( ( ( 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 )
171		rspa	\|- ( ( 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 ) )
172	171	r19.21bi	\|- ( ( ( A. j e. ( 0 ... n ) A. t e. T 0 <_ ( ( x ` j ) ` t ) /\ j e. ( 0 ... n ) ) /\ t e. T ) -> 0 <_ ( ( x ` j ) ` t ) )
173	168 169 170 172	syl21anc	\|- ( ( ( 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 ) )
174		simpr	\|- ( ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) -> ( ( x ` j ) ` t ) <_ 1 )
175	174	2ralimi	\|- ( 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 )
176	163 165 175	3syl	\|- ( ( ( 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 )
177		rspa	\|- ( ( 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 )
178	177	r19.21bi	\|- ( ( ( A. j e. ( 0 ... n ) A. t e. T ( ( x ` j ) ` t ) <_ 1 /\ j e. ( 0 ... n ) ) /\ t e. T ) -> ( ( x ` j ) ` t ) <_ 1 )
179	176 169 170 178	syl21anc	\|- ( ( ( 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 )
180		simp1r3	\|- ( ( ( 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 ) ) )
181	164	simp2bi	\|- ( 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 ) )
182	180 181	syl	\|- ( ( ( 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 ) )
183		simp2	\|- ( ( ( 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 ) )
184		simp3	\|- ( ( ( 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 ) )
185		rspa	\|- ( ( 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 ) )
186	185	r19.21bi	\|- ( ( ( 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 ) )
187	182 183 184 186	syl21anc	\|- ( ( ( 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 ) )
188		simp1r3	\|- ( ( ( 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 ) ) )
189	164	simp3bi	\|- ( 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 ) )
190	188 189	syl	\|- ( ( ( 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 ) )
191		simp2	\|- ( ( ( 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 ) )
192		simp3	\|- ( ( ( 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 ) )
193		rspa	\|- ( ( 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 ) )
194	193	r19.21bi	\|- ( ( ( 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 ) )
195	190 191 192 194	syl21anc	\|- ( ( ( 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 ) )
196	1 131 141 6 7 142 109 145 146 148 150 151 152 162 173 179 187 195	stoweidlem34	\|- ( ( 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 ) ) ) )
197		nfmpt1	\|- F/_ t ( t e. T \|-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) )
198	197	nfeq2	\|- F/ t g = ( t e. T \|-> sum_ i e. ( 0 ... n ) ( E x. ( ( x ` i ) ` t ) ) )
199		fveq1	\|- ( 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 ) )
200	199	breq1d	\|- ( 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 ) ) )
201	199	breq2d	\|- ( 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 ) ) )
202	200 201	anbi12d	\|- ( 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 ) ) ) )
203	202	anbi2d	\|- ( 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 ) ) ) ) )
204	203	rexbidv	\|- ( 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 ) ) ) ) )
205	198 204	ralbid	\|- ( 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 ) ) ) ) )
206	205	rspcev	\|- ( ( ( 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 ) ) ) )
207	125 196 206	syl2anc	\|- ( ( 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 ) ) ) )
208	207	ex	\|- ( 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 ) ) ) ) )
209	208	2eximdv	\|- ( 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) )
210	107 209	mpd	\|- ( ph -> 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )
211		idd	\|- ( ph -> ( 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) -> 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) )
212	211	exlimdv	\|- ( ph -> ( 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) -> 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) )
213	210 212	mpd	\|- ( ph -> 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )
214		idd	\|- ( 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 ) ) ) -> 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 ) ) ) ) )
215	214	exlimdv	\|- ( ph -> ( 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 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` 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 ) ) ) ) )
216	213 215	mpd	\|- ( 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 ) ) ) )

Metamath Proof Explorer

Theorem stoweidlem60

Proof