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 i φ
stoweidlem42.2 t φ
stoweidlem42.3 _ t Y
stoweidlem42.4 P = f Y , g Y t T f t g t
stoweidlem42.5 X = seq 1 P U M
stoweidlem42.6 F = t T i 1 M U i t
stoweidlem42.7 Z = t T seq 1 × F t M
stoweidlem42.8 φ M
stoweidlem42.9 φ U : 1 M Y
stoweidlem42.10 φ i 1 M t B 1 E M < U i t
stoweidlem42.11 φ E +
stoweidlem42.12 φ E < 1 3
stoweidlem42.13 φ f Y f : T
stoweidlem42.14 φ f Y g Y t T f t g t Y
stoweidlem42.15 φ T V
stoweidlem42.16 φ B T
Assertion stoweidlem42 φ t B 1 E < X t

Proof

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