Metamath Proof Explorer

Theorem stoweidlem41

Description: This lemma is used to prove that there exists x as in Lemma 1 of BrosowskiDeutsh p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - q_n". Here E is used to represent ε in the paper, and y to represent q_n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem41.1 
|- F/ t ph
stoweidlem41.2 
|- X = ( t e. T |-> ( 1 - ( y ` t ) ) )
stoweidlem41.3 
|- F = ( t e. T |-> 1 )
stoweidlem41.4 
|- V C_ T
stoweidlem41.5 
|- ( ph -> y e. A )
stoweidlem41.6 
|- ( ph -> y : T --> RR )
stoweidlem41.7 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem41.8 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem41.9 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem41.10 
|- ( ( ph /\ w e. RR ) -> ( t e. T |-> w ) e. A )
stoweidlem41.11 
|- ( ph -> E e. RR+ )
stoweidlem41.12 
|- ( ph -> A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) )
stoweidlem41.13 
|- ( ph -> A. t e. V ( 1 - E ) < ( y ` t ) )
stoweidlem41.14 
|- ( ph -> A. t e. ( T \ U ) ( y ` t ) < E )
Assertion stoweidlem41 
|- ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( x ` t ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem41.1 
 |-  F/ t ph
2 stoweidlem41.2 
 |-  X = ( t e. T |-> ( 1 - ( y ` t ) ) )
3 stoweidlem41.3 
 |-  F = ( t e. T |-> 1 )
4 stoweidlem41.4 
 |-  V C_ T
5 stoweidlem41.5 
 |-  ( ph -> y e. A )
6 stoweidlem41.6 
 |-  ( ph -> y : T --> RR )
7 stoweidlem41.7 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
8 stoweidlem41.8 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
9 stoweidlem41.9 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
10 stoweidlem41.10 
 |-  ( ( ph /\ w e. RR ) -> ( t e. T |-> w ) e. A )
11 stoweidlem41.11 
 |-  ( ph -> E e. RR+ )
12 stoweidlem41.12 
 |-  ( ph -> A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) )
13 stoweidlem41.13 
 |-  ( ph -> A. t e. V ( 1 - E ) < ( y ` t ) )
14 stoweidlem41.14 
 |-  ( ph -> A. t e. ( T \ U ) ( y ` t ) < E )
15 1re 
 |-  1 e. RR
16 3 fvmpt2 
 |-  ( ( t e. T /\ 1 e. RR ) -> ( F ` t ) = 1 )
17 15 16 mpan2 
 |-  ( t e. T -> ( F ` t ) = 1 )
18 17 adantl 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) = 1 )
19 18 oveq1d 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) - ( y ` t ) ) = ( 1 - ( y ` t ) ) )
20 1 19 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) - ( y ` t ) ) ) = ( t e. T |-> ( 1 - ( y ` t ) ) ) )
21 20 2 eqtr4di 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) - ( y ` t ) ) ) = X )
22 10 stoweidlem4 
 |-  ( ( ph /\ 1 e. RR ) -> ( t e. T |-> 1 ) e. A )
23 15 22 mpan2 
 |-  ( ph -> ( t e. T |-> 1 ) e. A )
24 3 23 eqeltrid 
 |-  ( ph -> F e. A )
25 nfmpt1 
 |-  F/_ t ( t e. T |-> 1 )
26 3 25 nfcxfr 
 |-  F/_ t F
27 nfcv 
 |-  F/_ t y
28 26 27 1 7 8 9 10 stoweidlem33 
 |-  ( ( ph /\ F e. A /\ y e. A ) -> ( t e. T |-> ( ( F ` t ) - ( y ` t ) ) ) e. A )
29 24 5 28 mpd3an23 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) - ( y ` t ) ) ) e. A )
30 21 29 eqeltrrd 
 |-  ( ph -> X e. A )
31 6 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( y ` t ) e. RR )
32 1red 
 |-  ( ( ph /\ t e. T ) -> 1 e. RR )
33 0red 
 |-  ( ( ph /\ t e. T ) -> 0 e. RR )
34 12 r19.21bi 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) )
35 34 simprd 
 |-  ( ( ph /\ t e. T ) -> ( y ` t ) <_ 1 )
36 1m0e1 
 |-  ( 1 - 0 ) = 1
37 35 36 breqtrrdi 
 |-  ( ( ph /\ t e. T ) -> ( y ` t ) <_ ( 1 - 0 ) )
