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 ⊢ Ⅎ 𝑡 𝜑
stoweidlem41.2 ⊢ 𝑋 = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
stoweidlem41.3 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ 1 )
stoweidlem41.4 ⊢ 𝑉 ⊆ 𝑇
stoweidlem41.5 ⊢ ( 𝜑 → 𝑦 ∈ 𝐴 )
stoweidlem41.6 ⊢ ( 𝜑 → 𝑦 : 𝑇 ⟶ ℝ )
stoweidlem41.7 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem41.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem41.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem41.10 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑤 ) ∈ 𝐴 )
stoweidlem41.11 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem41.12 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) )
stoweidlem41.13 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) )
stoweidlem41.14 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 )
Assertion stoweidlem41 ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem41.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem41.2 ⊢ 𝑋 = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
3 stoweidlem41.3 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ 1 )
4 stoweidlem41.4 ⊢ 𝑉 ⊆ 𝑇
5 stoweidlem41.5 ⊢ ( 𝜑 → 𝑦 ∈ 𝐴 )
6 stoweidlem41.6 ⊢ ( 𝜑 → 𝑦 : 𝑇 ⟶ ℝ )
7 stoweidlem41.7 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
8 stoweidlem41.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9 stoweidlem41.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem41.10 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑤 ) ∈ 𝐴 )
11 stoweidlem41.11 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
12 stoweidlem41.12 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) )
13 stoweidlem41.13 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) )
14 stoweidlem41.14 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 )
15 1re ⊢ 1 ∈ ℝ
16 3 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ 1 ∈ ℝ ) → ( 𝐹 ‘ 𝑡 ) = 1 )
17 15 16 mpan2 ⊢ ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) = 1 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) = 1 )
19 18 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝑦 ‘ 𝑡 ) ) = ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
20 1 19 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝑦 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) ) )
21 20 2 eqtr4di ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝑦 ‘ 𝑡 ) ) ) = 𝑋 )
22 10 stoweidlem4 ⊢ ( ( 𝜑 ∧ 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
23 15 22 mpan2 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
24 3 23 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
25 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ 1 )
26 3 25 nfcxfr ⊢ Ⅎ 𝑡 𝐹
27 nfcv ⊢ Ⅎ 𝑡 𝑦
28 26 27 1 7 8 9 10 stoweidlem33 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝑦 ‘ 𝑡 ) ) ) ∈ 𝐴 )
29 24 5 28 mpd3an23 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝑦 ‘ 𝑡 ) ) ) ∈ 𝐴 )
30 21 29 eqeltrrd ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
31 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑦 ‘ 𝑡 ) ∈ ℝ )
32 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
33 0red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ∈ ℝ )
34 12 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) )
35 34 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑦 ‘ 𝑡 ) ≤ 1 )
36 1m0e1 ⊢ ( 1 − 0 ) = 1
37 35 36 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑦 ‘ 𝑡 ) ≤ ( 1 − 0 ) )
38 31 32 33 37 lesubd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
40 32 31 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( 𝑦 ‘ 𝑡 ) ) ∈ ℝ )
41 2 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( 1 − ( 𝑦 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝑋 ‘ 𝑡 ) = ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
42 39 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑋 ‘ 𝑡 ) = ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
43 38 42 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑋 ‘ 𝑡 ) )
44 34 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑦 ‘ 𝑡 ) )
45 33 31 32 44 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( 𝑦 ‘ 𝑡 ) ) ≤ ( 1 − 0 ) )
46 45 36 breqtrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( 𝑦 ‘ 𝑡 ) ) ≤ 1 )
47 42 46 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑋 ‘ 𝑡 ) ≤ 1 )
48 43 47 jca ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) )
49 48 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
50 1 49 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) )
51 4 sseli ⊢ ( 𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑇 )
52 51 42 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑋 ‘ 𝑡 ) = ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
53 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 1 ∈ ℝ )
54 11 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐸 ∈ ℝ )
56 51 31 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑦 ‘ 𝑡 ) ∈ ℝ )
57 13 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) )
58 53 55 56 57 ltsub23d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( 𝑦 ‘ 𝑡 ) ) < 𝐸 )
59 52 58 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑋 ‘ 𝑡 ) < 𝐸 )
60 59 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑉 → ( 𝑋 ‘ 𝑡 ) < 𝐸 ) )
61 1 60 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑉 ( 𝑋 ‘ 𝑡 ) < 𝐸 )
62 eldifi ⊢ ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → 𝑡 ∈ 𝑇 )
63 62 31 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑦 ‘ 𝑡 ) ∈ ℝ )
64 54 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐸 ∈ ℝ )
65 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 1 ∈ ℝ )
66 14 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑦 ‘ 𝑡 ) < 𝐸 )
67 63 64 65 66 ltsub2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 1 − 𝐸 ) < ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
68 62 42 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑋 ‘ 𝑡 ) = ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
69 67 68 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) )
70 69 ex ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
71 1 70 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) )
72 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
73 2 72 nfcxfr ⊢ Ⅎ 𝑡 𝑋
74 73 nfeq2 ⊢ Ⅎ 𝑡 𝑥 = 𝑋
75 fveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝑡 ) = ( 𝑋 ‘ 𝑡 ) )
76 75 breq2d ⊢ ( 𝑥 = 𝑋 → ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ↔ 0 ≤ ( 𝑋 ‘ 𝑡 ) ) )
77 75 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ‘ 𝑡 ) ≤ 1 ↔ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) )
78 76 77 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
79 74 78 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
80 75 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ‘ 𝑡 ) < 𝐸 ↔ ( 𝑋 ‘ 𝑡 ) < 𝐸 ) )
81 74 80 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝐸 ↔ ∀ 𝑡 ∈ 𝑉 ( 𝑋 ‘ 𝑡 ) < 𝐸 ) )
82 75 breq2d ⊢ ( 𝑥 = 𝑋 → ( ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ↔ ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
83 74 82 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
84 79 81 83 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) ) )
85 84 rspcev ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )
86 30 50 61 71 85 syl13anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )