Metamath Proof Explorer

Theorem stoweidlem42

Description: This lemma is used to prove that x built as in Lemma 2 of BrosowskiDeutsh p. 91, is such that x > 1 - ε on B. Here X is used to represent x in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem42.1 
|- F/ i ph
stoweidlem42.2 
|- F/ t ph
stoweidlem42.3 
|- F/_ t Y
stoweidlem42.4 
|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
stoweidlem42.5 
|- X = ( seq 1 ( P , U ) ` M )
stoweidlem42.6 
|- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
stoweidlem42.7 
|- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
stoweidlem42.8 
|- ( ph -> M e. NN )
stoweidlem42.9 
|- ( ph -> U : ( 1 ... M ) --> Y )
stoweidlem42.10 
|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )
stoweidlem42.11 
|- ( ph -> E e. RR+ )
stoweidlem42.12 
|- ( ph -> E < ( 1 / 3 ) )
stoweidlem42.13 
|- ( ( ph /\ f e. Y ) -> f : T --> RR )
stoweidlem42.14 
|- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
stoweidlem42.15 
|- ( ph -> T e. _V )
stoweidlem42.16 
|- ( ph -> B C_ T )
Assertion stoweidlem42 
|- ( ph -> A. t e. B ( 1 - E ) < ( X ` t ) )

Proof

Step Hyp Ref Expression
1 stoweidlem42.1 
 |-  F/ i ph
2 stoweidlem42.2 
 |-  F/ t ph
3 stoweidlem42.3 
 |-  F/_ t Y
4 stoweidlem42.4 
 |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
5 stoweidlem42.5 
 |-  X = ( seq 1 ( P , U ) ` M )
6 stoweidlem42.6 
 |-  F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
7 stoweidlem42.7 
 |-  Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
8 stoweidlem42.8 
 |-  ( ph -> M e. NN )
9 stoweidlem42.9 
 |-  ( ph -> U : ( 1 ... M ) --> Y )
10 stoweidlem42.10 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )
11 stoweidlem42.11 
 |-  ( ph -> E e. RR+ )
12 stoweidlem42.12 
 |-  ( ph -> E < ( 1 / 3 ) )
13 stoweidlem42.13 
 |-  ( ( ph /\ f e. Y ) -> f : T --> RR )
14 stoweidlem42.14 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
15 stoweidlem42.15 
 |-  ( ph -> T e. _V )
16 stoweidlem42.16 
 |-  ( ph -> B C_ T )
17 1red 
 |-  ( ph -> 1 e. RR )
18 11 rpred 
 |-  ( ph -> E e. RR )
19 17 18 resubcld 
 |-  ( ph -> ( 1 - E ) e. RR )
20 19 adantr 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) e. RR )
21 18 8 nndivred 
 |-  ( ph -> ( E / M ) e. RR )
22 17 21 resubcld 
 |-  ( ph -> ( 1 - ( E / M ) ) e. RR )
23 22 adantr 
 |-  ( ( ph /\ t e. B ) -> ( 1 - ( E / M ) ) e. RR )
24 8 nnnn0d 
 |-  ( ph -> M e. NN0 )
25 24 adantr 
 |-  ( ( ph /\ t e. B ) -> M e. NN0 )
26 23 25 reexpcld 
 |-  ( ( ph /\ t e. B ) -> ( ( 1 - ( E / M ) ) ^ M ) e. RR )
27 elnnuz 
 |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )
28 8 27 sylib 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
29 28 adantr 
 |-  ( ( ph /\ t e. B ) -> M e. ( ZZ>= ` 1 ) )
30 nfv 
 |-  F/ i t e. B
31 1 30 nfan 
 |-  F/ i ( ph /\ t e. B )
32 nfv 
 |-  F/ i a e. ( 1 ... M )
33 31 32 nfan 
 |-  F/ i ( ( ph /\ t e. B ) /\ a e. ( 1 ... M ) )
34 nfcv 
 |-  F/_ i T
35 nfmpt1 
 |-  F/_ i ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) )
36 34 35 nfmpt 
 |-  F/_ i ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
37 6 36 nfcxfr 
 |-  F/_ i F
38 nfcv 
 |-  F/_ i t