38 31 32 33 37 lesubd 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( 1 - ( y ` t ) ) )
39 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
40 32 31 resubcld 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( y ` t ) ) e. RR )
41 2 fvmpt2 
 |-  ( ( t e. T /\ ( 1 - ( y ` t ) ) e. RR ) -> ( X ` t ) = ( 1 - ( y ` t ) ) )
42 39 40 41 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( X ` t ) = ( 1 - ( y ` t ) ) )
43 38 42 breqtrrd 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( X ` t ) )
44 34 simpld 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( y ` t ) )
45 33 31 32 44 lesub2dd 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( y ` t ) ) <_ ( 1 - 0 ) )
46 45 36 breqtrdi 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( y ` t ) ) <_ 1 )
47 42 46 eqbrtrd 
 |-  ( ( ph /\ t e. T ) -> ( X ` t ) <_ 1 )
48 43 47 jca 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) )
49 48 ex 
 |-  ( ph -> ( t e. T -> ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
50 1 49 ralrimi 
 |-  ( ph -> A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) )
51 4 sseli 
 |-  ( t e. V -> t e. T )
52 51 42 sylan2 
 |-  ( ( ph /\ t e. V ) -> ( X ` t ) = ( 1 - ( y ` t ) ) )
53 1red 
 |-  ( ( ph /\ t e. V ) -> 1 e. RR )
54 11 rpred 
 |-  ( ph -> E e. RR )
55 54 adantr 
 |-  ( ( ph /\ t e. V ) -> E e. RR )
56 51 31 sylan2 
 |-  ( ( ph /\ t e. V ) -> ( y ` t ) e. RR )
57 13 r19.21bi 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) < ( y ` t ) )
58 53 55 56 57 ltsub23d 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( y ` t ) ) < E )
59 52 58 eqbrtrd 
 |-  ( ( ph /\ t e. V ) -> ( X ` t ) < E )
60 59 ex 
 |-  ( ph -> ( t e. V -> ( X ` t ) < E ) )
61 1 60 ralrimi 
 |-  ( ph -> A. t e. V ( X ` t ) < E )
62 eldifi 
 |-  ( t e. ( T \ U ) -> t e. T )
63 62 31 sylan2 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( y ` t ) e. RR )
64 54 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> E e. RR )
65 1red 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> 1 e. RR )
66 14 r19.21bi 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( y ` t ) < E )
67 63 64 65 66 ltsub2dd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( 1 - E ) < ( 1 - ( y ` t ) ) )
68 62 42 sylan2 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( X ` t ) = ( 1 - ( y ` t ) ) )
69 67 68 breqtrrd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( 1 - E ) < ( X ` t ) )
70 69 ex 
 |-  ( ph -> ( t e. ( T \ U ) -> ( 1 - E ) < ( X ` t ) ) )
71 1 70 ralrimi 
 |-  ( ph -> A. t e. ( T \ U ) ( 1 - E ) < ( X ` t ) )
72 nfmpt1 
 |-  F/_ t ( t e. T |-> ( 1 - ( y ` t ) ) )
73 2 72 nfcxfr 
 |-  F/_ t X
74 73 nfeq2 
 |-  F/ t x = X
75 fveq1 
 |-  ( x = X -> ( x ` t ) = ( X ` t ) )
76 75 breq2d 
 |-  ( x = X -> ( 0 <_ ( x ` t ) <-> 0 <_ ( X ` t ) ) )
77 75 breq1d 
 |-  ( x = X -> ( ( x ` t ) <_ 1 <-> ( X ` t ) <_ 1 ) )
78 76 77 anbi12d 
 |-  ( x = X -> ( ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) <-> ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
79 74 78 ralbid 
 |-  ( x = X -> ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
80 75 breq1d 
 |-  ( x = X -> ( ( x ` t ) < E <-> ( X ` t ) < E ) )
81 74 80 ralbid 
 |-  ( x = X -> ( A. t e. V ( x ` t ) < E <-> A. t e. V ( X ` t ) < E ) )
82 75 breq2d 
 |-  ( x = X -> ( ( 1 - E ) < ( x ` t ) <-> ( 1 - E ) < ( X ` t ) ) )
83 74 82 ralbid 
 |-  ( x = X -> ( A. t e. ( T \ U ) ( 1 - E ) < ( x ` t ) <-> A. t e. ( T \ U ) ( 1 - E ) < ( X ` t ) ) )
84 79 81 83 3anbi123d 
 |-  ( x = X -> ( ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( x ` t ) ) <-> ( A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) /\ A. t e. V ( X ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( X ` t ) ) ) )
85 84 rspcev 
 |-  ( ( X e. A /\ ( A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) /\ A. t e. V ( X ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( X ` t ) ) ) -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( x ` t ) ) )
86 30 50 61 71 85 syl13anc 
 |-  ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( x ` t ) ) )