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 t φ
stoweidlem41.2 X = t T 1 y t
stoweidlem41.3 F = t T 1
stoweidlem41.4 V T
stoweidlem41.5 φ y A
stoweidlem41.6 φ y : T
stoweidlem41.7 φ f A f : T
stoweidlem41.8 φ f A g A t T f t + g t A
stoweidlem41.9 φ f A g A t T f t g t A
stoweidlem41.10 φ w t T w A
stoweidlem41.11 φ E +
stoweidlem41.12 φ t T 0 y t y t 1
stoweidlem41.13 φ t V 1 E < y t
stoweidlem41.14 φ t T U y t < E
Assertion stoweidlem41 φ x A t T 0 x t x t 1 t V x t < E t T U 1 E < x t

Proof

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