39 37 38 nffv 
 |-  F/_ i ( F ` t )
40 nfcv 
 |-  F/_ i a
41 39 40 nffv 
 |-  F/_ i ( ( F ` t ) ` a )
42 41 nfel1 
 |-  F/ i ( ( F ` t ) ` a ) e. RR
43 33 42 nfim 
 |-  F/ i ( ( ( ph /\ t e. B ) /\ a e. ( 1 ... M ) ) -> ( ( F ` t ) ` a ) e. RR )
44 eleq1 
 |-  ( i = a -> ( i e. ( 1 ... M ) <-> a e. ( 1 ... M ) ) )
45 44 anbi2d 
 |-  ( i = a -> ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) <-> ( ( ph /\ t e. B ) /\ a e. ( 1 ... M ) ) ) )
46 fveq2 
 |-  ( i = a -> ( ( F ` t ) ` i ) = ( ( F ` t ) ` a ) )
47 46 eleq1d 
 |-  ( i = a -> ( ( ( F ` t ) ` i ) e. RR <-> ( ( F ` t ) ` a ) e. RR ) )
48 45 47 imbi12d 
 |-  ( i = a -> ( ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) e. RR ) <-> ( ( ( ph /\ t e. B ) /\ a e. ( 1 ... M ) ) -> ( ( F ` t ) ` a ) e. RR ) ) )
49 16 sselda 
 |-  ( ( ph /\ t e. B ) -> t e. T )
50 ovex 
 |-  ( 1 ... M ) e. _V
51 mptexg 
 |-  ( ( 1 ... M ) e. _V -> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V )
52 50 51 mp1i 
 |-  ( ( ph /\ t e. B ) -> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V )
53 6 fvmpt2 
 |-  ( ( t e. T /\ ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
54 49 52 53 syl2anc 
 |-  ( ( ph /\ t e. B ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
55 9 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) e. Y )
56 simpl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ph )
57 56 55 jca 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ph /\ ( U ` i ) e. Y ) )
58 eleq1 
 |-  ( f = ( U ` i ) -> ( f e. Y <-> ( U ` i ) e. Y ) )
59 58 anbi2d 
 |-  ( f = ( U ` i ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( U ` i ) e. Y ) ) )
60 feq1 
 |-  ( f = ( U ` i ) -> ( f : T --> RR <-> ( U ` i ) : T --> RR ) )
61 59 60 imbi12d 
 |-  ( f = ( U ` i ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` i ) e. Y ) -> ( U ` i ) : T --> RR ) ) )
62 61 13 vtoclg 
 |-  ( ( U ` i ) e. Y -> ( ( ph /\ ( U ` i ) e. Y ) -> ( U ` i ) : T --> RR ) )
63 55 57 62 sylc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )
64 63 adantlr 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )
65 49 adantr 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> t e. T )
66 64 65 ffvelcdmd 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( ( U ` i ) ` t ) e. RR )
67 54 66 fvmpt2d 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) = ( ( U ` i ) ` t ) )
68 67 66 eqeltrd 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) e. RR )
69 43 48 68 chvarfv 
 |-  ( ( ( ph /\ t e. B ) /\ a e. ( 1 ... M ) ) -> ( ( F ` t ) ` a ) e. RR )
70 remulcl 
 |-  ( ( a e. RR /\ j e. RR ) -> ( a x. j ) e. RR )
71 70 adantl 
 |-  ( ( ( ph /\ t e. B ) /\ ( a e. RR /\ j e. RR ) ) -> ( a x. j ) e. RR )
72 29 69 71 seqcl 
 |-  ( ( ph /\ t e. B ) -> ( seq 1 ( x. , ( F ` t ) ) ` M ) e. RR )
73 11 rpcnd 
 |-  ( ph -> E e. CC )
74 8 nncnd 
 |-  ( ph -> M e. CC )
75 8 nnne0d 
 |-  ( ph -> M =/= 0 )
76 73 74 75 divcan1d 
 |-  ( ph -> ( ( E / M ) x. M ) = E )
77 76 eqcomd 
 |-  ( ph -> E = ( ( E / M ) x. M ) )
78 77 oveq2d 
 |-  ( ph -> ( 1 - E ) = ( 1 - ( ( E / M ) x. M ) ) )
79 1cnd 
 |-  ( ph -> 1 e. CC )
80 73 74 75 divcld 
 |-  ( ph -> ( E / M ) e. CC )
81 80 74 mulcld 
 |-  ( ph -> ( ( E / M ) x. M ) e. CC )
82 79 81 negsubd 
 |-  ( ph -> ( 1 + -u ( ( E / M ) x. M ) ) = ( 1 - ( ( E / M ) x. M ) ) )
83 80 74 mulneg1d 
 |-  ( ph -> ( -u ( E / M ) x. M ) = -u ( ( E / M ) x. M ) )
84 83 eqcomd 
 |-  ( ph -> -u ( ( E / M ) x. M ) = ( -u ( E / M ) x. M ) )
85 84 oveq2d 
 |-  ( ph -> ( 1 + -u ( ( E / M ) x. M ) ) = ( 1 + ( -u ( E / M ) x. M ) ) )
86 78 82 85 3eqtr2d 
 |-  ( ph -> ( 1 - E ) = ( 1 + ( -u ( E / M ) x. M ) ) )
87 21 renegcld 
 |-  ( ph -> -u ( E / M ) e. RR )
88 8 nnred 
 |-  ( ph -> M e. RR )
89 3re 
 |-  3 e. RR
90 89 a1i 
 |-  ( ph -> 3 e. RR )
91 3ne0 
 |-  3 =/= 0
92 91 a1i 
 |-  ( ph -> 3 =/= 0 )
93 90 92 rereccld 
 |-  ( ph -> ( 1 / 3 ) e. RR )
94 1lt3 
 |-  1 < 3
95 94 a1i 
 |-  ( ph -> 1 < 3 )
96 0lt1 
 |-  0 < 1
97 96 a1i 
 |-  ( ph -> 0 < 1 )
98 3pos 
 |-  0 < 3
99 98 a1i 
 |-  ( ph -> 0 < 3 )
100 ltdiv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( 3 e. RR /\ 0 < 3 ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( 1 < 3 <-> ( 1 / 3 ) < ( 1 / 1 ) ) )
101 17 97 90 99 17 97 100 syl222anc 
 |-  ( ph -> ( 1 < 3 <-> ( 1 / 3 ) < ( 1 / 1 ) ) )
102 95 101 mpbid 
 |-  ( ph -> ( 1 / 3 ) < ( 1 / 1 ) )
103 1div1e1 
 |-  ( 1 / 1 ) = 1
104 102 103 breqtrdi 
 |-  ( ph -> ( 1 / 3 ) < 1 )
105 18 93 17 12 104 lttrd 
 |-  ( ph -> E < 1 )
106 8 nnge1d 
 |-  ( ph -> 1 <_ M )
107 18 17 88 105 106 ltletrd 
 |-  ( ph -> E < M )
108 18 88 107 ltled 
 |-  ( ph -> E <_ M )
109 11 rpregt0d 
 |-  ( ph -> ( E e. RR /\ 0 < E ) )
110 8 nngt0d 
 |-  ( ph -> 0 < M )
111 lediv2 
 |-  ( ( ( E e. RR /\ 0 < E ) /\ ( M e. RR /\ 0 < M ) /\ ( E e. RR /\ 0 < E ) ) -> ( E <_ M <-> ( E / M ) <_ ( E / E ) ) )
112 109 88 110 109 111 syl121anc 
 |-  ( ph -> ( E <_ M <-> ( E / M ) <_ ( E / E ) ) )
113 108 112 mpbid 
 |-  ( ph -> ( E / M ) <_ ( E / E ) )
114 11 rpcnne0d 
 |-  ( ph -> ( E e. CC /\ E =/= 0 ) )
115 divid 
 |-  ( ( E e. CC /\ E =/= 0 ) -> ( E / E ) = 1 )
116 114 115 syl 
 |-  ( ph -> ( E / E ) = 1 )
117 113 116 breqtrd 
 |-  ( ph -> ( E / M ) <_ 1 )
118 21 17 lenegd 
 |-  ( ph -> ( ( E / M ) <_ 1 <-> -u 1 <_ -u ( E / M ) ) )
119 117 118 mpbid 
 |-  ( ph -> -u 1 <_ -u ( E / M ) )
120 bernneq 
 |-  ( ( -u ( E / M ) e. RR /\ M e. NN0 /\ -u 1 <_ -u ( E / M ) ) -> ( 1 + ( -u ( E / M ) x. M ) ) <_ ( ( 1 + -u ( E / M ) ) ^ M ) )
121 87 24 119 120 syl3anc 
 |-  ( ph -> ( 1 + ( -u ( E / M ) x. M ) ) <_ ( ( 1 + -u ( E / M ) ) ^ M ) )
122 79 80 negsubd 
 |-  ( ph -> ( 1 + -u ( E / M ) ) = ( 1 - ( E / M ) ) )
123 122 oveq1d 
 |-  ( ph -> ( ( 1 + -u ( E / M ) ) ^ M ) = ( ( 1 - ( E / M ) ) ^ M ) )
124 121 123 breqtrd 
 |-  ( ph -> ( 1 + ( -u ( E / M ) x. M ) ) <_ ( ( 1 - ( E / M ) ) ^ M ) )
125 86 124 eqbrtrd 
 |-  ( ph -> ( 1 - E ) <_ ( ( 1 - ( E / M ) ) ^ M ) )
126 125 adantr 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) <_ ( ( 1 - ( E / M ) ) ^ M ) )
127 eqid 
 |-  seq 1 ( x. , ( F ` t ) ) = seq 1 ( x. , ( F ` t ) )
128 8 adantr 
 |-  ( ( ph /\ t e. B ) -> M e. NN )
129 eqid 
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) )
130 31 66 129 fmptdf 
 |-  ( ( ph /\ t e. B ) -> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) : ( 1 ... M ) --> RR )
131 54 feq1d 
 |-  ( ( ph /\ t e. B ) -> ( ( F ` t ) : ( 1 ... M ) --> RR <-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) : ( 1 ... M ) --> RR ) )
132 130 131 mpbird 
 |-  ( ( ph /\ t e. B ) -> ( F ` t ) : ( 1 ... M ) --> RR )
133 10 r19.21bi 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. B ) -> ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )
134 133 an32s 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )
135 134 67 breqtrrd 
 |-  ( ( ( ph /\ t e. B ) /\ i e. ( 1 ... M ) ) -> ( 1 - ( E / M ) ) < ( ( F ` t ) ` i ) )
136 80 addlidd 
 |-  ( ph -> ( 0 + ( E / M ) ) = ( E / M ) )
137 lediv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( M e. RR /\ 0 < M ) /\ ( E e. RR /\ 0 < E ) ) -> ( 1 <_ M <-> ( E / M ) <_ ( E / 1 ) ) )
138 17 97 88 110 109 137 syl221anc 
 |-  ( ph -> ( 1 <_ M <-> ( E / M ) <_ ( E / 1 ) ) )
139 106 138 mpbid 
 |-  ( ph -> ( E / M ) <_ ( E / 1 ) )
140 73 div1d 
 |-  ( ph -> ( E / 1 ) = E )
141 139 140 breqtrd 
 |-  ( ph -> ( E / M ) <_ E )
142 21 18 17 141 105 lelttrd 
 |-  ( ph -> ( E / M ) < 1 )
143 136 142 eqbrtrd 
 |-  ( ph -> ( 0 + ( E / M ) ) < 1 )
144 0red 
 |-  ( ph -> 0 e. RR )
145 144 21 17 ltaddsubd 
 |-  ( ph -> ( ( 0 + ( E / M ) ) < 1 <-> 0 < ( 1 - ( E / M ) ) ) )
146 143 145 mpbid 
 |-  ( ph -> 0 < ( 1 - ( E / M ) ) )
147 22 146 elrpd 
 |-  ( ph -> ( 1 - ( E / M ) ) e. RR+ )
148 147 adantr 
 |-  ( ( ph /\ t e. B ) -> ( 1 - ( E / M ) ) e. RR+ )
149 39 31 127 128 132 135 148 stoweidlem3 
 |-  ( ( ph /\ t e. B ) -> ( ( 1 - ( E / M ) ) ^ M ) < ( seq 1 ( x. , ( F ` t ) ) ` M ) )
150 20 26 72 126 149 lelttrd 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) < ( seq 1 ( x. , ( F ` t ) ) ` M ) )
151 7 fvmpt2 
 |-  ( ( t e. T /\ ( seq 1 ( x. , ( F ` t ) ) ` M ) e. RR ) -> ( Z ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
152 49 72 151 syl2anc 
 |-  ( ( ph /\ t e. B ) -> ( Z ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
153 150 152 breqtrrd 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) < ( Z ` t ) )
154 simpl 
 |-  ( ( ph /\ t e. B ) -> ph )
155 1 3 4 5 6 7 15 8 9 13 14 fmuldfeq 
 |-  ( ( ph /\ t e. T ) -> ( X ` t ) = ( Z ` t ) )
156 154 49 155 syl2anc 
 |-  ( ( ph /\ t e. B ) -> ( X ` t ) = ( Z ` t ) )
157 153 156 breqtrrd 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) < ( X ` t ) )
158 157 ex 
 |-  ( ph -> ( t e. B -> ( 1 - E ) < ( X ` t ) ) )
159 2 158 ralrimi 
 |-  ( ph -> A. t e. B ( 1 - E ) < ( X ` t ) )